|
adamc@78
|
1 MODULES_NODOC := Tactics MoreSpecif
|
|
adamc@24
|
2 MODULES_PROSE := Intro
|
|
adamc@83
|
3 MODULES_CODE := StackMachine InductiveTypes Predicates Coinductive Subset MoreDep
|
|
adamc@22
|
4 MODULES_DOC := $(MODULES_PROSE) $(MODULES_CODE)
|
|
adamc@3
|
5 MODULES := $(MODULES_NODOC) $(MODULES_DOC)
|
|
adamc@3
|
6 VS := $(MODULES:%=src/%.v)
|
|
adamc@3
|
7 VS_DOC := $(MODULES_DOC:%=%.v)
|
|
adamc@3
|
8 GLOBALS := .coq_globals
|
|
adamc@22
|
9 TEMPLATES := $(MODULES_CODE:%=templates/%.v)
|
|
adamc@2
|
10
|
|
adamc@42
|
11 .PHONY: coq clean doc dvi html templates install cpdt.tgz
|
|
adamc@2
|
12
|
|
adamc@2
|
13 coq: Makefile.coq
|
|
adamc@2
|
14 make -f Makefile.coq
|
|
adamc@2
|
15
|
|
adamc@2
|
16 Makefile.coq: Makefile $(VS)
|
|
adamc@2
|
17 coq_makefile $(VS) \
|
|
adamc@3
|
18 COQC = "coqc -I src -impredicative-set \
|
|
adamc@3
|
19 -dump-glob $(GLOBALS)" \
|
|
adamc@2
|
20 -o Makefile.coq
|
|
adamc@2
|
21
|
|
adamc@2
|
22 clean:: Makefile.coq
|
|
adamc@2
|
23 make -f Makefile.coq clean
|
|
adamc@49
|
24 rm -f Makefile.coq .depend $(GLOBALS) cpdt.tgz \
|
|
adamc@22
|
25 latex/*.sty latex/cpdt.* templates/*.v
|
|
adamc@3
|
26
|
|
adamc@8
|
27 doc: latex/cpdt.dvi latex/cpdt.pdf html
|
|
adamc@3
|
28
|
|
adamc@21
|
29 latex/cpdt.tex: Makefile $(VS)
|
|
adamc@25
|
30 cd src ; coqdoc --latex -s $(VS_DOC) \
|
|
adamc@21
|
31 -p "\usepackage{url}" \
|
|
adamc@21
|
32 -p "\title{Certified Programming with Dependent Types}" \
|
|
adamc@21
|
33 -p "\author{Adam Chlipala}" \
|
|
adamc@21
|
34 -p "\iffalse" \
|
|
adamc@3
|
35 -o ../latex/cpdt.tex
|
|
adamc@3
|
36
|
|
adamc@3
|
37 latex/cpdt.dvi: latex/cpdt.tex
|
|
adamc@5
|
38 cd latex ; latex cpdt ; latex cpdt
|
|
adamc@4
|
39
|
|
adamc@8
|
40 latex/cpdt.pdf: latex/cpdt.dvi
|
|
adamc@8
|
41 cd latex ; pdflatex cpdt
|
|
adamc@8
|
42
|
|
adamc@39
|
43 html: Makefile $(VS) src/toc.html
|
|
adamc@39
|
44 cd src ; coqdoc $(VS_DOC) \
|
|
adamc@4
|
45 --glob-from ../$(GLOBALS) \
|
|
adamc@4
|
46 -d ../html
|
|
adamc@39
|
47 cp src/toc.html html/
|
|
adamc@4
|
48
|
|
adamc@4
|
49 dvi:
|
|
adamc@4
|
50 xdvi latex/cpdt
|
|
adamc@22
|
51
|
|
adamc@22
|
52 templates: $(TEMPLATES)
|
|
adamc@22
|
53
|
|
adamc@41
|
54 templates/%.v: src/%.v tools/make_template.ml
|
|
adamc@22
|
55 ocaml tools/make_template.ml <$< >$@
|
|
adamc@39
|
56
|
|
adamc@39
|
57 cpdt.tgz:
|
|
adamc@39
|
58 hg archive -t tgz $@
|
|
adamc@39
|
59
|
|
adamc@39
|
60 install: cpdt.tgz latex/cpdt.pdf html
|
|
adamc@39
|
61 cp cpdt.tgz staging/
|
|
adamc@39
|
62 cp latex/cpdt.pdf staging/
|
|
adamc@39
|
63 cp -R html staging/
|
|
adamc@69
|
64 rsync -az --exclude '*~' staging/* bowser.eecs.harvard.edu:public_html/cpdt/book/
|
|
adamc@39
|
65 rsync -az --exclude '*~' staging/* ssh.hcoop.net:sites/chlipala/adam/cpdt/
|
