Imported Upstream version 8.8.2upstream/8.8.2

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: