summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon HO2024-04-26 10:54:26 +0200
committerGitHub2024-04-26 10:54:26 +0200
commit2df6dd65b84a2fd9aad4f716f323bf3f85bf82db (patch)
tree303766a9be2889fb7841526c6c671912db8e478e
parenta3e38d5f47e4780768902e49e28e471e38efd40a (diff)
parenteb519e0e56d30763db6ca6667a9f4095061252a4 (diff)
Merge pull request #158 from RaitoBezarius/lean-ci-under-nix
chore(ci): move Lean CI under Nix
-rw-r--r--.github/workflows/ci.yml19
-rw-r--r--flake.nix1
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