|
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) \
|
|
adam@534
|
20 COQC = "coqc -R src Cpdt" \
|
|
adam@534
|
21 COQDEP = "coqdep -R src Cpdt" \
|
|
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@536
|
31 COQDOC = coqdoc -R . Cpdt
|
|
adam@536
|
32
|
|
adam@311
|
33 latex/%.v.tex: Makefile src/%.v src/%.glob
|
|
adam@536
|
34 cd src ; $(COQDOC) --interpolate --latex --body-only -s \
|
|
adam@311
|
35 $*.v -o ../latex/$*.v.tex
|
|
adamc@3
|
36
|
|
adam@311
|
37 latex/cpdt.pdf: latex/cpdt.tex $(TEX) latex/cpdt.bib
|
|
adam@311
|
38 cd latex ; pdflatex cpdt ; pdflatex cpdt ; bibtex cpdt ; makeindex cpdt ; pdflatex cpdt ; pdflatex cpdt
|
|
adamc@4
|
39
|
|
adam@306
|
40 latex/%.pdf: latex/%.tex latex/cpdt.bib
|
|
adam@306
|
41 cd latex ; pdflatex $* ; pdflatex $* ; bibtex $* ; makeindex $* ; pdflatex $* ; pdflatex $*
|
|
adamc@8
|
42
|
|
adamc@39
|
43 html: Makefile $(VS) src/toc.html
|
|
adamc@205
|
44 mkdir -p html
|
|
adam@536
|
45 cd src ; $(COQDOC) --interpolate --no-externals $(VS_DOC) \
|
|
adamc@4
|
46 -d ../html
|
|
adamc@39
|
47 cp src/toc.html html/
|
|
adamc@4
|
48
|
|
adamc@22
|
49 templates: $(TEMPLATES)
|
|
adamc@22
|
50
|
|
adamc@41
|
51 templates/%.v: src/%.v tools/make_template.ml
|
|
adamc@22
|
52 ocaml tools/make_template.ml <$< >$@
|
|
adamc@39
|
53
|
|
adamc@39
|
54 cpdt.tgz:
|
|
adamc@39
|
55 hg archive -t tgz $@
|
|
adamc@39
|
56
|
|
adam@517
|
57 cpdtlib.tgz: Makefile
|
|
adam@517
|
58 mkdir -p cpdtlib
|
|
adam@517
|
59 cp src/LICENSE cpdtlib
|
|
amp@546
|
60 # Generate specifically BSD licenced versions of the lib files.
|
|
amp@546
|
61 ocaml tools/bsd_license.ml < src/CpdtTactics.v > cpdtlib/CpdtTactics.v
|
|
amp@546
|
62 ocaml tools/bsd_license.ml < src/MoreSpecif.v > cpdtlib/MoreSpecif.v
|
|
amp@546
|
63 ocaml tools/bsd_license.ml < src/DepList.v > cpdtlib/DepList.v
|
|
adam@517
|
64 tar zcf cpdtlib.tgz cpdtlib/*
|
|
adam@517
|
65
|
|
adam@517
|
66 install: cpdt.tgz cpdtlib.tgz latex/cpdt.pdf latex/exercises.pdf html
|
|
adam@517
|
67 cp cpdt*.tgz staging/
|
|
adamc@39
|
68 cp latex/cpdt.pdf staging/
|
|
adam@489
|
69 cp latex/exercises.pdf staging/ex/
|
|
adamc@39
|
70 cp -R html staging/
|
|
adam@307
|
71 rsync -az --exclude '*~' staging/* chlipala.net:sites/chlipala/adam/cpdt/
|
|
adam@307
|
72
|
|
adam@307
|
73 pdf:
|
|
adam@307
|
74 evince latex/cpdt.pdf&
|
|
adam@370
|
75
|
|
adam@370
|
76 latex/exercises.pdf: Makefile src/Exercises.v
|
|
adam@538
|
77 coqc -R src Cpdt src/Exercises
|
|
adam@538
|
78 $(COQDOC) --latex -s src/Exercises.v -o latex/exercises.tex
|
|
adam@370
|
79 cd latex ; pdflatex exercises
|
