Makefile 1.86 KB
Newer Older
1
MODULES_NODOC := Axioms Tactics MoreSpecif DepList
2
MODULES_PROSE := Intro
Adam Chlipala's avatar
Adam Chlipala committed
3
MODULES_CODE  := StackMachine InductiveTypes Predicates Coinductive Subset \
4
	MoreDep DataStruct Equality Generic Universes Match Reflection \
5
	Large Firstorder Hoas Interps Extensional Intensional Impure
Adam Chlipala's avatar
Adam Chlipala committed
6
MODULES_DOC   := $(MODULES_PROSE) $(MODULES_CODE)
Adam Chlipala's avatar
Adam Chlipala committed
7 8 9
MODULES       := $(MODULES_NODOC) $(MODULES_DOC)
VS            := $(MODULES:%=src/%.v)
VS_DOC        := $(MODULES_DOC:%=%.v)
Adam Chlipala's avatar
Adam Chlipala committed
10
TEMPLATES     := $(MODULES_CODE:%=templates/%.v)
11

Adam Chlipala's avatar
Adam Chlipala committed
12
.PHONY: coq clean doc dvi html templates install cpdt.tgz
13 14 15 16 17 18

coq: Makefile.coq
	make -f Makefile.coq

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

clean:: Makefile.coq
	make -f Makefile.coq clean
Adam Chlipala's avatar
Adam Chlipala committed
25
	rm -f Makefile.coq .depend cpdt.tgz \
Adam Chlipala's avatar
Adam Chlipala committed
26
		latex/*.sty latex/cpdt.* templates/*.v
Adam Chlipala's avatar
Adam Chlipala committed
27
	rm -f *.aux *.dvi *.log
Adam Chlipala's avatar
Adam Chlipala committed
28

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

31
latex/cpdt.tex: Makefile $(VS)
32
	cd src ; coqdoc --interpolate --latex -s $(VS_DOC) \
Adam Chlipala's avatar
Adam Chlipala committed
33
		-p "\usepackage{url,amsmath,amssymb}" \
34 35 36
		-p "\title{Certified Programming with Dependent Types}" \
		-p "\author{Adam Chlipala}" \
		-p "\iffalse" \
Adam Chlipala's avatar
Adam Chlipala committed
37 38
		-o ../latex/cpdt.tex

Adam Chlipala's avatar
Adam Chlipala committed
39
latex/%.tex: src/%.v
Adam Chlipala's avatar
Adam Chlipala committed
40
	coqdoc --interpolate --latex -s \
Adam Chlipala's avatar
Adam Chlipala committed
41
		-p "\usepackage{url,amsmath,amssymb}" \
Adam Chlipala's avatar
Adam Chlipala committed
42
		$< -o $@
Adam Chlipala's avatar
Adam Chlipala committed
43

Adam Chlipala's avatar
Adam Chlipala committed
44
latex/%.dvi: latex/%.tex
45
	cd latex ; latex $* ; latex $*
Adam Chlipala's avatar
Adam Chlipala committed
46

Adam Chlipala's avatar
Adam Chlipala committed
47
latex/%.pdf: latex/%.dvi
Adam Chlipala's avatar
Adam Chlipala committed
48
	cd latex ; pdflatex $* ; pdflatex $*
Adam Chlipala's avatar
Adam Chlipala committed
49

Adam Chlipala's avatar
Adam Chlipala committed
50
html: Makefile $(VS) src/toc.html
51
	mkdir -p html
52
	cd src ; coqdoc --interpolate $(VS_DOC) \
Adam Chlipala's avatar
Adam Chlipala committed
53
		-d ../html
Adam Chlipala's avatar
Adam Chlipala committed
54
	cp src/toc.html html/
Adam Chlipala's avatar
Adam Chlipala committed
55 56 57

dvi:
	xdvi latex/cpdt
Adam Chlipala's avatar
Adam Chlipala committed
58 59 60

templates: $(TEMPLATES)

61
templates/%.v: src/%.v tools/make_template.ml
Adam Chlipala's avatar
Adam Chlipala committed
62
	ocaml tools/make_template.ml <$< >$@
Adam Chlipala's avatar
Adam Chlipala committed
63 64 65 66 67 68 69 70

cpdt.tgz:
	hg archive -t tgz $@

install: cpdt.tgz latex/cpdt.pdf html
	cp cpdt.tgz staging/
	cp latex/cpdt.pdf staging/
	cp -R html staging/
Adam Chlipala's avatar
Adam Chlipala committed
71
	rsync -az --exclude '*~' staging/* schizomaniac.net:sites/chlipala/adam/cpdt/