adamc@204: MODULES_NODOC := Axioms Tactics MoreSpecif DepList adamc@24: MODULES_PROSE := Intro adamc@105: MODULES_CODE := StackMachine InductiveTypes Predicates Coinductive Subset \ adamc@175: MoreDep DataStruct Equality Match Reflection Firstorder Hoas Interps \ adamc@193: Extensional Intensional Impure Generic 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@204: 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@208: rm -f *.aux *.dvi *.log adamc@3: adamc@8: doc: latex/cpdt.dvi latex/cpdt.pdf html adamc@3: adamc@21: latex/cpdt.tex: Makefile $(VS) adamc@206: cd src ; coqdoc --interpolate --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@208: latex/%.tex: src/%.v adamc@212: coqdoc --interpolate --latex -s \ adamc@212: -p "\usepackage{url}" \ adamc@212: $< -o $@ adamc@4: adamc@208: latex/%.dvi: latex/%.tex adamc@210: cd latex ; latex $* ; latex $* adamc@208: adamc@210: %.pdf: %.dvi adamc@208: pdflatex $< adamc@8: adamc@39: html: Makefile $(VS) src/toc.html adamc@205: mkdir -p html adamc@206: cd src ; coqdoc --interpolate $(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@201: # 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/