diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
commit | 9043add656177eeac1491a73d2f3ab92bec0013c (patch) | |
tree | 2b0092c84bfbf718eca10c81f60b2640dc8cab05 /Makefile.doc | |
parent | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (diff) |
Imported Upstream version 8.8.2upstream/8.8.2
Diffstat (limited to 'Makefile.doc')
-rw-r--r-- | Makefile.doc | 273 |
1 files changed, 81 insertions, 192 deletions
diff --git a/Makefile.doc b/Makefile.doc index cdd9852e..07581748 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -1,10 +1,12 @@ -####################################################################### -# v # The Coq Proof Assistant / The Coq Development Team # -# <O___,, # INRIA-Rocquencourt & LRI-CNRS-Orsay # -# \VV/ ############################################################# -# // # This file is distributed under the terms of the # -# # GNU Lesser General Public License Version 2.1 # -####################################################################### +########################################################################## +## # The Coq Proof Assistant / The Coq Development Team ## +## v # INRIA, CNRS and contributors - Copyright 1999-2018 ## +## <O___,, # (see CREDITS file for the list of authors) ## +## \VV/ ############################################################### +## // # This file is distributed under the terms of the ## +## # GNU Lesser General Public License Version 2.1 ## +## # (see LICENSE file for the text of the license) ## +########################################################################## # Makefile for the Coq documentation @@ -30,69 +32,68 @@ 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 +HTMLSTYLE:=coqremote export TEXINPUTS:=$(HEVEALIB): +ifdef COQDOC_NOBOOT +COQTEXOPTS:=-n 72 -sl -small +else COQTEXOPTS:=-boot -n 72 -sl -small +endif -DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex +# Sphinx-related variables +SPHINXOPTS= -j4 +SPHINXBUILD= sphinx-build +SPHINXBUILDDIR= doc/sphinx/_build -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) +# Internal variables. +ALLSPHINXOPTS= -d $(SPHINXBUILDDIR)/doctrees $(SPHINXOPTS) -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) \ +DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex -REFMANEPSFILES:=doc/refman/coqide.eps doc/refman/coqide-queries.eps +###################################################################### +### General rules +###################################################################### -REFMANFILES:=$(REFMANTEXFILES) $(DOCCOMMON) $(REFMANEPSFILES) doc/refman/biblio.bib +.PHONY: doc doc-html doc-pdf doc-ps +.PHONY: stdlib full-stdlib sphinx +.PHONY: tutorial rectutorial -REFMANPNGFILES:=$(REFMANEPSFILES:.eps=.png) +doc: refman tutorial rectutorial stdlib +ifndef QUICK +SPHINX_DEPS := coq +endif -###################################################################### -### General rules -###################################################################### +# refman-html and refman-latex +refman-%: coq + $(SHOW)'SPHINXBUILD doc/sphinx ($*)' + $(HIDE)COQBIN="$(abspath bin)" $(SPHINXBUILD) -b $* \ + $(ALLSPHINXOPTS) doc/sphinx $(SPHINXBUILDDIR)/$* -.PHONY: doc doc-html doc-pdf doc-ps refman refman-quick tutorial -.PHONY: stdlib full-stdlib faq rectutorial refman-html-dir +refman-pdf: refman-latex + +$(MAKE) -C $(SPHINXBUILDDIR)/latex -INDEXURLS:=doc/refman/html/index_urls.txt +refman: coq + +$(MAKE) refman-html + +$(MAKE) refman-pdf -doc: refman faq tutorial rectutorial stdlib $(INDEXURLS) +# compatibility alias +sphinx: refman-html 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/tutorial/Tutorial.v.html doc/stdlib/html/index.html \ + doc/RecTutorial/RecTutorial.html refman-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/tutorial/Tutorial.v.pdf doc/stdlib/Library.pdf \ + doc/RecTutorial/RecTutorial.pdf refman-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 + 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 @@ -103,8 +104,6 @@ stdlib: \ 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 @@ -123,20 +122,6 @@ 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 ###################################################################### @@ -144,9 +129,6 @@ endif 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 ###################################################################### @@ -157,76 +139,6 @@ 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@.*>\([^<]*\)</span>.*, <a href="\([^"]*\)">.*@\1,\2@' > $@ - - -###################################################################### # Tutorial ###################################################################### @@ -243,33 +155,6 @@ doc/tutorial/Tutorial.v.pdf: $(DOCCOMMON) doc/tutorial/Tutorial.v.tex 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 ###################################################################### @@ -367,39 +252,39 @@ doc/RecTutorial/RecTutorial.html: doc/RecTutorial/RecTutorial.tex # Install all documentation files ###################################################################### -.PHONY: install-doc install-doc-meta install-doc-html install-doc-printable install-doc-index-urls +.PHONY: 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-index-urls +install-doc: install-doc-meta install-doc-html install-doc-printable \ + install-doc-index-urls install-doc-sphinx 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 +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/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/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/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) +install-doc-sphinx: + $(MKDIR) $(FULLDOCDIR)/sphinx + (for f in `cd doc/sphinx/_build; find . -type f`; do \ + $(MKDIR) $$(dirname $(FULLDOCDIR)/sphinx/$$f);\ + $(INSTALLLIB) doc/sphinx/_build/$$f $(FULLDOCDIR)/sphinx/$$f;\ + done) ########################################################################### # Documentation of the source code (using ocamldoc) @@ -407,10 +292,10 @@ install-doc-index-urls: 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) +DOCMLLIBS= $(CORECMA:.cma=_MLLIB_DEPENDENCIES) $(PLUGINSCMO:.cmo=_MLPACK_DEPENDENCIES) +DOCMLS=$(foreach lib,$(DOCMLLIBS),$(addsuffix .ml, $($(lib)))) + +DOCMLIS=$(wildcard $(addsuffix /*.mli, $(SRCDIRS))) # Defining options to generate dependencies graphs DOT=dot @@ -422,7 +307,7 @@ 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)\ + $(HIDE)$(OCAMLFIND) ocamldoc -latex -rectypes -I $(MYCAMLP5LIB) $(MLINCLUDES)\ $(DOCMLIS) -noheader -t "Coq mlis documentation" \ -intro $(OCAMLDOCDIR)/docintro -o $@.tmp $(SHOW)'OCAMLDOC utf8 fix' @@ -432,13 +317,13 @@ $(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 $(MYCAMLP4LIB) $(MLINCLUDES) \ + $(HIDE)$(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads -I $(MYCAMLP5LIB) $(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) \ + $(OCAMLFIND) ocamldoc -dot -dot-reduce -rectypes -I +threads -I $(CAMLLIB) -I $(MYCAMLP5LIB) $(MLINCLUDES) \ $(filter $(addsuffix /%.ml,$(CORESRCDIRS)),$(MLFILES)) -o $(OCAMLDOCDIR)/coq.dot %_dep.png: %.dot @@ -454,9 +339,14 @@ OCAMLDOC_MLLIBD = $(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) - $(OCAMLDOC_MLLIBD) ml-doc: - $(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads $(MLINCLUDES) $(COQIDEFLAGS) -d $(OCAMLDOCDIR) $(MLSTATICFILES) + $(SHOW)'OCAMLDOC -html' + $(HIDE)mkdir -p $(OCAMLDOCDIR)/html/implementation + $(HIDE)$(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads $(MLINCLUDES) $(COQIDEFLAGS) \ + $(DOCMLS) -d $(OCAMLDOCDIR)/html/implementation -colorize-code \ + -t "Coq mls documentation" \ + -css-style ../style.css -parsing/parsing.dot : | parsing/parsing.mllib.d parsing/highparsing.mllib.d +parsing/parsing.dot : | parsing/parsing.mllib.d $(OCAMLDOC_MLLIBD) grammar/grammar.dot : | grammar/grammar.mllib.d @@ -471,8 +361,7 @@ tactics/tactics.dot: | tactics/tactics.mllib.d ltac/ltac.mllib.d $(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) - + $(HIDE)(cd doc/tools/; ./show_latex_messages -no-overfull ../../$(OCAMLDOCDIR)/$*.log) # For emacs: # Local Variables: |