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 +++++++++++-
 tests/hol4/hashmap/hashmap_PropertiesScript.sml |  9 +++++----
 2 files changed, 16 insertions(+), 5 deletions(-)

(limited to 'tests/hol4')

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
diff --git a/tests/hol4/hashmap/hashmap_PropertiesScript.sml b/tests/hol4/hashmap/hashmap_PropertiesScript.sml
index 6b64affe..c8e87f07 100644
--- a/tests/hol4/hashmap/hashmap_PropertiesScript.sml
+++ b/tests/hol4/hashmap/hashmap_PropertiesScript.sml
@@ -670,8 +670,10 @@ Proof
   case_tac >>
   case_tac >>
   Cases_on ‘hm’ >> fs [] >>
-  fs [hashmap_TypesTheory.recordtype_hash_map_t_seldef_hash_map_slots_fupd_def] >>
-  fs [hashmap_TypesTheory.recordtype_hash_map_t_seldef_hash_map_num_entries_fupd_def]
+  (* Remark: we initially used directly hashmap_TypesTheory.recordtype_hash_map_t_seldef_hash_map_slots_fupd_def
+     and hashmap_TypesTheory.recordtype_hash_map_t_seldef_hash_map_num_entries_fupd_def,
+     but it fails in the Nix derivation *)
+  fs (TypeBase.updates_of “:'a hash_map_t”)
 QED
 val hash_map_insert_no_resize_fwd_back_branches_eq = SIMP_RULE (srw_ss ()) [] hash_map_insert_no_resize_fwd_back_branches_eq
 
@@ -1818,8 +1820,7 @@ Proof
   rw [bind_def] >>
   rpt (case_tac >> fs []) >>
   Cases_on ‘hm’ >> fs [] >>
-  fs [hashmap_TypesTheory.recordtype_hash_map_t_seldef_hash_map_slots_fupd_def,
-      hashmap_TypesTheory.recordtype_hash_map_t_seldef_hash_map_num_entries_fupd_def]
+  fs (TypeBase.updates_of “:'a hash_map_t”)
 QED
 
 (* TODO: this doesn't work very well *)
-- 
cgit v1.2.3