summaryrefslogtreecommitdiff
path: root/tests/hol4/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 /tests/hol4/Makefile
parent435d75174a12a47da84537cc7c9730a0eccf6d1f (diff)
Start setting up the Nix derivation for HOL4
Diffstat (limited to '')
-rw-r--r--tests/hol4/Makefile12
1 files changed, 11 insertions, 1 deletions
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