adam@314: MODULES_NODOC := CpdtTactics MoreSpecif DepList adamc@24: MODULES_PROSE := Intro adam@353: MODULES_CODE := StackMachine InductiveTypes Predicates Coinductive Subset GeneralRec \ adam@324: MoreDep DataStruct Equality Generic Universes LogicProg Match Reflection \ adam@381: Large ProgLang adam@383: MODULES_DOC := $(MODULES_PROSE) $(MODULES_CODE) Conclusion adamc@3: MODULES := $(MODULES_NODOC) $(MODULES_DOC) adamc@3: VS := $(MODULES:%=src/%.v) adam@311: TEX := $(MODULES:%=latex/%.v.tex) adamc@3: VS_DOC := $(MODULES_DOC:%=%.v) adamc@22: TEMPLATES := $(MODULES_CODE:%=templates/%.v) adamc@2: adam@307: .PHONY: coq clean doc html templates install cpdt.tgz pdf adamc@2: adamc@2: coq: Makefile.coq adam@305: $(MAKE) -f Makefile.coq adamc@2: adamc@2: Makefile.coq: Makefile $(VS) adamc@2: coq_makefile $(VS) \ adam@534: COQC = "coqc -R src Cpdt" \ adam@534: COQDEP = "coqdep -R src Cpdt" \ adamc@2: -o Makefile.coq adamc@2: adamc@2: clean:: Makefile.coq adam@305: $(MAKE) -f Makefile.coq clean adam@311: rm -f Makefile.coq .depend cpdt.tgz templates/*.v adam@320: cd latex; rm -f *.sty *.log *.aux *.dvi *.v.tex *.toc *.bbl *.blg *.idx *.ilg *.pdf *.ind *.out adamc@3: adam@306: doc: latex/cpdt.pdf html adamc@3: adam@311: latex/%.v.tex: Makefile src/%.v src/%.glob adam@503: cd src ; coqdoc --interpolate --latex --body-only -s \ adam@311: $*.v -o ../latex/$*.v.tex adamc@3: adam@311: latex/cpdt.pdf: latex/cpdt.tex $(TEX) latex/cpdt.bib adam@311: cd latex ; pdflatex cpdt ; pdflatex cpdt ; bibtex cpdt ; makeindex cpdt ; pdflatex cpdt ; pdflatex cpdt adamc@4: adam@306: latex/%.pdf: latex/%.tex latex/cpdt.bib adam@306: cd latex ; pdflatex $* ; pdflatex $* ; bibtex $* ; makeindex $* ; pdflatex $* ; pdflatex $* adamc@8: adamc@39: html: Makefile $(VS) src/toc.html adamc@205: mkdir -p html adam@473: cd src ; coqdoc --interpolate --no-externals $(VS_DOC) \ adamc@4: -d ../html adamc@39: cp src/toc.html html/ adamc@4: adamc@22: templates: $(TEMPLATES) adamc@22: adamc@41: templates/%.v: src/%.v tools/make_template.ml adamc@22: ocaml tools/make_template.ml <$< >$@ adamc@39: adamc@39: cpdt.tgz: adamc@39: hg archive -t tgz $@ adamc@39: adam@517: cpdtlib.tgz: Makefile adam@517: mkdir -p cpdtlib adam@517: cp src/LICENSE cpdtlib adam@517: cp src/CpdtTactics.v cpdtlib adam@517: cp src/MoreSpecif.v cpdtlib adam@517: cp src/DepList.v cpdtlib adam@517: tar zcf cpdtlib.tgz cpdtlib/* adam@517: adam@517: install: cpdt.tgz cpdtlib.tgz latex/cpdt.pdf latex/exercises.pdf html adam@517: cp cpdt*.tgz staging/ adamc@39: cp latex/cpdt.pdf staging/ adam@489: cp latex/exercises.pdf staging/ex/ adamc@39: cp -R html staging/ adam@307: rsync -az --exclude '*~' staging/* chlipala.net:sites/chlipala/adam/cpdt/ adam@307: adam@307: pdf: adam@307: evince latex/cpdt.pdf& adam@370: adam@370: latex/exercises.pdf: Makefile src/Exercises.v adam@370: coqc -I src src/Exercises adam@370: coqdoc --latex -s src/Exercises.v -o latex/exercises.tex adam@370: cd latex ; pdflatex exercises