annotate Makefile @ 256:4293dd6912cd

Prosified Extensional
author Adam Chlipala <adamc@hcoop.net>
date Wed, 16 Dec 2009 15:31:54 -0500
parents 52b9e43be069
children de53c8bcfa8d
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@227 4 MoreDep DataStruct Equality Generic Universes Match Reflection \
adamc@235 5 Large Firstorder Hoas Interps Extensional Intensional Impure
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@22 10 TEMPLATES := $(MODULES_CODE:%=templates/%.v)
adamc@2 11
adamc@42 12 .PHONY: coq clean doc dvi html templates install cpdt.tgz
adamc@2 13
adamc@2 14 coq: Makefile.coq
adamc@2 15 make -f Makefile.coq
adamc@2 16
adamc@2 17 Makefile.coq: Makefile $(VS)
adamc@2 18 coq_makefile $(VS) \
adamc@215 19 COQC = "coqc -I src" \
adamc@89 20 COQDEP = "coqdep -I src" \
adamc@2 21 -o Makefile.coq
adamc@2 22
adamc@2 23 clean:: Makefile.coq
adamc@2 24 make -f Makefile.coq clean
adamc@215 25 rm -f Makefile.coq .depend cpdt.tgz \
adamc@22 26 latex/*.sty latex/cpdt.* templates/*.v
adamc@208 27 rm -f *.aux *.dvi *.log
adamc@3 28
adamc@8 29 doc: latex/cpdt.dvi latex/cpdt.pdf html
adamc@3 30
adamc@21 31 latex/cpdt.tex: Makefile $(VS)
adamc@206 32 cd src ; coqdoc --interpolate --latex -s $(VS_DOC) \
adamc@219 33 -p "\usepackage{url,amsmath,amssymb}" \
adamc@21 34 -p "\title{Certified Programming with Dependent Types}" \
adamc@21 35 -p "\author{Adam Chlipala}" \
adamc@21 36 -p "\iffalse" \
adamc@3 37 -o ../latex/cpdt.tex
adamc@3 38
adamc@208 39 latex/%.tex: src/%.v
adamc@212 40 coqdoc --interpolate --latex -s \
adamc@219 41 -p "\usepackage{url,amsmath,amssymb}" \
adamc@212 42 $< -o $@
adamc@4 43
adamc@208 44 latex/%.dvi: latex/%.tex
adamc@210 45 cd latex ; latex $* ; latex $*
adamc@208 46
adamc@214 47 latex/%.pdf: latex/%.dvi
adamc@226 48 cd latex ; pdflatex $* ; pdflatex $*
adamc@8 49
adamc@39 50 html: Makefile $(VS) src/toc.html
adamc@205 51 mkdir -p html
adamc@206 52 cd src ; coqdoc --interpolate $(VS_DOC) \
adamc@4 53 -d ../html
adamc@39 54 cp src/toc.html html/
adamc@4 55
adamc@4 56 dvi:
adamc@4 57 xdvi latex/cpdt
adamc@22 58
adamc@22 59 templates: $(TEMPLATES)
adamc@22 60
adamc@41 61 templates/%.v: src/%.v tools/make_template.ml
adamc@22 62 ocaml tools/make_template.ml <$< >$@
adamc@39 63
adamc@39 64 cpdt.tgz:
adamc@39 65 hg archive -t tgz $@
adamc@39 66
adamc@39 67 install: cpdt.tgz latex/cpdt.pdf html
adamc@39 68 cp cpdt.tgz staging/
adamc@39 69 cp latex/cpdt.pdf staging/
adamc@39 70 cp -R html staging/
adamc@226 71 rsync -az --exclude '*~' staging/* schizomaniac.net:sites/chlipala/adam/cpdt/