####################################################################### # v # The Coq Proof Assistant / The Coq Development Team # # = 1.05 # The main entry point : documentation: doc-$(WITHDOC) ## see $(WITHDOC) in config/Makefile doc-all: doc doc-no: .PHONY: documentation doc-all doc-no ###################################################################### ### Variables ###################################################################### LATEX:=latex BIBTEX:=BIBINPUTS=.: bibtex -min-crossrefs=10 MAKEINDEX:=makeindex PDFLATEX:=pdflatex DVIPS:=dvips FIG2DEV:=fig2dev CONVERT:=convert HEVEA:=hevea HACHA:=hacha HEVEAOPTS:=-fix -exec xxdate.exe HEVEALIB:=/usr/local/lib/hevea:/usr/lib/hevea HTMLSTYLE:=simple export TEXINPUTS:=$(HEVEALIB): COQTEXOPTS:=-boot -n 72 -sl -small DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex REFMANCOQTEXFILES:=$(addprefix doc/refman/, \ RefMan-gal.v.tex RefMan-ext.v.tex \ RefMan-mod.v.tex RefMan-tac.v.tex \ RefMan-cic.v.tex RefMan-lib.v.tex \ RefMan-tacex.v.tex RefMan-syn.v.tex \ RefMan-oth.v.tex RefMan-ltac.v.tex \ RefMan-decl.v.tex RefMan-pro.v.tex RefMan-sch.v.tex \ Cases.v.tex Coercion.v.tex CanonicalStructures.v.tex Extraction.v.tex \ Program.v.tex Omega.v.tex Micromega.v.tex Polynom.v.tex Nsatz.v.tex \ Setoid.v.tex Classes.v.tex Universes.v.tex \ Misc.v.tex) REFMANTEXFILES:=$(addprefix doc/refman/, \ headers.sty Reference-Manual.tex \ RefMan-pre.tex RefMan-int.tex RefMan-com.tex \ RefMan-uti.tex RefMan-ide.tex RefMan-add.tex RefMan-modr.tex \ AsyncProofs.tex ) \ $(REFMANCOQTEXFILES) \ REFMANEPSFILES:=doc/refman/coqide.eps doc/refman/coqide-queries.eps REFMANFILES:=$(REFMANTEXFILES) $(DOCCOMMON) $(REFMANEPSFILES) doc/refman/biblio.bib REFMANPNGFILES:=$(REFMANEPSFILES:.eps=.png) ###################################################################### ### General rules ###################################################################### .PHONY: doc doc-html doc-pdf doc-ps refman refman-quick tutorial .PHONY: stdlib full-stdlib faq rectutorial refman-html-dir INDEXURLS:=doc/refman/html/index_urls.txt doc: refman faq tutorial rectutorial stdlib $(INDEXURLS) 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 full-stdlib: \ doc/stdlib/html/index.html doc/stdlib/FullLibrary.ps doc/stdlib/FullLibrary.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 $(COQTEX) $(COQTEXOPTS) $< else %.v.tex: %.tex $(COQTEX) $(COQTOPEXE) $(ALLVO) $(COQTEX) $(COQTEXOPTS) $< endif %.ps: %.dvi (cd `dirname $<`; $(DVIPS) -q -o `basename $@` `basename $<`) %.png: %.fig $(FIG2DEV) -L png -m 2 $< $@ %.pdf: %.fig $(FIG2DEV) -L pdftex $< $@ $(FIG2DEV) -L pdftex_t -p `basename $@` $< $@_t %.eps: %.fig $(FIG2DEV) -L pstex $< $@ $(FIG2DEV) -L pstex_t -p `basename $@` $< $@_t %.eps: %.png $(CONVERT) $< $@ ###################################################################### # 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.optidx -o Reference-Manual.optind;\ $(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: doc/refman/Reference-Manual.dvi $(REFMANPNGFILES) (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 sed -e "s/COQVERSION/$(VERSION)/g" $< > $@ doc/refman/styles.hva: doc/common/styles/html/$(HTMLSTYLE)/styles.hva $(INSTALLLIB) $< doc/refman INDEXES:= doc/refman/html/command-index.html doc/refman/html/tactic-index.html ALLINDEXES:= doc/refman/html/index.html $(INDEXES) refman-html-dir $(ALLINDEXES): 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) ###################################################################### # Index file for CoqIDE ###################################################################### $(INDEXURLS): $(INDEXES) cat $< | grep li-indexenv | grep href= | sed -e 's@.*>\([^<]*\).*, .*@\1,\2@' > $@ ###################################################################### # 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 doc/faq/axioms.eps (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.pdf (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 doc/faq/axioms.png # 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/html/genindex.html: else doc/stdlib/html/genindex.html: | $(COQDOC) $(ALLVO) endif - rm -rf doc/stdlib/html $(MKDIR) doc/stdlib/html $(COQDOC) -q -d doc/stdlib/html --with-header doc/common/styles/html/$(HTMLSTYLE)/header.html --with-footer doc/common/styles/html/$(HTMLSTYLE)/footer.html --multi-index --html -g \ -R theories Coq -R plugins Coq $(VFILES) mv doc/stdlib/html/index.html doc/stdlib/html/genindex.html 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/hidden-files doc/stdlib/html/index.html: doc/stdlib/html/genindex.html doc/stdlib/index-list.html cat doc/common/styles/html/$(HTMLSTYLE)/header.html doc/stdlib/index-list.html > $@ cat doc/common/styles/html/$(HTMLSTYLE)/footer.html >> $@ ### Standard library (light version, full version is definitely too big) ifdef QUICK doc/stdlib/Library.coqdoc.tex: else doc/stdlib/Library.coqdoc.tex: | $(COQDOC) $(THEORIESLIGHTVO) endif $(COQDOC) -q -boot --gallina --body-only --latex --stdout \ -R theories Coq $(THEORIESLIGHTVO:.vo=.v) >> $@ doc/stdlib/Library.dvi: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Library.tex (cd doc/stdlib;\ $(LATEX) -interaction=batchmode Library;\ $(LATEX) -interaction=batchmode Library > /dev/null;\ ../tools/show_latex_messages -no-overfull Library.log) doc/stdlib/Library.pdf: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Library.dvi (cd doc/stdlib;\ $(PDFLATEX) -interaction=batchmode Library;\ ../tools/show_latex_messages -no-overfull Library.log) ### Standard library (full version if you're crazy enouth to try) doc/stdlib/FullLibrary.tex: doc/stdlib/Library.tex sed -e 's/Library.coqdoc/FullLibrary.coqdoc/g;s/\\begin{document}/\\newcommand{\\textlambda}{\\ensuremath{\\lambda}}\\newcommand{\\textPi}{\\ensuremath{\\Pi}}\\begin{document}/' $< > $@ ifdef QUICK doc/stdlib/FullLibrary.coqdoc.tex: $(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \ -R theories Coq -R plugins Coq $(VFILES) > $@ sed -i.tmp -e 's///g' $@ && rm $@.tmp else doc/stdlib/FullLibrary.coqdoc.tex: $(COQDOC) $(ALLVO) $(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \ -R theories Coq -R plugins Coq $(VFILES) > $@ sed -i.tmp -e 's///g' $@ && rm $@.tmp endif doc/stdlib/FullLibrary.dvi: $(DOCCOMMON) doc/stdlib/FullLibrary.coqdoc.tex doc/stdlib/FullLibrary.tex (cd doc/stdlib;\ $(LATEX) -interaction=batchmode FullLibrary;\ $(LATEX) -interaction=batchmode FullLibrary > /dev/null;\ ../tools/show_latex_messages -no-overfull FullLibrary.log) doc/stdlib/FullLibrary.pdf: $(DOCCOMMON) doc/stdlib/FullLibrary.coqdoc.tex doc/stdlib/FullLibrary.dvi (cd doc/stdlib;\ $(PDFLATEX) -interaction=batchmode FullLibrary;\ ../tools/show_latex_messages -no-overfull FullLibrary.log) ###################################################################### # Tutorial on inductive types ###################################################################### doc/RecTutorial/RecTutorial.dvi: doc/common/version.tex doc/common/title.tex doc/RecTutorial/RecTutorial.tex (cd doc/RecTutorial;\ $(LATEX) -interaction=batchmode RecTutorial;\ $(BIBTEX) -terse RecTutorial;\ $(LATEX) -interaction=batchmode RecTutorial > /dev/null;\ $(LATEX) -interaction=batchmode RecTutorial > /dev/null;\ ../tools/show_latex_messages RecTutorial.log) doc/RecTutorial/RecTutorial.pdf: doc/common/version.tex doc/common/title.tex doc/RecTutorial/RecTutorial.dvi (cd doc/RecTutorial;\ $(PDFLATEX) -interaction=batchmode RecTutorial.tex;\ ../tools/show_latex_messages RecTutorial.log) doc/RecTutorial/RecTutorial.html: doc/RecTutorial/RecTutorial.tex (cd doc/RecTutorial; $(HEVEA) $(HEVEAOPTS) RecTutorial) ###################################################################### # Install all documentation files ###################################################################### .PHONY: install-doc install-doc-meta install-doc-html install-doc-printable install-doc-index-urls install-doc: install-doc-meta install-doc-html install-doc-printable install-doc-index-urls install-doc-meta: $(MKDIR) $(FULLDOCDIR) $(INSTALLLIB) doc/LICENSE $(FULLDOCDIR)/LICENSE.doc install-doc-html: $(MKDIR) $(addprefix $(FULLDOCDIR)/html/, refman stdlib faq) $(INSTALLLIB) doc/refman/html/* $(FULLDOCDIR)/html/refman $(INSTALLLIB) doc/stdlib/html/* $(FULLDOCDIR)/html/stdlib $(INSTALLLIB) doc/RecTutorial/RecTutorial.html $(FULLDOCDIR)/html/RecTutorial.html $(INSTALLLIB) doc/faq/html/* $(FULLDOCDIR)/html/faq $(INSTALLLIB) doc/tutorial/Tutorial.v.html $(FULLDOCDIR)/html/Tutorial.html install-doc-printable: $(MKDIR) $(FULLDOCDIR)/ps $(FULLDOCDIR)/pdf $(INSTALLLIB) doc/refman/Reference-Manual.pdf \ doc/stdlib/Library.pdf $(FULLDOCDIR)/pdf $(INSTALLLIB) doc/refman/Reference-Manual.ps \ doc/stdlib/Library.ps $(FULLDOCDIR)/ps $(INSTALLLIB) doc/tutorial/Tutorial.v.pdf $(FULLDOCDIR)/pdf/Tutorial.pdf $(INSTALLLIB) doc/RecTutorial/RecTutorial.pdf $(FULLDOCDIR)/pdf/RecTutorial.pdf $(INSTALLLIB) doc/faq/FAQ.v.pdf $(FULLDOCDIR)/pdf/FAQ.pdf $(INSTALLLIB) doc/tutorial/Tutorial.v.ps $(FULLDOCDIR)/ps/Tutorial.ps $(INSTALLLIB) doc/RecTutorial/RecTutorial.ps $(FULLDOCDIR)/ps/RecTutorial.ps $(INSTALLLIB) doc/faq/FAQ.v.ps $(FULLDOCDIR)/ps/FAQ.ps install-doc-index-urls: $(MKDIR) $(FULLDATADIR) $(INSTALLLIB) $(INDEXURLS) $(FULLDATADIR) ########################################################################### # Documentation of the source code (using ocamldoc) ########################################################################### OCAMLDOCDIR=dev/ocamldoc DOCMLIS=$(wildcard ./lib/*.mli ./intf/*.mli ./kernel/*.mli ./library/*.mli \ ./engine/*.mli ./pretyping/*.mli ./interp/*.mli printing/*.mli \ ./parsing/*.mli ./proofs/*.mli \ ./tactics/*.mli ./stm/*.mli ./toplevel/*.mli ./ltac/*.mli) # Defining options to generate dependencies graphs DOT=dot ODOCDOTOPTS=-dot -dot-reduce .PHONY: source-doc mli-doc ml-doc source-doc: mli-doc $(OCAMLDOCDIR)/coq.pdf $(OCAMLDOCDIR)/coq.tex: $(DOCMLIS:.mli=.cmi) $(SHOW)'OCAMLDOC -latex -o $@' $(HIDE)$(OCAMLFIND) ocamldoc -latex -rectypes -I $(MYCAMLP4LIB) $(MLINCLUDES)\ $(DOCMLIS) -noheader -t "Coq mlis documentation" \ -intro $(OCAMLDOCDIR)/docintro -o $@.tmp $(SHOW)'OCAMLDOC utf8 fix' $(HIDE)$(OCAMLDOCDIR)/fix-ocamldoc-utf8 $@.tmp $(HIDE)cat $(OCAMLDOCDIR)/header.tex $@.tmp > $@ rm $@.tmp mli-doc: $(DOCMLIS:.mli=.cmi) $(SHOW)'OCAMLDOC -html' $(HIDE)$(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads -I $(MYCAMLP4LIB) $(MLINCLUDES) \ $(DOCMLIS) -d $(OCAMLDOCDIR)/html -colorize-code \ -t "Coq mlis documentation" -intro $(OCAMLDOCDIR)/docintro \ -css-style style.css ml-dot: $(MLFILES) $(OCAMLFIND) ocamldoc -dot -dot-reduce -rectypes -I +threads -I $(CAMLLIB) -I $(MYCAMLP4LIB) $(MLINCLUDES) \ $(filter $(addsuffix /%.ml,$(CORESRCDIRS)),$(MLFILES)) -o $(OCAMLDOCDIR)/coq.dot %_dep.png: %.dot $(DOT) -Tpng $< -o $@ %_types.dot: %.mli $(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -dot-types -o $@ $< OCAMLDOC_MLLIBD = $(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ \ $(foreach lib,$(|:.mllib.d=_MLLIB_DEPENDENCIES),$(addsuffix .ml,$($(lib)))) %.dot: | %.mllib.d $(OCAMLDOC_MLLIBD) ml-doc: $(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads $(MLINCLUDES) $(COQIDEFLAGS) -d $(OCAMLDOCDIR) $(MLSTATICFILES) parsing/parsing.dot : | parsing/parsing.mllib.d parsing/highparsing.mllib.d $(OCAMLDOC_MLLIBD) grammar/grammar.dot : | grammar/grammar.mllib.d $(OCAMLDOC_MLLIBD) tactics/tactics.dot: | tactics/tactics.mllib.d ltac/ltac.mllib.d $(OCAMLDOC_MLLIBD) %.dot: %.mli $(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $< $(OCAMLDOCDIR)/%.pdf: $(OCAMLDOCDIR)/%.tex $(SHOW)'PDFLATEX $*.tex' $(HIDE)(cd $(OCAMLDOCDIR) ; pdflatex -interaction=batchmode $*.tex && pdflatex -interaction=batchmode $*.tex) $(HIDE)(cd doc/tools/; show_latex_messages -no-overfull ../../$(OCAMLDOCDIR)/$*.log) # For emacs: # Local Variables: # mode: makefile # End: