annotate Makefile @ 37:c9ade53b27aa

TVL and constant-folding exercises
author Adam Chlipala <adamc@hcoop.net>
date Fri, 12 Sep 2008 15:30:59 -0400
parents 65314ca099ed
children fd18331e5c0b
rev   line source
adamc@3 1 MODULES_NODOC := Tactics
adamc@24 2 MODULES_PROSE := Intro
adamc@26 3 MODULES_CODE := StackMachine InductiveTypes
adamc@22 4 MODULES_DOC := $(MODULES_PROSE) $(MODULES_CODE)
adamc@3 5 MODULES := $(MODULES_NODOC) $(MODULES_DOC)
adamc@3 6 VS := $(MODULES:%=src/%.v)
adamc@3 7 VS_DOC := $(MODULES_DOC:%=%.v)
adamc@3 8 GLOBALS := .coq_globals
adamc@22 9 TEMPLATES := $(MODULES_CODE:%=templates/%.v)
adamc@2 10
adamc@22 11 .PHONY: coq clean doc dvi html templates
adamc@2 12
adamc@2 13 coq: Makefile.coq
adamc@2 14 make -f Makefile.coq
adamc@2 15
adamc@2 16 Makefile.coq: Makefile $(VS)
adamc@2 17 coq_makefile $(VS) \
adamc@3 18 COQC = "coqc -I src -impredicative-set \
adamc@3 19 -dump-glob $(GLOBALS)" \
adamc@2 20 -o Makefile.coq
adamc@2 21
adamc@2 22 clean:: Makefile.coq
adamc@2 23 make -f Makefile.coq clean
adamc@3 24 rm -f Makefile.coq .depend $(GLOBALS) \
adamc@22 25 latex/*.sty latex/cpdt.* templates/*.v
adamc@3 26
adamc@8 27 doc: latex/cpdt.dvi latex/cpdt.pdf html
adamc@3 28
adamc@21 29 latex/cpdt.tex: Makefile $(VS)
adamc@25 30 cd src ; coqdoc --latex -s $(VS_DOC) \
adamc@21 31 -p "\usepackage{url}" \
adamc@21 32 -p "\title{Certified Programming with Dependent Types}" \
adamc@21 33 -p "\author{Adam Chlipala}" \
adamc@21 34 -p "\iffalse" \
adamc@3 35 -o ../latex/cpdt.tex
adamc@3 36
adamc@3 37 latex/cpdt.dvi: latex/cpdt.tex
adamc@5 38 cd latex ; latex cpdt ; latex cpdt
adamc@4 39
adamc@8 40 latex/cpdt.pdf: latex/cpdt.dvi
adamc@8 41 cd latex ; pdflatex cpdt
adamc@8 42
adamc@21 43 html: Makefile $(VS)
adamc@5 44 cd src ; coqdoc $(VS_DOC) -toc \
adamc@4 45 --glob-from ../$(GLOBALS) \
adamc@4 46 -d ../html
adamc@4 47
adamc@4 48 dvi:
adamc@4 49 xdvi latex/cpdt
adamc@22 50
adamc@22 51 templates: $(TEMPLATES)
adamc@22 52
adamc@22 53 templates/%.v: src/%.v
adamc@22 54 ocaml tools/make_template.ml <$< >$@