Merge pull request #83 from AeneasVerif/son/backs

Remove the option to split the forward/backward functions

1 files changed, 5 insertions, 14 deletions

diff --git a/flake.nix b/flake.nix
index 82179fcb..cfeb5188 100644
--- a/flake.nix
+++ b/flake.nix
@@ -114,18 +114,6 @@
           # 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";
@@ -183,7 +171,10 @@
           default = aeneas;
         };
         checks = {
-          inherit aeneas aeneas-tests aeneas-verify-fstar aeneas-verify-fstar-split
-                  aeneas-verify-coq aeneas-verify-lean aeneas-verify-hol4; };
+          inherit aeneas aeneas-tests
+                  aeneas-verify-fstar
+                  aeneas-verify-coq
+                  aeneas-verify-lean
+                  aeneas-verify-hol4; };
       });
 }