diff options
Diffstat (limited to 'Makefile.doc')
| -rw-r--r-- | Makefile.doc | 85 |
1 files changed, 55 insertions, 30 deletions
diff --git a/Makefile.doc b/Makefile.doc index 8cb9c9f0fa..4a247f1d94 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 @@ -44,25 +46,29 @@ else COQTEXOPTS:=-boot -n 72 -sl -small endif +# Sphinx-related variables +SPHINXOPTS= -j4 +SPHINXBUILD= sphinx-build +SPHINXBUILDDIR= doc/sphinx/_build + +# Internal variables. +ALLSPHINXOPTS= -d $(SPHINXBUILDDIR)/doctrees $(SPHINXOPTS) + 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-gal.v.tex \ RefMan-oth.v.tex RefMan-ltac.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 \ + RefMan-pro.v.tex \ + Coercion.v.tex Extraction.v.tex \ + Program.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-modr.tex \ - AsyncProofs.tex RefMan-ssr.tex) \ + RefMan-uti.tex \ + AsyncProofs.tex) \ $(REFMANCOQTEXFILES) \ REFMANEPSFILES:=doc/refman/coqide.eps doc/refman/coqide-queries.eps @@ -76,12 +82,18 @@ REFMANPNGFILES:=$(REFMANEPSFILES:.eps=.png) ### General rules ###################################################################### -.PHONY: doc doc-html doc-pdf doc-ps refman refman-quick tutorial +.PHONY: doc sphinxdoc-html doc-pdf doc-ps refman refman-quick tutorial .PHONY: stdlib full-stdlib rectutorial refman-html-dir INDEXURLS:=doc/refman/html/index_urls.txt -doc: refman tutorial rectutorial stdlib $(INDEXURLS) +doc: sphinx refman tutorial rectutorial stdlib $(INDEXURLS) + +sphinx: coq + $(SHOW)'SPHINXBUILD doc/sphinx' + $(HIDE)COQBIN="$(PWD)/bin" $(SPHINXBUILD) -b html $(ALLSPHINXOPTS) doc/sphinx $(SPHINXBUILDDIR)/html + @echo + @echo "Build finished. The HTML pages are in $(SPHINXBUILDDIR)/html." doc-html:\ doc/tutorial/Tutorial.v.html doc/refman/html/index.html \ @@ -345,9 +357,11 @@ 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) @@ -378,6 +392,12 @@ 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) @@ -385,10 +405,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 @@ -400,7 +420,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' @@ -410,13 +430,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 @@ -432,7 +452,12 @@ 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 $(OCAMLDOC_MLLIBD) @@ -449,7 +474,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) ########################################################################### # local web server |