|
adam@297
|
1 MODULES_NODOC := Tactics MoreSpecif DepList
|
|
adamc@24
|
2 MODULES_PROSE := Intro
|
|
adamc@105
|
3 MODULES_CODE := StackMachine InductiveTypes Predicates Coinductive Subset \
|
|
adamc@227
|
4 MoreDep DataStruct Equality Generic Universes Match Reflection \
|
|
adamc@265
|
5 Large Firstorder DeBruijn Hoas Interps Extensional Intensional OpSem
|
|
adamc@22
|
6 MODULES_DOC := $(MODULES_PROSE) $(MODULES_CODE)
|
|
adamc@3
|
7 MODULES := $(MODULES_NODOC) $(MODULES_DOC)
|
|
adamc@3
|
8 VS := $(MODULES:%=src/%.v)
|
|
adamc@3
|
9 VS_DOC := $(MODULES_DOC:%=%.v)
|
|
adamc@22
|
10 TEMPLATES := $(MODULES_CODE:%=templates/%.v)
|
|
adamc@2
|
11
|
|
adam@307
|
12 .PHONY: coq clean doc html templates install cpdt.tgz pdf
|
|
adamc@2
|
13
|
|
adamc@2
|
14 coq: Makefile.coq
|
|
adam@305
|
15 $(MAKE) -f Makefile.coq
|
|
adamc@2
|
16
|
|
adamc@2
|
17 Makefile.coq: Makefile $(VS)
|
|
adamc@2
|
18 coq_makefile $(VS) \
|
|
adamc@215
|
19 COQC = "coqc -I src" \
|
|
adamc@89
|
20 COQDEP = "coqdep -I src" \
|
|
adamc@2
|
21 -o Makefile.coq
|
|
adamc@2
|
22
|
|
adamc@2
|
23 clean:: Makefile.coq
|
|
adam@305
|
24 $(MAKE) -f Makefile.coq clean
|
|
adamc@215
|
25 rm -f Makefile.coq .depend cpdt.tgz \
|
|
adamc@22
|
26 latex/*.sty latex/cpdt.* templates/*.v
|
|
adam@306
|
27 rm -f *.aux *.log
|
|
adamc@3
|
28
|
|
adam@306
|
29 doc: latex/cpdt.pdf html
|
|
adamc@3
|
30
|
|
adam@306
|
31 latex/cpdt.tex: Makefile $(VS) src/BackMatter.v latex/cpdt.bib
|
|
adam@306
|
32 cd src ; coqdoc --interpolate --latex -s $(VS_DOC) BackMatter.v \
|
|
adam@306
|
33 -p "\usepackage{url}" \
|
|
adamc@21
|
34 -p "\iffalse" \
|
|
adamc@3
|
35 -o ../latex/cpdt.tex
|
|
adamc@3
|
36
|
|
adam@284
|
37 latex/%.tex: src/%.v src/%.glob
|
|
adam@302
|
38 cd src ; coqdoc --interpolate --latex \
|
|
adam@306
|
39 -p "\usepackage{url}" \
|
|
adam@282
|
40 $*.v -o ../latex/$*.tex
|
|
adamc@4
|
41
|
|
adam@306
|
42 latex/%.pdf: latex/%.tex latex/cpdt.bib
|
|
adam@306
|
43 cd latex ; pdflatex $* ; pdflatex $* ; bibtex $* ; makeindex $* ; pdflatex $* ; pdflatex $*
|
|
adamc@8
|
44
|
|
adamc@39
|
45 html: Makefile $(VS) src/toc.html
|
|
adamc@205
|
46 mkdir -p html
|
|
adamc@206
|
47 cd src ; coqdoc --interpolate $(VS_DOC) \
|
|
adamc@4
|
48 -d ../html
|
|
adamc@39
|
49 cp src/toc.html html/
|
|
adamc@4
|
50
|
|
adamc@22
|
51 templates: $(TEMPLATES)
|
|
adamc@22
|
52
|
|
adamc@41
|
53 templates/%.v: src/%.v tools/make_template.ml
|
|
adamc@22
|
54 ocaml tools/make_template.ml <$< >$@
|
|
adamc@39
|
55
|
|
adamc@39
|
56 cpdt.tgz:
|
|
adamc@39
|
57 hg archive -t tgz $@
|
|
adamc@39
|
58
|
|
adamc@39
|
59 install: cpdt.tgz latex/cpdt.pdf html
|
|
adamc@39
|
60 cp cpdt.tgz staging/
|
|
adamc@39
|
61 cp latex/cpdt.pdf staging/
|
|
adamc@39
|
62 cp -R html staging/
|
|
adam@307
|
63 rsync -az --exclude '*~' staging/* chlipala.net:sites/chlipala/adam/cpdt/
|
|
adam@307
|
64
|
|
adam@307
|
65 pdf:
|
|
adam@307
|
66 evince latex/cpdt.pdf&
|
