annotate Makefile @ 558:cbe6d5ad3e13

Cornell course
author Adam Chlipala <adam@chlipala.net>
date Mon, 18 Sep 2017 10:16:51 -0400
parents 306539f29eea
children
rev   line source
adam@314 1 MODULES_NODOC := CpdtTactics MoreSpecif DepList
adamc@24 2 MODULES_PROSE := Intro
adam@353 3 MODULES_CODE := StackMachine InductiveTypes Predicates Coinductive Subset GeneralRec \
adam@324 4 MoreDep DataStruct Equality Generic Universes LogicProg Match Reflection \
adam@381 5 Large ProgLang
adam@383 6 MODULES_DOC := $(MODULES_PROSE) $(MODULES_CODE) Conclusion
adamc@3 7 MODULES := $(MODULES_NODOC) $(MODULES_DOC)
adamc@3 8 VS := $(MODULES:%=src/%.v)
adam@311 9 TEX := $(MODULES:%=latex/%.v.tex)
adamc@3 10 VS_DOC := $(MODULES_DOC:%=%.v)
adamc@22 11 TEMPLATES := $(MODULES_CODE:%=templates/%.v)
adamc@2 12
adam@307 13 .PHONY: coq clean doc html templates install cpdt.tgz pdf
adamc@2 14
adamc@2 15 coq: Makefile.coq
adam@305 16 $(MAKE) -f Makefile.coq
adamc@2 17
adamc@2 18 Makefile.coq: Makefile $(VS)
adamc@2 19 coq_makefile $(VS) \
adam@534 20 COQC = "coqc -R src Cpdt" \
adam@534 21 COQDEP = "coqdep -R src Cpdt" \
adamc@2 22 -o Makefile.coq
adamc@2 23
adamc@2 24 clean:: Makefile.coq
adam@305 25 $(MAKE) -f Makefile.coq clean
adam@311 26 rm -f Makefile.coq .depend cpdt.tgz templates/*.v
adam@320 27 cd latex; rm -f *.sty *.log *.aux *.dvi *.v.tex *.toc *.bbl *.blg *.idx *.ilg *.pdf *.ind *.out
adamc@3 28
adam@306 29 doc: latex/cpdt.pdf html
adamc@3 30
adam@536 31 COQDOC = coqdoc -R . Cpdt
adam@536 32
adam@311 33 latex/%.v.tex: Makefile src/%.v src/%.glob
adam@536 34 cd src ; $(COQDOC) --interpolate --latex --body-only -s \
adam@311 35 $*.v -o ../latex/$*.v.tex
adamc@3 36
adam@311 37 latex/cpdt.pdf: latex/cpdt.tex $(TEX) latex/cpdt.bib
adam@311 38 cd latex ; pdflatex cpdt ; pdflatex cpdt ; bibtex cpdt ; makeindex cpdt ; pdflatex cpdt ; pdflatex cpdt
adamc@4 39
adam@306 40 latex/%.pdf: latex/%.tex latex/cpdt.bib
adam@306 41 cd latex ; pdflatex $* ; pdflatex $* ; bibtex $* ; makeindex $* ; pdflatex $* ; pdflatex $*
adamc@8 42
adamc@39 43 html: Makefile $(VS) src/toc.html
adamc@205 44 mkdir -p html
adam@536 45 cd src ; $(COQDOC) --interpolate --no-externals $(VS_DOC) \
adamc@4 46 -d ../html
adamc@39 47 cp src/toc.html html/
adamc@4 48
adamc@22 49 templates: $(TEMPLATES)
adamc@22 50
adamc@41 51 templates/%.v: src/%.v tools/make_template.ml
adamc@22 52 ocaml tools/make_template.ml <$< >$@
adamc@39 53
adamc@39 54 cpdt.tgz:
adamc@39 55 hg archive -t tgz $@
adamc@39 56
adam@517 57 cpdtlib.tgz: Makefile
adam@517 58 mkdir -p cpdtlib
adam@517 59 cp src/LICENSE cpdtlib
amp@546 60 # Generate specifically BSD licenced versions of the lib files.
amp@546 61 ocaml tools/bsd_license.ml < src/CpdtTactics.v > cpdtlib/CpdtTactics.v
amp@546 62 ocaml tools/bsd_license.ml < src/MoreSpecif.v > cpdtlib/MoreSpecif.v
amp@546 63 ocaml tools/bsd_license.ml < src/DepList.v > cpdtlib/DepList.v
adam@517 64 tar zcf cpdtlib.tgz cpdtlib/*
adam@517 65
adam@517 66 install: cpdt.tgz cpdtlib.tgz latex/cpdt.pdf latex/exercises.pdf html
adam@517 67 cp cpdt*.tgz staging/
adamc@39 68 cp latex/cpdt.pdf staging/
adam@489 69 cp latex/exercises.pdf staging/ex/
adamc@39 70 cp -R html staging/
adam@307 71 rsync -az --exclude '*~' staging/* chlipala.net:sites/chlipala/adam/cpdt/
adam@307 72
adam@307 73 pdf:
adam@307 74 evince latex/cpdt.pdf&
adam@370 75
adam@370 76 latex/exercises.pdf: Makefile src/Exercises.v
adam@538 77 coqc -R src Cpdt src/Exercises
adam@538 78 $(COQDOC) --latex -s src/Exercises.v -o latex/exercises.tex
adam@370 79 cd latex ; pdflatex exercises