annotate Makefile @ 137:c0bda476b44b

Functional programming in Ltac
author Adam Chlipala <adamc@hcoop.net>
date Sun, 26 Oct 2008 15:18:13 -0400
parents bc1f7d3687e7
children 6a00d49e85fb
rev   line source
adamc@125 1 MODULES_NODOC := Axioms Tactics MoreSpecif DepList
adamc@24 2 MODULES_PROSE := Intro
adamc@105 3 MODULES_CODE := StackMachine InductiveTypes Predicates Coinductive Subset \
adamc@132 4 MoreDep DataStruct Equality Match
adamc@22 5 MODULES_DOC := $(MODULES_PROSE) $(MODULES_CODE)
adamc@3 6 MODULES := $(MODULES_NODOC) $(MODULES_DOC)
adamc@3 7 VS := $(MODULES:%=src/%.v)
adamc@3 8 VS_DOC := $(MODULES_DOC:%=%.v)
adamc@3 9 GLOBALS := .coq_globals
adamc@22 10 TEMPLATES := $(MODULES_CODE:%=templates/%.v)
adamc@2 11
adamc@42 12 .PHONY: coq clean doc dvi html templates install cpdt.tgz
adamc@2 13
adamc@2 14 coq: Makefile.coq
adamc@2 15 make -f Makefile.coq
adamc@2 16
adamc@2 17 Makefile.coq: Makefile $(VS)
adamc@2 18 coq_makefile $(VS) \
adamc@89 19 COQC = "coqc -I src -dump-glob $(GLOBALS)" \
adamc@89 20 COQDEP = "coqdep -I src" \
adamc@2 21 -o Makefile.coq
adamc@2 22
adamc@2 23 clean:: Makefile.coq
adamc@2 24 make -f Makefile.coq clean
adamc@49 25 rm -f Makefile.coq .depend $(GLOBALS) cpdt.tgz \
adamc@22 26 latex/*.sty latex/cpdt.* templates/*.v
adamc@3 27
adamc@8 28 doc: latex/cpdt.dvi latex/cpdt.pdf html
adamc@3 29
adamc@21 30 latex/cpdt.tex: Makefile $(VS)
adamc@25 31 cd src ; coqdoc --latex -s $(VS_DOC) \
adamc@21 32 -p "\usepackage{url}" \
adamc@21 33 -p "\title{Certified Programming with Dependent Types}" \
adamc@21 34 -p "\author{Adam Chlipala}" \
adamc@21 35 -p "\iffalse" \
adamc@3 36 -o ../latex/cpdt.tex
adamc@3 37
adamc@3 38 latex/cpdt.dvi: latex/cpdt.tex
adamc@5 39 cd latex ; latex cpdt ; latex cpdt
adamc@4 40
adamc@8 41 latex/cpdt.pdf: latex/cpdt.dvi
adamc@8 42 cd latex ; pdflatex cpdt
adamc@8 43
adamc@39 44 html: Makefile $(VS) src/toc.html
adamc@39 45 cd src ; coqdoc $(VS_DOC) \
adamc@4 46 --glob-from ../$(GLOBALS) \
adamc@4 47 -d ../html
adamc@39 48 cp src/toc.html html/
adamc@4 49
adamc@4 50 dvi:
adamc@4 51 xdvi latex/cpdt
adamc@22 52
adamc@22 53 templates: $(TEMPLATES)
adamc@22 54
adamc@41 55 templates/%.v: src/%.v tools/make_template.ml
adamc@22 56 ocaml tools/make_template.ml <$< >$@
adamc@39 57
adamc@39 58 cpdt.tgz:
adamc@39 59 hg archive -t tgz $@
adamc@39 60
adamc@39 61 install: cpdt.tgz latex/cpdt.pdf html
adamc@39 62 cp cpdt.tgz staging/
adamc@39 63 cp latex/cpdt.pdf staging/
adamc@39 64 cp -R html staging/
adamc@69 65 rsync -az --exclude '*~' staging/* bowser.eecs.harvard.edu:public_html/cpdt/book/
adamc@39 66 rsync -az --exclude '*~' staging/* ssh.hcoop.net:sites/chlipala/adam/cpdt/