Merge pull request #158 from RaitoBezarius/lean-ci-under-nix

chore(ci): move Lean CI under Nix

2 files changed, 6 insertions, 14 deletions

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index eeb92c51..0ccc74e0 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -28,7 +28,6 @@ jobs:
     needs: check_if_skip_duplicate_job
     if: needs.check_if_skip_duplicate_job.outputs.should_skip != 'true'
     steps:
-      #- uses: cachix/install-nix-action@v22
       - uses: actions/checkout@v4
       - run: nix build -L .#checks.x86_64-linux.aeneas-check-tidiness
       - run: nix build -L .#aeneas
@@ -36,22 +35,14 @@ jobs:
       - run: nix build -L .#checks.x86_64-linux.aeneas-verify-fstar
       - run: nix build -L .#checks.x86_64-linux.aeneas-verify-coq
       - run: nix build -L .#checks.x86_64-linux.aeneas-verify-hol4
-      # Lean doesn't work with Nix
+      # Lean cannot run its tests in the sandbox because `elan` will download things
       #- run: nix build -L .#checks.x86_64-linux.aeneas-verify-lean
 
-  lean: # Lean isn't supported by Nix, so we put it in a different job
+  lean:
     runs-on: [ubuntu-latest]
     needs: check_if_skip_duplicate_job
     if: needs.check_if_skip_duplicate_job.outputs.should_skip != 'true'
     steps:
-      # Install curl
-      - run: sudo apt update && sudo apt install curl
-      # Install Elan (https://leanprover-community.github.io/install/linux.html) and Lean in
-      # non-interactive mode:
-      - run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | bash -s -- -y
-      # Checkout the repo and download it to the runner
-      - name: Checkout
-        uses: actions/checkout@v4
-      # Verify - note that we need to update the environment with `source` so
-      # that the lake binary is in the path.
-      - run: source ~/.profile && cd tests/lean && make
+      - uses: actions/checkout@v4
+      - uses: cachix/install-nix-action@v26
+      - run: nix develop --command bash -c "cd tests/lean && make"
diff --git a/flake.nix b/flake.nix
index f77bd23b..7faee70a 100644
--- a/flake.nix
+++ b/flake.nix
@@ -171,6 +171,7 @@
         };
         devShells.default = pkgs.mkShell {
           packages = [
+            pkgs.elan
             pkgs.ocamlPackages.ocaml
             pkgs.ocamlPackages.ocamlformat
             pkgs.ocamlPackages.menhir