# Makefile for the Coq documentation # COQSRC needs to be set to a coq source repository # To compile documentation, you need the following tools: # Dvi: latex (latex2e), bibtex, makeindex # Pdf: pdflatex # Html: hevea (http://hevea.inria.fr) >= 1.05 ###################################################################### ### General rules ###################################################################### .PHONY: doc doc-html doc-pdf doc-ps refman tutorial stdlib faq rectutorial doc: refman faq tutorial rectutorial stdlib ide/index_urls.txt doc-html:\ doc/tutorial/Tutorial.v.html doc/refman/html/index.html \ doc/faq/html/index.html doc/stdlib/html/index.html doc/RecTutorial/RecTutorial.html doc-pdf:\ doc/tutorial/Tutorial.v.pdf doc/refman/Reference-Manual.pdf \ doc/faq/FAQ.v.pdf doc/stdlib/Library.pdf doc/RecTutorial/RecTutorial.pdf doc-ps:\ doc/tutorial/Tutorial.v.ps doc/refman/Reference-Manual.ps \ doc/faq/FAQ.v.ps doc/stdlib/Library.ps doc/RecTutorial/RecTutorial.ps refman: \ doc/refman/html/index.html doc/refman/Reference-Manual.ps doc/refman/Reference-Manual.pdf tutorial: \ doc/tutorial/Tutorial.v.html doc/tutorial/Tutorial.v.ps doc/tutorial/Tutorial.v.pdf stdlib: \ doc/stdlib/html/index.html doc/stdlib/Library.ps doc/stdlib/Library.pdf faq: doc/faq/html/index.html doc/faq/FAQ.v.ps doc/faq/FAQ.v.pdf rectutorial: doc/RecTutorial/RecTutorial.html \ doc/RecTutorial/RecTutorial.ps doc/RecTutorial/RecTutorial.pdf ###################################################################### ### Implicit rules ###################################################################### ifdef QUICK %.v.tex: %.tex (cd `dirname $<`; $(COQSRC)/$(COQTEX) $(COQTEXOPTS) `basename $<`) else %.v.tex: %.tex $(COQTEX) $(COQTOPEXE) $(PLUGINSVO) $(THEORIESVO) (cd `dirname $<`; $(COQSRC)/$(COQTEX) $(COQTEXOPTS) `basename $<`) endif %.ps: %.dvi (cd `dirname $<`; dvips -q -o `basename $@` `basename $<`) %.eps: %.png pngtopnm $< | pnmtops -equalpixels -noturn -rle > $@ ###################################################################### # Macros for filtering outputs ###################################################################### HIDEBIBTEXINFO=| grep -v "^A level-1 auxiliary file" SHOWMAKEINDEXERROR=egrep '^!! Input index error|^\*\* Input style error|^ --' # Empty subsection levels in faq are on purpose HEVEAFAQFILTER=2>&1 | grep -v "^Warning: List with no item" ###################################################################### # Common ###################################################################### ### Version doc/common/version.tex: config/Makefile printf '\\newcommand{\\coqversion}{$(VERSION)}' > doc/common/version.tex ###################################################################### # Reference Manual ###################################################################### ### Reference Manual (printable format) # The second LATEX compilation is necessary otherwise the pages of the index # are not correct (don't know why...) - BB doc/refman/Reference-Manual.dvi: $(REFMANFILES) doc/refman/Reference-Manual.tex @(cd doc/refman;\ $(LATEX) -interaction=batchmode Reference-Manual;\ $(BIBTEX) -terse Reference-Manual $(HIDEBIBTEXINFO);\ $(LATEX) -interaction=batchmode Reference-Manual > /dev/null;\ $(MAKEINDEX) -q Reference-Manual;\ $(SHOWMAKEINDEXERROR) Reference-Manual.ilg;\ $(MAKEINDEX) -q Reference-Manual.tacidx -o Reference-Manual.tacind;\ $(SHOWMAKEINDEXERROR) Reference-Manual.ilg;\ $(MAKEINDEX) -q Reference-Manual.comidx -o Reference-Manual.comind;\ $(SHOWMAKEINDEXERROR) Reference-Manual.ilg;\ $(MAKEINDEX) -q Reference-Manual.erridx -o Reference-Manual.errind;\ $(SHOWMAKEINDEXERROR) Reference-Manual.ilg;\ $(LATEX) -interaction=batchmode Reference-Manual > /dev/null;\ $(LATEX) -interaction=batchmode Reference-Manual > /dev/null;\ ../tools/show_latex_messages -no-overfull Reference-Manual.log) doc/refman/Reference-Manual.pdf: $(REFMANFILES) doc/refman/Reference-Manual.tex (cd doc/refman;\ $(PDFLATEX) -interaction=batchmode Reference-Manual.tex;\ ../tools/show_latex_messages -no-overfull Reference-Manual.log) ### Reference Manual (browsable format) doc/refman/Reference-Manual.html: doc/refman/styles.hva doc/refman/headers.hva doc/refman/Reference-Manual.dvi # to ensure bbl file (cd doc/refman; BIBINPUTS=.: $(HEVEA) $(HEVEAOPTS) ./styles.hva ./Reference-Manual.tex) doc/refman/cover.html: doc/common/styles/html/$(HTMLSTYLE)/cover.html $(INSTALLLIB) $< doc/refman doc/refman/styles.hva: doc/common/styles/html/$(HTMLSTYLE)/styles.hva $(INSTALLLIB) $< doc/refman doc/refman/html/index.html: doc/refman/Reference-Manual.html $(REFMANPNGFILES) \ doc/refman/cover.html doc/refman/styles.hva doc/refman/index.html - rm -rf doc/refman/html $(MKDIR) doc/refman/html $(INSTALLLIB) $(REFMANPNGFILES) doc/refman/html (cd doc/refman/html; hacha -nolinks -tocbis -o toc.html ../styles.hva ../Reference-Manual.html) $(INSTALLLIB) doc/refman/cover.html doc/refman/html/index.html $(INSTALLLIB) doc/common/styles/html/$(HTMLSTYLE)/*.css doc/refman/html refman-quick: (cd doc/refman;\ $(PDFLATEX) -interaction=batchmode Reference-Manual.tex;\ ../tools/show_latex_messages -no-overfull Reference-Manual.log && \ $(HEVEA) $(HEVEAOPTS) ./Reference-Manual.tex) ###################################################################### # Tutorial ###################################################################### doc/tutorial/Tutorial.v.dvi: $(DOCCOMMON) doc/tutorial/Tutorial.v.tex (cd doc/tutorial;\ $(LATEX) -interaction=batchmode Tutorial.v;\ ../tools/show_latex_messages Tutorial.v.log) doc/tutorial/Tutorial.v.pdf: $(DOCCOMMON) doc/tutorial/Tutorial.v.tex (cd doc/tutorial;\ $(PDFLATEX) -interaction=batchmode Tutorial.v.tex;\ ../tools/show_latex_messages Tutorial.v.log) doc/tutorial/Tutorial.v.html: $(DOCCOMMON) doc/tutorial/Tutorial.v.tex (cd doc/tutorial; $(HEVEA) $(HEVEAOPTS) Tutorial.v) ###################################################################### # FAQ ###################################################################### doc/faq/FAQ.v.dvi: doc/common/version.tex doc/common/title.tex doc/faq/FAQ.v.tex (cd doc/faq;\ $(LATEX) -interaction=batchmode FAQ.v;\ $(BIBTEX) -terse FAQ.v;\ $(LATEX) -interaction=batchmode FAQ.v > /dev/null;\ $(LATEX) -interaction=batchmode FAQ.v > /dev/null;\ ../tools/show_latex_messages FAQ.v.log) doc/faq/FAQ.v.pdf: doc/common/version.tex doc/common/title.tex doc/faq/FAQ.v.dvi doc/faq/axioms.png (cd doc/faq;\ $(PDFLATEX) -interaction=batchmode FAQ.v.tex;\ ../tools/show_latex_messages FAQ.v.log) doc/faq/FAQ.v.html: doc/faq/FAQ.v.dvi # to ensure FAQ.v.bbl (cd doc/faq; ($(HEVEA) $(HEVEAOPTS) FAQ.v.tex $(HEVEAFAQFILTER))) doc/faq/html/index.html: doc/faq/FAQ.v.html - rm -rf doc/faq/html $(MKDIR) doc/faq/html $(INSTALLLIB) doc/faq/interval_discr.v doc/faq/axioms.png doc/faq/html $(INSTALLLIB) doc/faq/FAQ.v.html doc/faq/html/index.html ###################################################################### # Standard library ###################################################################### ### Standard library (browsable html format) ifdef QUICK doc/stdlib/index-body.html: - rm -rf doc/stdlib/html $(MKDIR) doc/stdlib/html $(COQDOC) -q -boot -d doc/stdlib/html --multi-index --html -g \ -R theories Coq $(THEORIESVO:.vo=.v) mv doc/stdlib/html/index.html doc/stdlib/index-body.html else doc/stdlib/index-body.html: $(COQDOC) $(THEORIESVO) - rm -rf doc/stdlib/html $(MKDIR) doc/stdlib/html $(COQDOC) -q -boot -d doc/stdlib/html --multi-index --html -g \ -R theories Coq $(THEORIESVO:.vo=.v) mv doc/stdlib/html/index.html doc/stdlib/index-body.html endif doc/stdlib/index-list.html: doc/stdlib/index-list.html.template doc/stdlib/make-library-index ./doc/stdlib/make-library-index doc/stdlib/index-list.html doc/stdlib/html/index.html: doc/stdlib/index-list.html doc/stdlib/index-body.html doc/stdlib/index-trailer.html cat doc/stdlib/index-list.html > $@ sed -n -e '/