|
adamc@3
|
1 MODULES_NODOC := Tactics
|
|
adamc@4
|
2 MODULES_DOC := Intro StackMachine
|
|
adamc@3
|
3 MODULES := $(MODULES_NODOC) $(MODULES_DOC)
|
|
adamc@3
|
4 VS := $(MODULES:%=src/%.v)
|
|
adamc@3
|
5 VS_DOC := $(MODULES_DOC:%=%.v)
|
|
adamc@3
|
6 GLOBALS := .coq_globals
|
|
adamc@2
|
7
|
|
adamc@4
|
8 .PHONY: coq clean doc dvi html
|
|
adamc@2
|
9
|
|
adamc@2
|
10 coq: Makefile.coq
|
|
adamc@2
|
11 make -f Makefile.coq
|
|
adamc@2
|
12
|
|
adamc@2
|
13 Makefile.coq: Makefile $(VS)
|
|
adamc@2
|
14 coq_makefile $(VS) \
|
|
adamc@3
|
15 COQC = "coqc -I src -impredicative-set \
|
|
adamc@3
|
16 -dump-glob $(GLOBALS)" \
|
|
adamc@2
|
17 -o Makefile.coq
|
|
adamc@2
|
18
|
|
adamc@2
|
19 clean:: Makefile.coq
|
|
adamc@2
|
20 make -f Makefile.coq clean
|
|
adamc@3
|
21 rm -f Makefile.coq .depend $(GLOBALS) \
|
|
adamc@3
|
22 latex/*.sty latex/cpdt.*
|
|
adamc@3
|
23
|
|
adamc@8
|
24 doc: latex/cpdt.dvi latex/cpdt.pdf html
|
|
adamc@3
|
25
|
|
adamc@3
|
26 latex/cpdt.tex: $(VS)
|
|
adamc@3
|
27 cd src ; coqdoc --latex $(VS_DOC) \
|
|
adamc@5
|
28 -p "\usepackage{url}" -toc \
|
|
adamc@3
|
29 -o ../latex/cpdt.tex
|
|
adamc@3
|
30
|
|
adamc@3
|
31 latex/cpdt.dvi: latex/cpdt.tex
|
|
adamc@5
|
32 cd latex ; latex cpdt ; latex cpdt
|
|
adamc@4
|
33
|
|
adamc@8
|
34 latex/cpdt.pdf: latex/cpdt.dvi
|
|
adamc@8
|
35 cd latex ; pdflatex cpdt
|
|
adamc@8
|
36
|
|
adamc@4
|
37 html: $(VS)
|
|
adamc@5
|
38 cd src ; coqdoc $(VS_DOC) -toc \
|
|
adamc@4
|
39 --glob-from ../$(GLOBALS) \
|
|
adamc@4
|
40 -d ../html
|
|
adamc@4
|
41
|
|
adamc@4
|
42 dvi:
|
|
adamc@4
|
43 xdvi latex/cpdt
|
