Makefile 2.09 KB
Newer Older
1
MODULES_NODOC := CpdtTactics MoreSpecif DepList
2
MODULES_PROSE := Intro
3
MODULES_CODE  := StackMachine InductiveTypes Predicates Coinductive Subset GeneralRec \
Adam Chlipala's avatar
Adam Chlipala committed
4
	MoreDep DataStruct Equality Generic Universes LogicProg Match Reflection \
Adam Chlipala's avatar
Adam Chlipala committed
5
	Large ProgLang
Adam Chlipala's avatar
Adam Chlipala committed
6
MODULES_DOC   := $(MODULES_PROSE) $(MODULES_CODE) Conclusion
Adam Chlipala's avatar
Adam Chlipala committed
7 8
MODULES       := $(MODULES_NODOC) $(MODULES_DOC)
VS            := $(MODULES:%=src/%.v)
9
TEX           := $(MODULES:%=latex/%.v.tex)
Adam Chlipala's avatar
Adam Chlipala committed
10
VS_DOC        := $(MODULES_DOC:%=%.v)
Adam Chlipala's avatar
Adam Chlipala committed
11
TEMPLATES     := $(MODULES_CODE:%=templates/%.v)
12

13
.PHONY: coq clean doc html templates install cpdt.tgz pdf
14 15

coq: Makefile.coq
16
	$(MAKE) -f Makefile.coq
17 18 19

Makefile.coq: Makefile $(VS)
	coq_makefile $(VS) \
Adam Chlipala's avatar
Adam Chlipala committed
20
		COQC = "coqc -I src" \
21
		COQDEP = "coqdep -I src" \
22 23 24
		-o Makefile.coq

clean:: Makefile.coq
25
	$(MAKE) -f Makefile.coq clean
26
	rm -f Makefile.coq .depend cpdt.tgz templates/*.v
Adam Chlipala's avatar
Adam Chlipala committed
27
	cd latex; rm -f *.sty *.log *.aux *.dvi *.v.tex *.toc *.bbl *.blg *.idx *.ilg *.pdf *.ind *.out
Adam Chlipala's avatar
Adam Chlipala committed
28

Adam Chlipala's avatar
Adam Chlipala committed
29
doc: latex/cpdt.pdf html
Adam Chlipala's avatar
Adam Chlipala committed
30

31
latex/%.v.tex: Makefile src/%.v src/%.glob
32
	cd src ; coqdoc --interpolate --latex --body-only -s --no-externals \
33
		$*.v -o ../latex/$*.v.tex
Adam Chlipala's avatar
Adam Chlipala committed
34

35 36
latex/cpdt.pdf: latex/cpdt.tex $(TEX) latex/cpdt.bib
	cd latex ; pdflatex cpdt ; pdflatex cpdt ; bibtex cpdt ; makeindex cpdt ; pdflatex cpdt ; pdflatex cpdt
Adam Chlipala's avatar
Adam Chlipala committed
37

Adam Chlipala's avatar
Adam Chlipala committed
38 39
latex/%.pdf: latex/%.tex latex/cpdt.bib
	cd latex ; pdflatex $* ; pdflatex $* ; bibtex $* ; makeindex $* ; pdflatex $* ; pdflatex $*
Adam Chlipala's avatar
Adam Chlipala committed
40

Adam Chlipala's avatar
Adam Chlipala committed
41
html: Makefile $(VS) src/toc.html
42
	mkdir -p html
43
	cd src ; coqdoc --interpolate --no-externals $(VS_DOC) \
Adam Chlipala's avatar
Adam Chlipala committed
44
		-d ../html
Adam Chlipala's avatar
Adam Chlipala committed
45
	cp src/toc.html html/
Adam Chlipala's avatar
Adam Chlipala committed
46

Adam Chlipala's avatar
Adam Chlipala committed
47 48
templates: $(TEMPLATES)

49
templates/%.v: src/%.v tools/make_template.ml
Adam Chlipala's avatar
Adam Chlipala committed
50
	ocaml tools/make_template.ml <$< >$@
Adam Chlipala's avatar
Adam Chlipala committed
51 52 53 54

cpdt.tgz:
	hg archive -t tgz $@

Adam Chlipala's avatar
Adam Chlipala committed
55
install: cpdt.tgz latex/cpdt.pdf latex/exercises.pdf html
Adam Chlipala's avatar
Adam Chlipala committed
56 57
	cp cpdt.tgz staging/
	cp latex/cpdt.pdf staging/
Adam Chlipala's avatar
Adam Chlipala committed
58
	cp latex/exercises.pdf staging/ex/
Adam Chlipala's avatar
Adam Chlipala committed
59
	cp -R html staging/
60 61 62 63
	rsync -az --exclude '*~' staging/* chlipala.net:sites/chlipala/adam/cpdt/

pdf:
	evince latex/cpdt.pdf&
64 65 66 67 68

latex/exercises.pdf: Makefile src/Exercises.v
	coqc -I src src/Exercises
	coqdoc --latex -s src/Exercises.v -o latex/exercises.tex
	cd latex ; pdflatex exercises