summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2023-12-23 00:19:08 +0100
committerSon Ho2023-12-23 00:19:08 +0100
commitaa5e25785738a779ca5fd89191c85d6ab828c142 (patch)
treeecc97c6316d121d6d5754eac88c25e4361dab49e
parent6fd112a30d12cda6390ea3b856a81096d6bcedfe (diff)
Update the flake.nix and the ci.yml
-rw-r--r--.github/workflows/ci.yml1
-rw-r--r--flake.nix16
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
diff --git a/flake.nix b/flake.nix
index 8263174d..82179fcb 100644
--- 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; };
});
}