Mercurial > cpdt > repo
comparison Makefile @ 219:dbac52f5bce1
Port Generic
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Fri, 13 Nov 2009 12:03:08 -0500 |
parents | 6601384e7e14 |
children | 9d0b9577f8b1 |
comparison
equal
deleted
inserted
replaced
218:c8508d277a00 | 219:dbac52f5bce1 |
---|---|
1 MODULES_NODOC := Axioms Tactics MoreSpecif DepList | 1 MODULES_NODOC := Axioms Tactics MoreSpecif DepList |
2 MODULES_PROSE := Intro | 2 MODULES_PROSE := Intro |
3 MODULES_CODE := StackMachine InductiveTypes Predicates Coinductive Subset \ | 3 MODULES_CODE := StackMachine InductiveTypes Predicates Coinductive Subset \ |
4 MoreDep DataStruct Equality Match Reflection Firstorder Hoas Interps \ | 4 MoreDep DataStruct Equality Generic Match Reflection Firstorder Hoas \ |
5 Extensional Intensional Impure Generic | 5 Interps Extensional Intensional Impure |
6 MODULES_DOC := $(MODULES_PROSE) $(MODULES_CODE) | 6 MODULES_DOC := $(MODULES_PROSE) $(MODULES_CODE) |
7 MODULES := $(MODULES_NODOC) $(MODULES_DOC) | 7 MODULES := $(MODULES_NODOC) $(MODULES_DOC) |
8 VS := $(MODULES:%=src/%.v) | 8 VS := $(MODULES:%=src/%.v) |
9 VS_DOC := $(MODULES_DOC:%=%.v) | 9 VS_DOC := $(MODULES_DOC:%=%.v) |
10 TEMPLATES := $(MODULES_CODE:%=templates/%.v) | 10 TEMPLATES := $(MODULES_CODE:%=templates/%.v) |
28 | 28 |
29 doc: latex/cpdt.dvi latex/cpdt.pdf html | 29 doc: latex/cpdt.dvi latex/cpdt.pdf html |
30 | 30 |
31 latex/cpdt.tex: Makefile $(VS) | 31 latex/cpdt.tex: Makefile $(VS) |
32 cd src ; coqdoc --interpolate --latex -s $(VS_DOC) \ | 32 cd src ; coqdoc --interpolate --latex -s $(VS_DOC) \ |
33 -p "\usepackage{url}" \ | 33 -p "\usepackage{url,amsmath,amssymb}" \ |
34 -p "\title{Certified Programming with Dependent Types}" \ | 34 -p "\title{Certified Programming with Dependent Types}" \ |
35 -p "\author{Adam Chlipala}" \ | 35 -p "\author{Adam Chlipala}" \ |
36 -p "\iffalse" \ | 36 -p "\iffalse" \ |
37 -o ../latex/cpdt.tex | 37 -o ../latex/cpdt.tex |
38 | 38 |
39 latex/%.tex: src/%.v | 39 latex/%.tex: src/%.v |
40 coqdoc --interpolate --latex -s \ | 40 coqdoc --interpolate --latex -s \ |
41 -p "\usepackage{url}" \ | 41 -p "\usepackage{url,amsmath,amssymb}" \ |
42 $< -o $@ | 42 $< -o $@ |
43 | 43 |
44 latex/%.dvi: latex/%.tex | 44 latex/%.dvi: latex/%.tex |
45 cd latex ; latex $* ; latex $* | 45 cd latex ; latex $* ; latex $* |
46 | 46 |