Update the flake.nix and the ci.yml

AeneasVerif · Dec 22, 2023 · aa5e257 · aa5e257
1 parent 6fd112a
commit aa5e257
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 1 deletion.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -14,6 +14,7 @@ jobs:
       - 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-fstar-split
       - 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

diff --git a/flake.nix b/flake.nix
@@ -114,6 +114,18 @@
           # The tests don't generate anything - TODO: actually they do
           installPhase = "touch $out";
         };
+        # Replay the F* proofs for the cases where we split the fwd/back functions.
+        aeneas-verify-fstar-split = pkgs.stdenv.mkDerivation {
+          name = "aeneas_verify_fstar_split";
+          src = ./tests/fstar-split;
+          FSTAR_EXE = "${hacl-nix.packages.${system}.fstar}/bin/fstar.exe";
+          buildPhase= ''
+            make prepare-projects
+            make verify -j $NIX_BUILD_CORES
+          '';
+          # The tests don't generate anything - TODO: actually they do
+          installPhase = "touch $out";
+        };
         # Replay the Coq proofs.
         aeneas-verify-coq = pkgs.stdenv.mkDerivation {
           name = "aeneas_verify_coq";
@@ -170,6 +182,8 @@
           inherit aeneas;
           default = aeneas;
         };
-        checks = { inherit aeneas aeneas-tests aeneas-verify-fstar aeneas-verify-coq aeneas-verify-lean aeneas-verify-hol4; };
+        checks = {
+          inherit aeneas aeneas-tests aeneas-verify-fstar aeneas-verify-fstar-split
+                  aeneas-verify-coq aeneas-verify-lean aeneas-verify-hol4; };
       });
 }