remove Holmakefile.gen and replace with CakeML style Holmakefile

kth-step · Feb 16, 2024 · 8044597 · 8044597
1 parent d65e127
commit 8044597
Show file tree

Hide file tree

Showing 90 changed files with 224 additions and 761 deletions.
diff --git a/.gitignore b/.gitignore
@@ -10,9 +10,6 @@
 *.exe
 *-heap
 
-# Generated Holmake files
-Holmakefile
-
 # Makefile related stuff
 Makefile.local
 holba-tests.log

diff --git a/.holpath b/.holpath
@@ -0,0 +1 @@
+HOLBADIR
diff --git a/src/Holmakefile.gen b/src/Holmakefile.gen
diff --git a/src/Holmakefile.inc b/src/Holmakefile.inc
diff --git a/src/aux/Holmakefile b/src/aux/Holmakefile
@@ -0,0 +1,4 @@
+INCLUDES = 
+
+all: $(DEFAULT_TARGETS)
+.PHONY: all
diff --git a/src/aux/Holmakefile.gen b/src/aux/Holmakefile.gen
diff --git a/src/shared/HolSmt/Holmakefile b/src/shared/HolSmt/Holmakefile
@@ -0,0 +1,4 @@
+INCLUDES = 
+
+all: $(DEFAULT_TARGETS)
+.PHONY: all
diff --git a/src/shared/HolSmt/Holmakefile.gen b/src/shared/HolSmt/Holmakefile.gen
diff --git a/src/shared/Holmakefile b/src/shared/Holmakefile
@@ -0,0 +1,7 @@
+INCLUDES = $(HOLBADIR)/src/theory/bir \
+           $(HOLBADIR)/src/theory/bir-support \
+           $(HOLBADIR)/src/shared/HolSmt \
+           $(HOLBADIR)/src/shared/sml-simplejson
+
+all: $(DEFAULT_TARGETS)
+.PHONY: all
diff --git a/src/shared/Holmakefile.gen b/src/shared/Holmakefile.gen
diff --git a/src/shared/examples/Holmakefile b/src/shared/examples/Holmakefile
@@ -0,0 +1,4 @@
+INCLUDES = 
+
+all: $(DEFAULT_TARGETS)
+.PHONY: all
diff --git a/src/shared/examples/Holmakefile.gen b/src/shared/examples/Holmakefile.gen
diff --git a/src/theory/Holmakefile.gen b/src/theory/Holmakefile.gen
diff --git a/src/theory/bir-support/Holmakefile b/src/theory/bir-support/Holmakefile
@@ -0,0 +1,4 @@
+INCLUDES = $(HOLBADIR)/src/theory/bir
+
+all: $(DEFAULT_TARGETS)
+.PHONY: all
diff --git a/src/theory/bir-support/Holmakefile.gen b/src/theory/bir-support/Holmakefile.gen
diff --git a/src/theory/bir/Holmakefile b/src/theory/bir/Holmakefile
@@ -0,0 +1,4 @@
+INCLUDES = $(HOLBADIR)/src/aux
+
+all: $(DEFAULT_TARGETS)
+.PHONY: all
diff --git a/src/theory/bir/Holmakefile.gen b/src/theory/bir/Holmakefile.gen
diff --git a/src/theory/models/Holmakefile.gen b/src/theory/models/Holmakefile.gen
diff --git a/src/theory/models/l3/Holmakefile.gen b/src/theory/models/l3/Holmakefile.gen
diff --git a/src/theory/models/l3/README b/src/theory/models/l3/README
diff --git a/src/theory/models/l3mod/Holmakefile b/src/theory/models/l3mod/Holmakefile
@@ -0,0 +1,6 @@
+INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
+           $(HOLDIR)/examples/l3-machine-code/m0/model \
+           $(HOLDIR)/examples/l3-machine-code/m0/step
+
+all: $(DEFAULT_TARGETS)
+.PHONY: all
diff --git a/src/theory/models/l3mod/Holmakefile.gen b/src/theory/models/l3mod/Holmakefile.gen
diff --git a/src/theory/models/l3mod/m0_mod_stepScript.sml b/src/theory/models/l3mod/m0_mod_stepScript.sml
@@ -4,6 +4,9 @@ open arithmeticTheory;
 open wordsTheory;
 open combinTheory;
 
+open m0Theory m0_stepTheory;
+open m0_stepLib;
+
 (* This theory contains the definition of the modified m0 step
    (, where clock cycles are counted with word64 instead if num). *)
 

diff --git a/src/theory/program_logic/Holmakefile b/src/theory/program_logic/Holmakefile
@@ -0,0 +1,4 @@
+INCLUDES = $(HOLBADIR)/src/aux
+
+all: $(DEFAULT_TARGETS)
+.PHONY: all
diff --git a/src/theory/program_logic/Holmakefile.gen b/src/theory/program_logic/Holmakefile.gen
diff --git a/src/theory/tools/Holmakefile.gen b/src/theory/tools/Holmakefile.gen
diff --git a/src/theory/tools/backlifter/Holmakefile b/src/theory/tools/backlifter/Holmakefile
@@ -0,0 +1,9 @@
+INCLUDES = $(HOLBADIR)/src/theory/bir \
+           $(HOLBADIR)/src/theory/bir-support \
+           $(HOLBADIR)/src/theory/program_logic \
+           $(HOLBADIR)/src/theory/models/l3mod \
+           $(HOLBADIR)/src/theory/tools/lifter \
+           $(HOLBADIR)/src/theory/tools/comp
+
+all: $(DEFAULT_TARGETS)
+.PHONY: all
diff --git a/src/theory/tools/backlifter/Holmakefile.gen b/src/theory/tools/backlifter/Holmakefile.gen
diff --git a/src/theory/tools/backlifter/bir_backlifterScript.sml b/src/theory/tools/backlifter/bir_backlifterScript.sml
@@ -20,6 +20,8 @@ open program_logicSimps;
 
 open bir_auxiliaryLib;
 
+open m0_mod_stepLib;
+
 val _ = new_theory "bir_backlifter";
 
 (* This part should be generalized *)

diff --git a/src/theory/tools/comp/Holmakefile b/src/theory/tools/comp/Holmakefile
@@ -0,0 +1,7 @@
+INCLUDES = $(HOLBADIR)/src/theory/bir \
+           $(HOLBADIR)/src/theory/bir-support \
+           $(HOLBADIR)/src/theory/program_logic \
+           $(HOLBADIR)/src/theory/tools/wp
+
+all: $(DEFAULT_TARGETS)
+.PHONY: all