Add a nix derivation for the Coq proofs

4 files changed, 25 insertions, 7 deletions

diff --git a/Makefile b/Makefile
index 3de839fe..797c8861 100644
--- a/Makefile
+++ b/Makefile
@@ -218,7 +218,7 @@ tcoqp-%:
 
 # Nix
 .PHONY: nix
-nix: nix-aeneas-tests nix-aeneas-verify-fstar
+nix: nix-aeneas-tests nix-aeneas-verify-fstar nix-aeneas-verify-coq
 
 .PHONY: nix-aeneas-tests
 nix-aeneas-tests:
@@ -227,3 +227,7 @@ nix-aeneas-tests:
 .PHONY: nix-aeneas-verify-fstar
 nix-aeneas-verify-fstar:
 	nix build .#checks.x86_64-linux.aeneas-verify-fstar --show-trace -L
+
+.PHONY: nix-aeneas-verify-coq
+nix-aeneas-verify-coq:
+	nix build .#checks.x86_64-linux.aeneas-verify-coq --show-trace -L
diff --git a/flake.nix b/flake.nix
index 1b3e4b31..50c79337 100644
--- a/flake.nix
+++ b/flake.nix
@@ -13,6 +13,7 @@
       let
         pkgs = import nixpkgs { inherit system; };
         ocamlPackages = pkgs.ocamlPackages;
+        coqPackages = pkgs.coqPackages;
         easy_logging = ocamlPackages.buildDunePackage rec {
           pname = "easy_logging";
           version = "0.8.2";
@@ -74,10 +75,18 @@
         };
         # Replay the F* proofs.
         aeneas-verify-fstar = pkgs.stdenv.mkDerivation {
-          name = "aeneas_tests";
+          name = "aeneas_verify_fstar";
           src = ./tests/fstar;
           FSTAR_EXE = "${hacl-nix.packages.${system}.fstar}/bin/fstar.exe";
-          # Tests don't generate anything
+          # The tests don't generate anything
+          installPhase = "touch $out";
+        };
+        # Replay the Coq proofs.
+        aeneas-verify-coq = pkgs.stdenv.mkDerivation {
+          name = "aeneas_verify_coq";
+          src = ./tests/coq;
+          buildInputs = [ pkgs.coq ];
+          # The tests don't generate anything
           installPhase = "touch $out";
         };
       in {
@@ -85,7 +94,7 @@
           inherit aeneas;
           default = aeneas;
         };
-        checks = { inherit aeneas aeneas-tests aeneas-verify-fstar; };
-        hydraJobs = { inherit aeneas aeneas-tests aeneas-verify-fstar; };
+        checks = { inherit aeneas aeneas-tests aeneas-verify-fstar aeneas-verify-coq; };
+        hydraJobs = { inherit aeneas aeneas-tests aeneas-verify-fstar aeneas-verify-coq; };
       });
 }
diff --git a/tests/coq/Makefile b/tests/coq/Makefile
index 8dee394b..c2b9e379 100644
--- a/tests/coq/Makefile
+++ b/tests/coq/Makefile
@@ -29,8 +29,10 @@ gen-coq-project-%:
 	rm -f $*/_CoqProject
 	echo "# This file was automatically generated - see ../Makefile" >> $*/_CoqProject
 	cat _CoqProject.template >> $*/_CoqProject
-	echo $(patsubst $*/%,"\n"%,$(wildcard $*/*.v)) >> $*/_CoqProject
-	sed -i -z "s/ \n/\n/g" $*/_CoqProject
+	echo $(wildcard $*/*.v) >> $*/_CoqProject # List the .v files
+	sed -i -z "s/"$*"\//\n/g" $*/_CoqProject # Insert breaks
+	sed -i -z "s/ \n/\n/g" $*/_CoqProject # Remove whitespaces at the end of lines
+	cat $*/_CoqProject
 
 .PHONY: clean-%
 clean-%:
diff --git a/tests/coq/_CoqProject.template b/tests/coq/_CoqProject.template
new file mode 100644
index 00000000..672629b2
--- /dev/null
+++ b/tests/coq/_CoqProject.template
@@ -0,0 +1,3 @@
+-R . Lib
+-arg -w
+-arg all