aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
diff options
context:
space:
mode:
authorLibravatar Rutger Broekhoff2024-06-26 20:50:18 +0200
committerLibravatar Rutger Broekhoff2024-06-26 20:50:18 +0200
commit73df1945b31c0beee88cf4476df4ccd09d31403b (patch)
treeed00db26b711442e643f38b66888a3df56e33ebd /Makefile
downloadmininix-formalization-73df1945b31c0beee88cf4476df4ccd09d31403b.tar.gz
mininix-formalization-73df1945b31c0beee88cf4476df4ccd09d31403b.zip
Import Coq project
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile20
1 files changed, 20 insertions, 0 deletions
diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..1e32cef
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,20 @@
1# Modified from the Logical Foundations Makefile
2
3COQMFFLAGS := -Q . mininix
4
5ALLVFILES := maptools.v relations.v expr.v shared.v binop.v matching.v sem.v \
6 interpreter.v complete.v sound.v correct.v semprop.v
7
8build: Makefile.coq
9 $(MAKE) -f Makefile.coq
10
11clean::
12 if [ -e Makefile.coq ]; then $(MAKE) -f Makefile.coq cleanall; fi
13 $(RM) $(wildcard Makefile.coq Makefile.coq.conf)
14
15Makefile.coq:
16 coq_makefile $(COQMFFLAGS) -o Makefile.coq $(ALLVFILES)
17
18-include Makefile.coq
19
20.PHONY: build clean