adamc@3: MODULES_NODOC := Tactics adamc@24: MODULES_PROSE := Intro adamc@26: MODULES_CODE := StackMachine InductiveTypes 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@22: .PHONY: coq clean doc dvi html templates 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@3: COQC = "coqc -I src -impredicative-set \ adamc@3: -dump-glob $(GLOBALS)" \ adamc@2: -o Makefile.coq adamc@2: adamc@2: clean:: Makefile.coq adamc@2: make -f Makefile.coq clean adamc@3: rm -f Makefile.coq .depend $(GLOBALS) \ 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@21: html: Makefile $(VS) adamc@5: cd src ; coqdoc $(VS_DOC) -toc \ adamc@4: --glob-from ../$(GLOBALS) \ adamc@4: -d ../html adamc@4: adamc@4: dvi: adamc@4: xdvi latex/cpdt adamc@22: adamc@22: templates: $(TEMPLATES) adamc@22: adamc@22: templates/%.v: src/%.v adamc@22: ocaml tools/make_template.ml <$< >$@