summaryrefslogtreecommitdiff
path: root/tests/coq
diff options
context:
space:
mode:
Diffstat (limited to 'tests/coq')
-rw-r--r--tests/coq/Makefile22
-rw-r--r--tests/coq/betree/Makefile1
-rw-r--r--tests/coq/betree/_CoqProject4
-rw-r--r--tests/coq/hashmap/Makefile1
-rw-r--r--tests/coq/hashmap/_CoqProject6
-rw-r--r--tests/coq/hashmap_on_disk/Makefile1
-rw-r--r--tests/coq/hashmap_on_disk/_CoqProject4
-rw-r--r--tests/coq/misc/Makefile1
-rw-r--r--tests/coq/misc/_CoqProject8
9 files changed, 35 insertions, 13 deletions
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