summaryrefslogtreecommitdiffstats
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile25
1 files changed, 25 insertions, 0 deletions
diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..bb42417
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,25 @@
+COMPCERTRECDIRS := lib common verilog backend cfrontend driver cparser
+COQINCLUDES := -Q . predaware \
+ -R ../vericert/src vericert \
+ $(foreach d, $(COMPCERTRECDIRS), -R ../vericert/lib/CompCert/$(d) compcert.$(d)) \
+ -R ../vericert/lib/CompCert/flocq Flocq \
+ -R ../vericert/lib/CompCert/MenhirLib MenhirLib
+
+COQMAKE := $(COQBIN)coq_makefile
+
+VS := Main.v
+
+all: Makefile.coq _CoqProject
+ $(MAKE) -f Makefile.coq
+
+Makefile.coq _CoqProject: force
+ @echo "COQMAKE Makefile.coq"
+ $(COQMAKE) $(COQINCLUDES) $(VS) -o Makefile.coq
+ echo "$(COQINCLUDES)" >_CoqProject
+
+force:
+
+clean:
+ git clean -dfx
+
+.PHONY: force all clean