diff options
Diffstat (limited to 'Makefile.doc')
| -rw-r--r-- | Makefile.doc | 125 |
1 files changed, 25 insertions, 100 deletions
diff --git a/Makefile.doc b/Makefile.doc index 07581748..a857ab80 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -10,10 +10,7 @@ # Makefile for the Coq documentation -# To compile documentation, you need the following tools: -# Dvi: latex (latex2e), bibtex, makeindex -# Pdf: pdflatex -# Html: hevea (http://hevea.inria.fr) >= 1.05 +# Read doc/README.md to learn about the dependencies # The main entry point : @@ -28,23 +25,18 @@ doc-no: ###################################################################### LATEX:=latex -BIBTEX:=BIBINPUTS=.: bibtex -min-crossrefs=10 MAKEINDEX:=makeindex PDFLATEX:=pdflatex DVIPS:=dvips -HEVEA:=hevea -HEVEAOPTS:=-fix -exec xxdate.exe -HEVEALIB:=/usr/local/lib/hevea:/usr/lib/hevea HTMLSTYLE:=coqremote -export TEXINPUTS:=$(HEVEALIB): -ifdef COQDOC_NOBOOT -COQTEXOPTS:=-n 72 -sl -small -else -COQTEXOPTS:=-boot -n 72 -sl -small -endif # Sphinx-related variables +SPHINXENV:=COQBIN="$(CURDIR)/bin/" SPHINXOPTS= -j4 +SPHINXWARNERROR ?= 0 +ifeq ($(SPHINXWARNERROR),1) +SPHINXOPTS += -W +endif SPHINXBUILD= sphinx-build SPHINXBUILDDIR= doc/sphinx/_build @@ -59,24 +51,23 @@ DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex .PHONY: doc doc-html doc-pdf doc-ps .PHONY: stdlib full-stdlib sphinx -.PHONY: tutorial rectutorial -doc: refman tutorial rectutorial stdlib +doc: refman stdlib ifndef QUICK SPHINX_DEPS := coq endif # refman-html and refman-latex -refman-%: coq +refman-%: $(SPHINX_DEPS) $(SHOW)'SPHINXBUILD doc/sphinx ($*)' - $(HIDE)COQBIN="$(abspath bin)" $(SPHINXBUILD) -b $* \ + $(HIDE)$(SPHINXENV) $(SPHINXBUILD) -b $* \ $(ALLSPHINXOPTS) doc/sphinx $(SPHINXBUILDDIR)/$* refman-pdf: refman-latex +$(MAKE) -C $(SPHINXBUILDDIR)/latex -refman: coq +refman: $(SPHINX_DEPS) +$(MAKE) refman-html +$(MAKE) refman-pdf @@ -84,19 +75,13 @@ refman: coq sphinx: refman-html doc-html:\ - doc/tutorial/Tutorial.v.html doc/stdlib/html/index.html \ - doc/RecTutorial/RecTutorial.html refman-html + doc/stdlib/html/index.html refman-html doc-pdf:\ - doc/tutorial/Tutorial.v.pdf doc/stdlib/Library.pdf \ - doc/RecTutorial/RecTutorial.pdf refman-pdf + doc/stdlib/Library.pdf refman-pdf doc-ps:\ - doc/tutorial/Tutorial.v.ps \ - doc/stdlib/Library.ps doc/RecTutorial/RecTutorial.ps - -tutorial: \ - doc/tutorial/Tutorial.v.html doc/tutorial/Tutorial.v.ps doc/tutorial/Tutorial.v.pdf + doc/stdlib/Library.ps stdlib: \ doc/stdlib/html/index.html doc/stdlib/Library.ps doc/stdlib/Library.pdf @@ -104,32 +89,14 @@ stdlib: \ full-stdlib: \ doc/stdlib/html/index.html doc/stdlib/FullLibrary.ps doc/stdlib/FullLibrary.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 $<`) ###################################################################### -# Macros for filtering outputs -###################################################################### - -HIDEBIBTEXINFO=| grep -v "^A level-1 auxiliary file" -SHOWMAKEINDEXERROR=egrep '^!! Input index error|^\*\* Input style error|^ --' - -###################################################################### # Common ###################################################################### @@ -139,23 +106,6 @@ doc/common/version.tex: config/Makefile printf '\\newcommand{\\coqversion}{$(VERSION)}' > doc/common/version.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) - -###################################################################### # Standard library ###################################################################### @@ -229,34 +179,13 @@ doc/stdlib/FullLibrary.pdf: $(DOCCOMMON) doc/stdlib/FullLibrary.coqdoc.tex doc/s ../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-sphinx + install-doc-sphinx install-doc-stdlib-html -install-doc: install-doc-meta install-doc-html install-doc-printable \ - install-doc-index-urls install-doc-sphinx +install-doc: install-doc-meta install-doc-html install-doc-printable install-doc-meta: $(MKDIR) $(FULLDOCDIR) @@ -267,17 +196,11 @@ install-doc-html: install-doc-stdlib-html install-doc-sphinx install-doc-stdlib-html: $(MKDIR) $(FULLDOCDIR)/html/stdlib $(INSTALLLIB) doc/stdlib/html/* $(FULLDOCDIR)/html/stdlib - $(INSTALLLIB) doc/RecTutorial/RecTutorial.html $(FULLDOCDIR)/html/RecTutorial.html - $(INSTALLLIB) doc/tutorial/Tutorial.v.html $(FULLDOCDIR)/html/Tutorial.html install-doc-printable: $(MKDIR) $(FULLDOCDIR)/ps $(FULLDOCDIR)/pdf $(INSTALLLIB) doc/stdlib/Library.pdf $(FULLDOCDIR)/pdf $(INSTALLLIB) 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/tutorial/Tutorial.v.ps $(FULLDOCDIR)/ps/Tutorial.ps - $(INSTALLLIB) doc/RecTutorial/RecTutorial.ps $(FULLDOCDIR)/ps/RecTutorial.ps install-doc-sphinx: $(MKDIR) $(FULLDOCDIR)/sphinx @@ -305,9 +228,11 @@ ODOCDOTOPTS=-dot -dot-reduce source-doc: mli-doc $(OCAMLDOCDIR)/coq.pdf +OCAMLDOC_CAML_FLAGS=-rectypes -I +threads $(MLINCLUDES) + $(OCAMLDOCDIR)/coq.tex: $(DOCMLIS:.mli=.cmi) $(SHOW)'OCAMLDOC -latex -o $@' - $(HIDE)$(OCAMLFIND) ocamldoc -latex -rectypes -I $(MYCAMLP5LIB) $(MLINCLUDES)\ + $(HIDE)$(OCAMLFIND) ocamldoc -latex $(OCAMLDOC_CAML_FLAGS) \ $(DOCMLIS) -noheader -t "Coq mlis documentation" \ -intro $(OCAMLDOCDIR)/docintro -o $@.tmp $(SHOW)'OCAMLDOC utf8 fix' @@ -317,31 +242,31 @@ $(OCAMLDOCDIR)/coq.tex: $(DOCMLIS:.mli=.cmi) mli-doc: $(DOCMLIS:.mli=.cmi) $(SHOW)'OCAMLDOC -html' - $(HIDE)$(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads -I $(MYCAMLP5LIB) $(MLINCLUDES) \ + $(HIDE)$(OCAMLFIND) ocamldoc -charset utf-8 -html $(OCAMLDOC_CAML_FLAGS) \ $(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 $(MYCAMLP5LIB) $(MLINCLUDES) \ + $(OCAMLFIND) ocamldoc -dot -dot-reduce $(OCAMLDOC_CAML_FLAGS) \ $(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 $@ $< + $(OCAMLFIND) ocamldoc $(OCAMLDOC_CAML_FLAGS) $(ODOCDOTOPTS) -dot-types -o $@ $< -OCAMLDOC_MLLIBD = $(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ \ +OCAMLDOC_MLLIBD = $(OCAMLFIND) ocamldoc $(OCAMLDOC_CAML_FLAGS) $(ODOCDOTOPTS) -o $@ \ $(foreach lib,$(|:.mllib.d=_MLLIB_DEPENDENCIES),$(addsuffix .ml,$($(lib)))) %.dot: | %.mllib.d $(OCAMLDOC_MLLIBD) -ml-doc: +ml-doc: kernel/copcodes.cmi $(SHOW)'OCAMLDOC -html' $(HIDE)mkdir -p $(OCAMLDOCDIR)/html/implementation - $(HIDE)$(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads $(MLINCLUDES) $(COQIDEFLAGS) \ + $(HIDE)$(OCAMLFIND) ocamldoc -charset utf-8 -html $(OCAMLDOC_CAML_FLAGS) \ $(DOCMLS) -d $(OCAMLDOCDIR)/html/implementation -colorize-code \ -t "Coq mls documentation" \ -css-style ../style.css @@ -356,7 +281,7 @@ tactics/tactics.dot: | tactics/tactics.mllib.d ltac/ltac.mllib.d $(OCAMLDOC_MLLIBD) %.dot: %.mli - $(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $< + $(OCAMLFIND) ocamldoc $(OCAMLDOC_CAML_FLAGS) $(ODOCDOTOPTS) -o $@ $< $(OCAMLDOCDIR)/%.pdf: $(OCAMLDOCDIR)/%.tex $(SHOW)'PDFLATEX $*.tex' |