From eb519e0e56d30763db6ca6667a9f4095061252a4 Mon Sep 17 00:00:00 2001
From: Ryan Lahfa
Date: Wed, 24 Apr 2024 11:34:27 +0200
Subject: chore(ci): move Lean CI under Nix

As it often happens, the Lean CI under Ubuntu is broken:
https://github.com/AeneasVerif/aeneas/actions/runs/8814059410/job/24193132680?pr=135
and blocking PRs.

Lean doesn't work nicely under the Nix sandbox, but in a CI context, we
can impurely run scripts and use Nix to get our dependencies, e.g. curl
or elan in this case.

It is still more reliable than letting Ubuntu or GitHub Actions figure
out their signing for their APT repositories apparently.

Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
---
 .github/workflows/ci.yml | 19 +++++--------------
 flake.nix                |  1 +
 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
-- 
cgit v1.2.3