summaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorSon Ho2023-06-02 16:10:20 +0200
committerSon HO2023-06-04 21:54:38 +0200
commit54afbf3a8b71ee729641ee3024d19aaf8fa92a67 (patch)
treea014bdb321be1ada84a8687e38bd17c487d68889 /Makefile
parent435d75174a12a47da84537cc7c9730a0eccf6d1f (diff)
Start setting up the Nix derivation for HOL4
Diffstat (limited to 'Makefile')
-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