Speed things up by using arm8/l3-equiv heap

CakeML · Jun 19, 2024 · a2fca1e · a2fca1e
1 parent 80adf6e
commit a2fca1e
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 0 deletions.
diff --git a/examples/lpr_checker/array/compilation/proofsARM8/Holmakefile b/examples/lpr_checker/array/compilation/proofsARM8/Holmakefile
@@ -13,3 +13,9 @@ README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wildcard *Syntax
 DIRS = $(wildcard */)
 README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES)
  $(protect $(CAKEMLDIR)/developers/readme_gen) $(README_SOURCES)
+
+ifdef POLY
+
+HOLHEAP=$(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv/l3-equivalence-heap
+
+endif
diff --git a/examples/pseudo_bool/array/compilation/proofsARM8/Holmakefile b/examples/pseudo_bool/array/compilation/proofsARM8/Holmakefile
@@ -13,3 +13,9 @@ README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wildcard *Syntax
 DIRS = $(wildcard */)
 README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES)
  $(protect $(CAKEMLDIR)/developers/readme_gen) $(README_SOURCES)
+
+ifdef POLY
+
+HOLHEAP=$(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv/l3-equivalence-heap
+
+endif