flake: group the main checks into a single derivation

AeneasVerif · Nov 29, 2024 · 7837bd0 · 7837bd0
1 parent 0b3b38a
commit 7837bd0
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 12 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -39,18 +39,14 @@ jobs:
       - run: nix build -L .#checks.x86_64-linux.aeneas-check-tidiness
       - run: nix build -L .#checks.x86_64-linux.check-charon-pin
       - run: nix build -L .#aeneas
-      - 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
-      - run: nix build -L .#checks.x86_64-linux.aeneas-verify-hol4
-      # Lean cannot run its tests in the sandbox because `elan` will download things
-      #- run: nix build -L .#checks.x86_64-linux.aeneas-verify-lean
+      - run: nix build -L .#checks.x86_64-linux.default
 
   lean:
     runs-on: [self-hosted, linux, nix]
     needs: check_if_skip_duplicate_job
     if: needs.check_if_skip_duplicate_job.outputs.should_skip != 'true'
     steps:
+      # Lean cannot run its tests in the sandbox because `elan` will download things
       - uses: actions/checkout@v4
       - run: nix develop --command bash -c "cd tests/lean && make"
 

diff --git a/flake.nix b/flake.nix
@@ -199,6 +199,14 @@
           installPhase = "touch $out";
         };
 
+        aeneas-checks = pkgs.runCommand "aeneas-checks" { } ''
+          echo ${aeneas-tests}
+          echo ${aeneas-verify-coq}
+          echo ${aeneas-verify-fstar}
+          echo ${aeneas-verify-hol4}
+          touch $out
+        '';
+
         check-charon-pin = pkgs.runCommand "aeneas-check-charon-pin"
           {
             buildInputs = [ pkgs.jq ];
@@ -241,12 +249,8 @@
           ];
         };
         checks = {
-          inherit aeneas aeneas-tests
-            aeneas-verify-fstar
-            aeneas-verify-coq
-            aeneas-verify-hol4
-            aeneas-check-tidiness
-            check-charon-pin;
+          default = aeneas-checks;
+          inherit aeneas-check-tidiness check-charon-pin;
         };
       });
 }