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@536: COQDOC = coqdoc -R . Cpdt
adam@536: 
adam@311: latex/%.v.tex: Makefile src/%.v src/%.glob
adam@536: 	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@536: 	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@538: 	coqc -R src Cpdt src/Exercises
adam@538: 	$(COQDOC) --latex -s src/Exercises.v -o latex/exercises.tex
adam@370: 	cd latex ; pdflatex exercises