From 54afbf3a8b71ee729641ee3024d19aaf8fa92a67 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 2 Jun 2023 16:10:20 +0200
Subject: Start setting up the Nix derivation for HOL4

---
 Makefile | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'Makefile')

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
-- 
cgit v1.2.3