From 4ca3f4dd129a228cbb9eb7ab5cfd609be4483db8 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 8 Mar 2024 16:41:05 +0100
Subject: Update the flake.nix

---
 flake.nix | 19 +++++--------------
 1 file changed, 5 insertions(+), 14 deletions(-)

(limited to 'flake.nix')

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; };
       });
 }
-- 
cgit v1.2.3