adamc@125: MODULES_NODOC := Axioms Tactics MoreSpecif DepList adamc@24: MODULES_PROSE := Intro adamc@105: MODULES_CODE := StackMachine InductiveTypes Predicates Coinductive Subset \ adamc@132: MoreDep DataStruct Equality Match adamc@22: MODULES_DOC := $(MODULES_PROSE) $(MODULES_CODE) adamc@3: MODULES := $(MODULES_NODOC) $(MODULES_DOC) adamc@3: VS := $(MODULES:%=src/%.v) adamc@3: VS_DOC := $(MODULES_DOC:%=%.v) adamc@3: GLOBALS := .coq_globals adamc@22: TEMPLATES := $(MODULES_CODE:%=templates/%.v) adamc@2: adamc@42: .PHONY: coq clean doc dvi html templates install cpdt.tgz adamc@2: adamc@2: coq: Makefile.coq adamc@2: make -f Makefile.coq adamc@2: adamc@2: Makefile.coq: Makefile $(VS) adamc@2: coq_makefile $(VS) \ adamc@89: COQC = "coqc -I src -dump-glob $(GLOBALS)" \ adamc@89: COQDEP = "coqdep -I src" \ adamc@2: -o Makefile.coq adamc@2: adamc@2: clean:: Makefile.coq adamc@2: make -f Makefile.coq clean adamc@49: rm -f Makefile.coq .depend $(GLOBALS) cpdt.tgz \ adamc@22: latex/*.sty latex/cpdt.* templates/*.v adamc@3: adamc@8: doc: latex/cpdt.dvi latex/cpdt.pdf html adamc@3: adamc@21: latex/cpdt.tex: Makefile $(VS) adamc@25: cd src ; coqdoc --latex -s $(VS_DOC) \ adamc@21: -p "\usepackage{url}" \ adamc@21: -p "\title{Certified Programming with Dependent Types}" \ adamc@21: -p "\author{Adam Chlipala}" \ adamc@21: -p "\iffalse" \ adamc@3: -o ../latex/cpdt.tex adamc@3: adamc@3: latex/cpdt.dvi: latex/cpdt.tex adamc@5: cd latex ; latex cpdt ; latex cpdt adamc@4: adamc@8: latex/cpdt.pdf: latex/cpdt.dvi adamc@8: cd latex ; pdflatex cpdt adamc@8: adamc@39: html: Makefile $(VS) src/toc.html adamc@39: cd src ; coqdoc $(VS_DOC) \ adamc@4: --glob-from ../$(GLOBALS) \ adamc@4: -d ../html adamc@39: cp src/toc.html html/ adamc@4: adamc@4: dvi: adamc@4: xdvi latex/cpdt adamc@22: adamc@22: templates: $(TEMPLATES) adamc@22: adamc@41: templates/%.v: src/%.v tools/make_template.ml adamc@22: ocaml tools/make_template.ml <$< >$@ adamc@39: adamc@39: cpdt.tgz: adamc@39: hg archive -t tgz $@ adamc@39: adamc@39: install: cpdt.tgz latex/cpdt.pdf html adamc@39: cp cpdt.tgz staging/ adamc@39: cp latex/cpdt.pdf staging/ adamc@39: cp -R html staging/ adamc@69: rsync -az --exclude '*~' staging/* bowser.eecs.harvard.edu:public_html/cpdt/book/ adamc@39: rsync -az --exclude '*~' staging/* ssh.hcoop.net:sites/chlipala/adam/cpdt/