summaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorSon Ho2022-11-16 15:34:27 +0100
committerSon HO2022-11-16 15:45:32 +0100
commitbbdd0da25b974b03d58489d3bbc2654f4f774644 (patch)
treed95f882effb9e0a576ab396f7741c2f4a42dc0c9 /Makefile
parent08530a51b8861e3dbb1a409d0c6f0e8c44adec83 (diff)
Add a nix derivation for the Coq proofs
Diffstat (limited to '')
-rw-r--r--Makefile6
1 files changed, 5 insertions, 1 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