blob: 6900b3dbe7225bb09e41991dd39af5749642e235 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
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
|
