diff options
| -rw-r--r-- | .github/workflows/ci.yml | 1 | ||||
| -rw-r--r-- | flake.nix | 16 |
2 files changed, 16 insertions, 1 deletions
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 6b5aacf0..2039e65d 100644 --- 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 @@ -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; }; }); } |