Merge pull request #2094 from cryspen/fix-ci-aeneas-cache

ci: use Aeneas's olean cache

Author: abentkamp

.github/workflows/core_models.yml

@@ -205,7 +205,9 @@ jobs:
 
       # ---- The actual pipeline ------------------------------------------
       - name: Extract Lean library, build Lean library, run regression tests
-        run: make CHARON=$AENEAS_DIR/charon/bin/charon AENEAS=$AENEAS_DIR/bin/aeneas lean tests
+        run: |
+          unset CI # Allows us to use Aeneas's olean cache
+          make CHARON=$AENEAS_DIR/charon/bin/charon AENEAS=$AENEAS_DIR/bin/aeneas lean tests
 
       # ---- Enforce that committed extraction matches re-extraction ------
       # If this fails: someone changed Rust source / patcher without

.github/workflows/verify_extraction.yml

@@ -79,6 +79,7 @@ jobs:
 
     - name: Build the example
       run: |
+        unset CI # Allows us to use Aeneas's olean cache
         cd examples/${{ matrix.example }}
         PATH="$HOME/.cargo/bin:$PATH" nix develop ..#ci-examples --command make clean
         PATH="$HOME/.cargo/bin:$PATH" nix develop ..#ci-examples --command make