From 2ae43be7b9d4118335c9d2cef6e098f9b9f807fe Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Thu, 9 Feb 2006 14:55:48 +0000
Subject: Initial import of compcert

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 Makefile | 75 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 75 insertions(+)
 create mode 100644 Makefile

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
new file mode 100644
index 00000000..6900b3db
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,75 @@
+COQC=coqc $(INCLUDES)
+COQDEP=coqdep $(INCLUDES)
+COQDOC=coqdoc
+
+INCLUDES=-I lib -I backend
+
+# Files in lib/
+
+LIB=Coqlib.v Maps.v Sets.v union_find.v Inclusion.v Lattice.v Ordered.v \
+  Integers.v Floats.v
+
+# Files in backend/
+
+BACKEND=AST.v Values.v Mem.v Globalenvs.v \
+  Op.v Cminor.v \
+  Cmconstr.v Cmconstrproof.v \
+  Csharpminor.v Cminorgen.v Cminorgenproof.v \
+  Registers.v RTL.v \
+  RTLgen.v RTLgenproof1.v RTLgenproof.v \
+  RTLtyping.v \
+  Kildall.v \
+  Constprop.v Constpropproof.v \
+  CSE.v CSEproof.v \
+  Locations.v Conventions.v LTL.v LTLtyping.v \
+  InterfGraph.v Coloring.v Coloringproof.v \
+  Parallelmove.v Allocation.v \
+  Allocproof_aux.v Allocproof.v \
+  Alloctyping_aux.v Alloctyping.v \
+  Tunneling.v Tunnelingproof.v Tunnelingtyping.v \
+  Linear.v Lineartyping.v \
+  Linearize.v Linearizeproof.v Linearizetyping.v \
+  Mach.v Machabstr.v Machtyping.v \
+  Stacking.v Stackingproof.v Stackingtyping.v \
+  Machabstr2mach.v \
+  PPC.v PPCgen.v PPCgenproof1.v PPCgenproof.v \
+  Main.v
+
+# All source files
+
+FILES=$(LIB:%=lib/%) $(BACKEND:%=backend/%)
+
+FLATFILES=$(LIB) $(BACKEND)
+
+proof: $(FILES:.v=.vo)
+
+all:
+	$(MAKE) proof
+	$(MAKE) -C extraction extraction
+	$(MAKE) -C extraction depend
+	$(MAKE) -C extraction
+
+documentation:
+	$(COQDOC) --html -d doc $(FLATFILES:%.v=--glob-from doc/%.glob) $(FILES)
+	doc/removeproofs doc/lib.*.html doc/backend.*.html
+
+latexdoc:
+	$(COQDOC) --latex -o doc/doc.tex -g $(FILES)
+
+.SUFFIXES: .v .vo
+
+.v.vo:
+	@rm -f doc/glob/$(*F).glob
+	$(COQC) -dump-glob doc/$(*F).glob $*.v
+
+depend:
+	$(COQDEP) $(FILES) > .depend
+
+clean:
+	rm -f */*.vo *~ */*~
+	rm -f doc/lib.*.html doc/backend.*.html doc/*.glob
+	$(MAKE) -C extraction clean
+	$(MAKE) -C test/cminor clean
+
+include .depend
+
-- 
cgit