Mercurial > cpdt > repo

annotate Makefile @ 21:00366a62bd00

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Proper title and copyright pages
author Adam Chlipala <adamc@hcoop.net>
date Wed, 03 Sep 2008 16:37:51 -0400
parents ea400f692b07
children 91e247c68ee8
rev   line source
adamc@3 1 MODULES_NODOC := Tactics
adamc@4 2 MODULES_DOC := Intro StackMachine
adamc@3 3 MODULES := $(MODULES_NODOC) $(MODULES_DOC)
adamc@3 4 VS := $(MODULES:%=src/%.v)
adamc@3 5 VS_DOC := $(MODULES_DOC:%=%.v)
adamc@3 6 GLOBALS := .coq_globals
adamc@2 7
adamc@4 8 .PHONY: coq clean doc dvi html
adamc@2 9
adamc@2 10 coq: Makefile.coq
adamc@2 11 make -f Makefile.coq
adamc@2 12
adamc@2 13 Makefile.coq: Makefile $(VS)
adamc@2 14 coq_makefile $(VS) \
adamc@3 15 COQC = "coqc -I src -impredicative-set \
adamc@3 16 -dump-glob $(GLOBALS)" \
adamc@2 17 -o Makefile.coq
adamc@2 18
adamc@2 19 clean:: Makefile.coq
adamc@2 20 make -f Makefile.coq clean
adamc@3 21 rm -f Makefile.coq .depend $(GLOBALS) \
adamc@3 22 latex/*.sty latex/cpdt.*
adamc@3 23
adamc@8 24 doc: latex/cpdt.dvi latex/cpdt.pdf html
adamc@3 25
adamc@21 26 latex/cpdt.tex: Makefile $(VS)
adamc@3 27 cd src ; coqdoc --latex $(VS_DOC) \
adamc@21 28 -p "\usepackage{url}" \
adamc@21 29 -p "\title{Certified Programming with Dependent Types}" \
adamc@21 30 -p "\author{Adam Chlipala}" \
adamc@21 31 -p "\iffalse" \
adamc@3 32 -o ../latex/cpdt.tex
adamc@3 33
adamc@3 34 latex/cpdt.dvi: latex/cpdt.tex
adamc@5 35 cd latex ; latex cpdt ; latex cpdt
adamc@4 36
adamc@8 37 latex/cpdt.pdf: latex/cpdt.dvi
adamc@8 38 cd latex ; pdflatex cpdt
adamc@8 39
adamc@21 40 html: Makefile $(VS)
adamc@5 41 cd src ; coqdoc $(VS_DOC) -toc \
adamc@4 42 --glob-from ../$(GLOBALS) \
adamc@4 43 -d ../html
adamc@4 44
adamc@4 45 dvi:
adamc@4 46 xdvi latex/cpdt