summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-11-16 15:34:27 +0100
committerSon HO2022-11-16 15:45:32 +0100
commitbbdd0da25b974b03d58489d3bbc2654f4f774644 (patch)
treed95f882effb9e0a576ab396f7741c2f4a42dc0c9
parent08530a51b8861e3dbb1a409d0c6f0e8c44adec83 (diff)
Add a nix derivation for the Coq proofs
-rw-r--r--Makefile6
-rw-r--r--flake.nix17
-rw-r--r--tests/coq/Makefile6
-rw-r--r--tests/coq/_CoqProject.template3
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