|
adam@314
|
1 MODULES_NODOC := CpdtTactics MoreSpecif DepList
|
|
adamc@24
|
2 MODULES_PROSE := Intro
|
|
adam@353
|
3 MODULES_CODE := StackMachine InductiveTypes Predicates Coinductive Subset GeneralRec \
|
|
adam@324
|
4 MoreDep DataStruct Equality Generic Universes LogicProg Match Reflection \
|
|
adam@381
|
5 Large ProgLang
|
|
adam@383
|
6 MODULES_DOC := $(MODULES_PROSE) $(MODULES_CODE) Conclusion
|
|
adamc@3
|
7 MODULES := $(MODULES_NODOC) $(MODULES_DOC)
|
|
adamc@3
|
8 VS := $(MODULES:%=src/%.v)
|
|
adam@311
|
9 TEX := $(MODULES:%=latex/%.v.tex)
|
|
adamc@3
|
10 VS_DOC := $(MODULES_DOC:%=%.v)
|
|
adamc@22
|
11 TEMPLATES := $(MODULES_CODE:%=templates/%.v)
|
|
adamc@2
|
12
|
|
adam@307
|
13 .PHONY: coq clean doc html templates install cpdt.tgz pdf
|
|
adamc@2
|
14
|
|
adamc@2
|
15 coq: Makefile.coq
|
|
adam@305
|
16 $(MAKE) -f Makefile.coq
|
|
adamc@2
|
17
|
|
adamc@2
|
18 Makefile.coq: Makefile $(VS)
|
|
adamc@2
|
19 coq_makefile $(VS) \
|
|
adamc@215
|
20 COQC = "coqc -I src" \
|
|
adamc@89
|
21 COQDEP = "coqdep -I src" \
|
|
adamc@2
|
22 -o Makefile.coq
|
|
adamc@2
|
23
|
|
adamc@2
|
24 clean:: Makefile.coq
|
|
adam@305
|
25 $(MAKE) -f Makefile.coq clean
|
|
adam@311
|
26 rm -f Makefile.coq .depend cpdt.tgz templates/*.v
|
|
adam@320
|
27 cd latex; rm -f *.sty *.log *.aux *.dvi *.v.tex *.toc *.bbl *.blg *.idx *.ilg *.pdf *.ind *.out
|
|
adamc@3
|
28
|
|
adam@306
|
29 doc: latex/cpdt.pdf html
|
|
adamc@3
|
30
|
|
adam@311
|
31 latex/%.v.tex: Makefile src/%.v src/%.glob
|
|
adam@503
|
32 cd src ; coqdoc --interpolate --latex --body-only -s \
|
|
adam@311
|
33 $*.v -o ../latex/$*.v.tex
|
|
adamc@3
|
34
|
|
adam@311
|
35 latex/cpdt.pdf: latex/cpdt.tex $(TEX) latex/cpdt.bib
|
|
adam@311
|
36 cd latex ; pdflatex cpdt ; pdflatex cpdt ; bibtex cpdt ; makeindex cpdt ; pdflatex cpdt ; pdflatex cpdt
|
|
adamc@4
|
37
|
|
adam@306
|
38 latex/%.pdf: latex/%.tex latex/cpdt.bib
|
|
adam@306
|
39 cd latex ; pdflatex $* ; pdflatex $* ; bibtex $* ; makeindex $* ; pdflatex $* ; pdflatex $*
|
|
adamc@8
|
40
|
|
adamc@39
|
41 html: Makefile $(VS) src/toc.html
|
|
adamc@205
|
42 mkdir -p html
|
|
adam@473
|
43 cd src ; coqdoc --interpolate --no-externals $(VS_DOC) \
|
|
adamc@4
|
44 -d ../html
|
|
adamc@39
|
45 cp src/toc.html html/
|
|
adamc@4
|
46
|
|
adamc@22
|
47 templates: $(TEMPLATES)
|
|
adamc@22
|
48
|
|
adamc@41
|
49 templates/%.v: src/%.v tools/make_template.ml
|
|
adamc@22
|
50 ocaml tools/make_template.ml <$< >$@
|
|
adamc@39
|
51
|
|
adamc@39
|
52 cpdt.tgz:
|
|
adamc@39
|
53 hg archive -t tgz $@
|
|
adamc@39
|
54
|
|
adam@517
|
55 cpdtlib.tgz: Makefile
|
|
adam@517
|
56 mkdir -p cpdtlib
|
|
adam@517
|
57 cp src/LICENSE cpdtlib
|
|
adam@517
|
58 cp src/CpdtTactics.v cpdtlib
|
|
adam@517
|
59 cp src/MoreSpecif.v cpdtlib
|
|
adam@517
|
60 cp src/DepList.v cpdtlib
|
|
adam@517
|
61 tar zcf cpdtlib.tgz cpdtlib/*
|
|
adam@517
|
62
|
|
adam@517
|
63 install: cpdt.tgz cpdtlib.tgz latex/cpdt.pdf latex/exercises.pdf html
|
|
adam@517
|
64 cp cpdt*.tgz staging/
|
|
adamc@39
|
65 cp latex/cpdt.pdf staging/
|
|
adam@489
|
66 cp latex/exercises.pdf staging/ex/
|
|
adamc@39
|
67 cp -R html staging/
|
|
adam@307
|
68 rsync -az --exclude '*~' staging/* chlipala.net:sites/chlipala/adam/cpdt/
|
|
adam@307
|
69
|
|
adam@307
|
70 pdf:
|
|
adam@307
|
71 evince latex/cpdt.pdf&
|
|
adam@370
|
72
|
|
adam@370
|
73 latex/exercises.pdf: Makefile src/Exercises.v
|
|
adam@370
|
74 coqc -I src src/Exercises
|
|
adam@370
|
75 coqdoc --latex -s src/Exercises.v -o latex/exercises.tex
|
|
adam@370
|
76 cd latex ; pdflatex exercises
|
