From d527795cb5c24892617bd5f7df75450e50069194 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 10 Nov 2023 17:30:23 +0100
Subject: Update the ci.yml

---
 .github/workflows/ci.yml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to '.github/workflows')

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
-- 
cgit v1.2.3