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

---
 tests/hol4/Makefile | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

(limited to 'tests/hol4/Makefile')

diff --git a/tests/hol4/Makefile b/tests/hol4/Makefile
index fa2c5512..cef04aca 100644
--- a/tests/hol4/Makefile
+++ b/tests/hol4/Makefile
@@ -9,6 +9,7 @@ CLEAN_DIRS = $(addprefix clean-,$(ALL_DIRS))
 COPY_HOLMAKEFILE = $(addprefix copy-holmakefile-,$(ALL_DIRS))
 
 # This allows to customize the INCLUDES variable of the Holmakefile - useful for Nix
+AENEAS_PRIMITIVES ?= ../../backends/hol4
 HOLMAKEFILE_INCLUDES ?= ../../../backends/hol4
 
 .PHONY: all
@@ -24,11 +25,20 @@ copy-holmakefile-%:
 	echo "INCLUDES = " $(HOLMAKEFILE_INCLUDES) >> $*/Holmakefile
 	cat Holmakefile.template >> $*/Holmakefile
 
+# There are racing issues with Holmake: if we run several builds in parallel,
+# Holmake will complain that the dependencies (in `aeneas/backends/hol4` are
+# not built). For this reason, we add this rule which enforces that *one*
+# Holmake process builds the dependencies, before the test subdirectories
+# (hashmap, etc.) are built in parallel.
+.PHONY: verify-primitives
+verify-primitives:
+	cd $(AENEAS_PRIMITIVES) && Holmake
+
 .PHONY: verify
 verify: $(VERIFY_DIRS)
 
 .PHONY: verif-%
-verif-%:
+verif-%: verify-primitives
 	cd $* && Holmake
 
 .PHONY: clean
-- 
cgit v1.2.3