summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2023-11-10 17:30:23 +0100
committerSon Ho2023-11-10 17:30:23 +0100
commitd527795cb5c24892617bd5f7df75450e50069194 (patch)
treefdd01fd2a06a743f7e6c24ab01bad8aa85886208
parent57ffe2c9b46e196310f0abd6c001751fe2f2a6b9 (diff)
Update the ci.yml
Diffstat (limited to '')
-rw-r--r--.github/workflows/ci.yml8
1 files changed, 4 insertions, 4 deletions
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 82b7e724..6b5aacf0 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -15,11 +15,10 @@ jobs:
- run: nix build -L .#checks.x86_64-linux.aeneas-tests
- run: nix build -L .#checks.x86_64-linux.aeneas-verify-fstar
- run: nix build -L .#checks.x86_64-linux.aeneas-verify-coq
- # HOL4 can be reactivated, but it is very slow
- #- run: nix build -L .#checks.x86_64-linux.aeneas-verify-hol4
+ - run: nix build -L .#checks.x86_64-linux.aeneas-verify-hol4
# Lean doesn't work with Nix
#- run: nix build -L .#checks.x86_64-linux.aeneas-verify-lean
- lean: # Lean isn't supported by Nix, so we need to add extra steps
+ lean: # Lean isn't supported by Nix, so we put it in a different job
runs-on: [ubuntu-latest]
steps:
# Install curl
@@ -30,5 +29,6 @@ jobs:
# Checkout the repo and download it to the runner
- name: Checkout
uses: actions/checkout@v4
- # Verify
+ # 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