diff options
Diffstat (limited to 'Makefile.doc')
| -rw-r--r-- | Makefile.doc | 249 |
1 files changed, 21 insertions, 228 deletions
diff --git a/Makefile.doc b/Makefile.doc index fc791ce1c..dde3a37b7 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 INSTALL.doc to learn about the dependencies # The main entry point : @@ -28,25 +25,13 @@ doc-no: ###################################################################### 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:=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 SPHINXBUILD= sphinx-build SPHINXBUILDDIR= doc/sphinx/_build @@ -56,58 +41,33 @@ 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-oth.v.tex RefMan-ltac.v.tex \ - RefMan-pro.v.tex \ - Universes.v.tex) - -REFMANTEXFILES:=$(addprefix doc/refman/, \ - headers.sty Reference-Manual.tex \ - RefMan-uti.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 sphinxdoc-html doc-pdf doc-ps refman refman-quick tutorial -.PHONY: stdlib full-stdlib rectutorial refman-html-dir +.PHONY: doc doc-html doc-pdf doc-ps +.PHONY: stdlib full-stdlib -INDEXURLS:=doc/refman/html/index_urls.txt +doc: sphinx stdlib -doc: sphinx refman tutorial rectutorial stdlib $(INDEXURLS) +ifndef QUICK +SPHINX_DEPS := coq +endif -sphinx: coq +sphinx: $(SPHINX_DEPS) $(SHOW)'SPHINXBUILD doc/sphinx' - $(HIDE)COQBIN="$(PWD)/bin" $(SPHINXBUILD) -b html $(ALLSPHINXOPTS) doc/sphinx $(SPHINXBUILDDIR)/html + $(HIDE)$(SPHINXENV) $(SPHINXBUILD) -W -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 \ - doc/stdlib/html/index.html doc/RecTutorial/RecTutorial.html + doc/stdlib/html/index.html sphinx doc-pdf:\ - doc/tutorial/Tutorial.v.pdf doc/refman/Reference-Manual.pdf \ - doc/stdlib/Library.pdf doc/RecTutorial/RecTutorial.pdf + doc/stdlib/Library.pdf doc-ps:\ - doc/tutorial/Tutorial.v.ps doc/refman/Reference-Manual.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 + doc/stdlib/Library.ps stdlib: \ doc/stdlib/html/index.html doc/stdlib/Library.ps doc/stdlib/Library.pdf @@ -115,45 +75,13 @@ 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 $<`) -%.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|^ --' - ###################################################################### # Common ###################################################################### @@ -164,99 +92,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 - -refman-html-dir $(INDEXES): doc/refman/html/index.html ; - -doc/refman/html/index.html: 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 - @touch $(INDEXES) - (cd doc/common/styles/html/$(HTMLSTYLE);\ - for f in `find . -name \*.css`; do \ - $(MKDIR) $$(dirname ../../../../refman/html/$$f);\ - $(INSTALLLIB) $$f ../../../../refman/html/$$f;\ - done) - -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 -###################################################################### - -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 ###################################################################### @@ -330,63 +165,28 @@ 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) $(INSTALLLIB) doc/LICENSE $(FULLDOCDIR)/LICENSE.doc -install-doc-html: - $(MKDIR) $(addprefix $(FULLDOCDIR)/html/, refman stdlib) - (for f in `cd doc/refman/html; find . -type f`; do \ - $(MKDIR) $$(dirname $(FULLDOCDIR)/html/refman/$$f);\ - $(INSTALLLIB) doc/refman/html/$$f $(FULLDOCDIR)/html/refman/$$f;\ - done) +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/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/tutorial/Tutorial.v.ps $(FULLDOCDIR)/ps/Tutorial.ps - $(INSTALLLIB) doc/RecTutorial/RecTutorial.ps $(FULLDOCDIR)/ps/RecTutorial.ps - -install-doc-index-urls: - $(MKDIR) $(FULLDATADIR) - $(INSTALLLIB) $(INDEXURLS) $(FULLDATADIR) + $(INSTALLLIB) doc/stdlib/Library.pdf $(FULLDOCDIR)/pdf + $(INSTALLLIB) doc/stdlib/Library.ps $(FULLDOCDIR)/ps install-doc-sphinx: $(MKDIR) $(FULLDOCDIR)/sphinx @@ -472,13 +272,6 @@ $(OCAMLDOCDIR)/%.pdf: $(OCAMLDOCDIR)/%.tex $(HIDE)(cd $(OCAMLDOCDIR) ; pdflatex -interaction=batchmode $*.tex && pdflatex -interaction=batchmode $*.tex) $(HIDE)(cd doc/tools/; ./show_latex_messages -no-overfull ../../$(OCAMLDOCDIR)/$*.log) -########################################################################### -# local web server -########################################################################### - -serve-refman-8080: refman - cd doc/refman/html; python3 -m http.server 8080 - # For emacs: # Local Variables: # mode: makefile |