summaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--Makefile6
1 files changed, 5 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 14f35ce7..a5d1fd09 100644
--- a/Makefile
+++ b/Makefile
@@ -283,7 +283,7 @@ thol4p-%:
# Nix - TODO: add the lean tests
.PHONY: nix
-nix: nix-aeneas-tests nix-aeneas-verify-fstar nix-aeneas-verify-coq
+nix: nix-aeneas-tests nix-aeneas-verify-fstar nix-aeneas-verify-coq nix-aeneas-verify-hol4
.PHONY: nix-aeneas-tests
nix-aeneas-tests:
@@ -300,3 +300,7 @@ nix-aeneas-verify-coq:
.PHONY: nix-aeneas-verify-lean
nix-aeneas-verify-lean:
nix build .#checks.x86_64-linux.aeneas-verify-lean --show-trace -L
+
+.PHONY: nix-aeneas-verify-hol4
+nix-aeneas-verify-hol4:
+ nix build .#checks.x86_64-linux.aeneas-verify-hol4 --show-trace -L