From aa5e25785738a779ca5fd89191c85d6ab828c142 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sat, 23 Dec 2023 00:19:08 +0100
Subject: Update the flake.nix and the ci.yml

---
 flake.nix | 16 +++++++++++++++-
 1 file changed, 15 insertions(+), 1 deletion(-)

(limited to 'flake.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; };
       });
 }
-- 
cgit v1.2.3