From a20819f170acc6aad7b5aca2fbe53c7b3ab7e2b8 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 16 Nov 2022 14:40:34 +0100
Subject: Automatically generate the Makefile and _CoqProject files in the
 tests subdirectories

---
 tests/coq/Makefile                        | 22 ++++++++++++++++++++--
 tests/coq/betree/Makefile                 |  1 +
 tests/coq/betree/_CoqProject              |  4 ++--
 tests/coq/hashmap/Makefile                |  1 +
 tests/coq/hashmap/_CoqProject             |  6 +++---
 tests/coq/hashmap_on_disk/Makefile        |  1 +
 tests/coq/hashmap_on_disk/_CoqProject     |  4 ++--
 tests/coq/misc/Makefile                   |  1 +
 tests/coq/misc/_CoqProject                |  8 ++++----
 tests/fstar/Makefile                      | 10 +++++++++-
 tests/fstar/Makefile.template             |  3 ++-
 tests/fstar/betree/Makefile               |  1 +
 tests/fstar/betree_back_stateful/Makefile |  1 +
 tests/fstar/hashmap/Makefile              |  1 +
 tests/fstar/hashmap_on_disk/Makefile      |  1 +
 tests/fstar/misc/Makefile                 |  1 +
 16 files changed, 51 insertions(+), 15 deletions(-)

(limited to 'tests')

diff --git a/tests/coq/Makefile b/tests/coq/Makefile
index a9c170f7..8dee394b 100644
--- a/tests/coq/Makefile
+++ b/tests/coq/Makefile
@@ -1,11 +1,15 @@
-ALL_DIRS ?= $(filter-out Makefile%, $(wildcard *))
+ALL_DIRS ?= $(filter-out %.template, $(filter-out Makefile%, $(wildcard *)))
 
 VERIFY_DIRS = $(addprefix verif-,$(ALL_DIRS))
 
 CLEAN_DIRS = $(addprefix clean-,$(ALL_DIRS))
 
+COPY_MAKEFILES = $(addprefix copy-makefile-,$(ALL_DIRS))
+
+GEN_COQ_PROJECT = $(addprefix gen-coq-project-,$(ALL_DIRS))
+
 .PHONY: all
-all: $(VERIFY_DIRS)
+all: $(COPY_MAKEFILES) $(GEN_COQ_PROJECT) $(VERIFY_DIRS)
 
 .PHONY: clean
 clean: $(CLEAN_DIRS)
@@ -14,6 +18,20 @@ clean: $(CLEAN_DIRS)
 verif-%:
 	cd $* && make all
 
+.PHONY: copy-makefile-%
+copy-makefile-%:
+	rm -f $*/Makefile
+	echo "# This file was automatically generated - modify ../Makefile.template instead" >> $*/Makefile
+	cat Makefile.template >> $*/Makefile
+
+.PHONY: gen-coq-project-%
+gen-coq-project-%:
+	rm -f $*/_CoqProject
+	echo "# This file was automatically generated - see ../Makefile" >> $*/_CoqProject
+	cat _CoqProject.template >> $*/_CoqProject
+	echo $(patsubst $*/%,"\n"%,$(wildcard $*/*.v)) >> $*/_CoqProject
+	sed -i -z "s/ \n/\n/g" $*/_CoqProject
+
 .PHONY: clean-%
 clean-%:
 	cd $* && make clean
diff --git a/tests/coq/betree/Makefile b/tests/coq/betree/Makefile
index ff1ccd39..1a5aee4a 100644
--- a/tests/coq/betree/Makefile
+++ b/tests/coq/betree/Makefile
@@ -1,3 +1,4 @@
+# This file was automatically generated - modify ../Makefile.template instead
 # Makefile originally taken from coq-club
 
 %: Makefile.coq phony
diff --git a/tests/coq/betree/_CoqProject b/tests/coq/betree/_CoqProject
index 3cf45746..42c62421 100644
--- a/tests/coq/betree/_CoqProject
+++ b/tests/coq/betree/_CoqProject
@@ -1,9 +1,9 @@
+# This file was automatically generated - see ../Makefile
 -R . Lib
 -arg -w
 -arg all
 
+BetreeMain_Types.v
 Primitives.v
-
 BetreeMain_Funs.v
 BetreeMain_Opaque.v
-BetreeMain_Types.v
\ No newline at end of file
diff --git a/tests/coq/hashmap/Makefile b/tests/coq/hashmap/Makefile
index ff1ccd39..1a5aee4a 100644
--- a/tests/coq/hashmap/Makefile
+++ b/tests/coq/hashmap/Makefile
@@ -1,3 +1,4 @@
+# This file was automatically generated - modify ../Makefile.template instead
 # Makefile originally taken from coq-club
 
 %: Makefile.coq phony
diff --git a/tests/coq/hashmap/_CoqProject b/tests/coq/hashmap/_CoqProject
index 94708adc..7f80afbf 100644
--- a/tests/coq/hashmap/_CoqProject
+++ b/tests/coq/hashmap/_CoqProject
@@ -1,8 +1,8 @@
+# This file was automatically generated - see ../Makefile
 -R . Lib
 -arg -w
 -arg all
 
-Primitives.v
-
 Hashmap_Types.v
-Hashmap_Funs.v
\ No newline at end of file
+Primitives.v
+Hashmap_Funs.v
diff --git a/tests/coq/hashmap_on_disk/Makefile b/tests/coq/hashmap_on_disk/Makefile
index ff1ccd39..1a5aee4a 100644
--- a/tests/coq/hashmap_on_disk/Makefile
+++ b/tests/coq/hashmap_on_disk/Makefile
@@ -1,3 +1,4 @@
+# This file was automatically generated - modify ../Makefile.template instead
 # Makefile originally taken from coq-club
 
 %: Makefile.coq phony
diff --git a/tests/coq/hashmap_on_disk/_CoqProject b/tests/coq/hashmap_on_disk/_CoqProject
index 95b82c41..b78c7b5f 100644
--- a/tests/coq/hashmap_on_disk/_CoqProject
+++ b/tests/coq/hashmap_on_disk/_CoqProject
@@ -1,9 +1,9 @@
+# This file was automatically generated - see ../Makefile
 -R . Lib
 -arg -w
 -arg all
 
+HashmapMain_Types.v
 Primitives.v
-
 HashmapMain_Funs.v
 HashmapMain_Opaque.v
-HashmapMain_Types.v
\ No newline at end of file
diff --git a/tests/coq/misc/Makefile b/tests/coq/misc/Makefile
index ff1ccd39..1a5aee4a 100644
--- a/tests/coq/misc/Makefile
+++ b/tests/coq/misc/Makefile
@@ -1,3 +1,4 @@
+# This file was automatically generated - modify ../Makefile.template instead
 # Makefile originally taken from coq-club
 
 %: Makefile.coq phony
diff --git a/tests/coq/misc/_CoqProject b/tests/coq/misc/_CoqProject
index b8590272..c9ee0ff6 100644
--- a/tests/coq/misc/_CoqProject
+++ b/tests/coq/misc/_CoqProject
@@ -1,13 +1,13 @@
+# This file was automatically generated - see ../Makefile
 -R . Lib
 -arg -w
 -arg all
 
 Primitives.v
-
-Constants.v
 External_Funs.v
-External_Opaque.v
+Constants.v
+PoloniusList.v
 External_Types.v
 NoNestedBorrows.v
+External_Opaque.v
 Paper.v
-PoloniusList.v
\ No newline at end of file
diff --git a/tests/fstar/Makefile b/tests/fstar/Makefile
index a9c170f7..aad3354e 100644
--- a/tests/fstar/Makefile
+++ b/tests/fstar/Makefile
@@ -4,8 +4,10 @@ VERIFY_DIRS = $(addprefix verif-,$(ALL_DIRS))
 
 CLEAN_DIRS = $(addprefix clean-,$(ALL_DIRS))
 
+COPY_MAKEFILES = $(addprefix copy-makefile-,$(ALL_DIRS))
+
 .PHONY: all
-all: $(VERIFY_DIRS)
+all: $(COPY_MAKEFILES) $(VERIFY_DIRS)
 
 .PHONY: clean
 clean: $(CLEAN_DIRS)
@@ -14,6 +16,12 @@ clean: $(CLEAN_DIRS)
 verif-%:
 	cd $* && make all
 
+.PHONY: copy-makefile-%
+copy-makefile-%:
+	rm -f $*/Makefile
+	echo "# This file was automatically generated - modify ../Makefile.template instead" >> $*/Makefile
+	cat Makefile.template >> $*/Makefile
+
 .PHONY: clean-%
 clean-%:
 	cd $* && make clean
diff --git a/tests/fstar/Makefile.template b/tests/fstar/Makefile.template
index a16b0edb..14790d6d 100644
--- a/tests/fstar/Makefile.template
+++ b/tests/fstar/Makefile.template
@@ -8,7 +8,8 @@ FSTAR_OPTIONS = $(FSTAR_HINTS) \
   --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
   --warn_error '+241@247+285-274' \
 
-FSTAR_NO_FLAGS = fstar.exe --already_cached 'Prims FStar LowStar Steel' --odir obj --cache_dir obj
+FSTAR_EXE ?= fstar.exe
+FSTAR_NO_FLAGS = $(FSTAR_EXE) --already_cached 'Prims FStar LowStar Steel' --odir obj --cache_dir obj
 
 FSTAR = $(FSTAR_NO_FLAGS) $(FSTAR_OPTIONS)
 
diff --git a/tests/fstar/betree/Makefile b/tests/fstar/betree/Makefile
index 14790d6d..fa7d1f36 100644
--- a/tests/fstar/betree/Makefile
+++ b/tests/fstar/betree/Makefile
@@ -1,3 +1,4 @@
+# This file was automatically generated - modify ../Makefile.template instead
 INCLUDE_DIRS = .
 
 FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS))
diff --git a/tests/fstar/betree_back_stateful/Makefile b/tests/fstar/betree_back_stateful/Makefile
index 14790d6d..fa7d1f36 100644
--- a/tests/fstar/betree_back_stateful/Makefile
+++ b/tests/fstar/betree_back_stateful/Makefile
@@ -1,3 +1,4 @@
+# This file was automatically generated - modify ../Makefile.template instead
 INCLUDE_DIRS = .
 
 FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS))
diff --git a/tests/fstar/hashmap/Makefile b/tests/fstar/hashmap/Makefile
index 14790d6d..fa7d1f36 100644
--- a/tests/fstar/hashmap/Makefile
+++ b/tests/fstar/hashmap/Makefile
@@ -1,3 +1,4 @@
+# This file was automatically generated - modify ../Makefile.template instead
 INCLUDE_DIRS = .
 
 FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS))
diff --git a/tests/fstar/hashmap_on_disk/Makefile b/tests/fstar/hashmap_on_disk/Makefile
index 14790d6d..fa7d1f36 100644
--- a/tests/fstar/hashmap_on_disk/Makefile
+++ b/tests/fstar/hashmap_on_disk/Makefile
@@ -1,3 +1,4 @@
+# This file was automatically generated - modify ../Makefile.template instead
 INCLUDE_DIRS = .
 
 FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS))
diff --git a/tests/fstar/misc/Makefile b/tests/fstar/misc/Makefile
index 14790d6d..fa7d1f36 100644
--- a/tests/fstar/misc/Makefile
+++ b/tests/fstar/misc/Makefile
@@ -1,3 +1,4 @@
+# This file was automatically generated - modify ../Makefile.template instead
 INCLUDE_DIRS = .
 
 FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS))
-- 
cgit v1.2.3