annotate Makefile @ 213:c4b1c0de7af9

Start of MoreDep port; new [dep_destruct] based on [dependent destruction]
author Adam Chlipala <adamc@hcoop.net>
date Wed, 11 Nov 2009 10:27:47 -0500
parents 3227be370687
children 768889c969e9
rev   line source
adamc@204 1 MODULES_NODOC := Axioms Tactics MoreSpecif DepList
adamc@24 2 MODULES_PROSE := Intro
adamc@105 3 MODULES_CODE := StackMachine InductiveTypes Predicates Coinductive Subset \
adamc@175 4 MoreDep DataStruct Equality Match Reflection Firstorder Hoas Interps \
adamc@193 5 Extensional Intensional Impure Generic
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@3 10 GLOBALS := .coq_globals
adamc@22 11 TEMPLATES := $(MODULES_CODE:%=templates/%.v)
adamc@2 12
adamc@42 13 .PHONY: coq clean doc dvi html templates install cpdt.tgz
adamc@2 14
adamc@2 15 coq: Makefile.coq
adamc@2 16 make -f Makefile.coq
adamc@2 17
adamc@2 18 Makefile.coq: Makefile $(VS)
adamc@2 19 coq_makefile $(VS) \
adamc@204 20 COQC = "coqc -I src -dump-glob $(GLOBALS)" \
adamc@89 21 COQDEP = "coqdep -I src" \
adamc@2 22 -o Makefile.coq
adamc@2 23
adamc@2 24 clean:: Makefile.coq
adamc@2 25 make -f Makefile.coq clean
adamc@49 26 rm -f Makefile.coq .depend $(GLOBALS) cpdt.tgz \
adamc@22 27 latex/*.sty latex/cpdt.* templates/*.v
adamc@208 28 rm -f *.aux *.dvi *.log
adamc@3 29
adamc@8 30 doc: latex/cpdt.dvi latex/cpdt.pdf html
adamc@3 31
adamc@21 32 latex/cpdt.tex: Makefile $(VS)
adamc@206 33 cd src ; coqdoc --interpolate --latex -s $(VS_DOC) \
adamc@21 34 -p "\usepackage{url}" \
adamc@21 35 -p "\title{Certified Programming with Dependent Types}" \
adamc@21 36 -p "\author{Adam Chlipala}" \
adamc@21 37 -p "\iffalse" \
adamc@3 38 -o ../latex/cpdt.tex
adamc@3 39
adamc@208 40 latex/%.tex: src/%.v
adamc@212 41 coqdoc --interpolate --latex -s \
adamc@212 42 -p "\usepackage{url}" \
adamc@212 43 $< -o $@
adamc@4 44
adamc@208 45 latex/%.dvi: latex/%.tex
adamc@210 46 cd latex ; latex $* ; latex $*
adamc@208 47
adamc@210 48 %.pdf: %.dvi
adamc@208 49 pdflatex $<
adamc@8 50
adamc@39 51 html: Makefile $(VS) src/toc.html
adamc@205 52 mkdir -p html
adamc@206 53 cd src ; coqdoc --interpolate $(VS_DOC) \
adamc@4 54 --glob-from ../$(GLOBALS) \
adamc@4 55 -d ../html
adamc@39 56 cp src/toc.html html/
adamc@4 57
adamc@4 58 dvi:
adamc@4 59 xdvi latex/cpdt
adamc@22 60
adamc@22 61 templates: $(TEMPLATES)
adamc@22 62
adamc@41 63 templates/%.v: src/%.v tools/make_template.ml
adamc@22 64 ocaml tools/make_template.ml <$< >$@
adamc@39 65
adamc@39 66 cpdt.tgz:
adamc@39 67 hg archive -t tgz $@
adamc@39 68
adamc@39 69 install: cpdt.tgz latex/cpdt.pdf html
adamc@39 70 cp cpdt.tgz staging/
adamc@39 71 cp latex/cpdt.pdf staging/
adamc@39 72 cp -R html staging/
adamc@201 73 # rsync -az --exclude '*~' staging/* bowser.eecs.harvard.edu:public_html/cpdt/book/
adamc@39 74 rsync -az --exclude '*~' staging/* ssh.hcoop.net:sites/chlipala/adam/cpdt/