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/