diff options
Diffstat (limited to 'Makefile.doc')
-rw-r--r-- | Makefile.doc | 184 |
1 files changed, 115 insertions, 69 deletions
diff --git a/Makefile.doc b/Makefile.doc index 54fa5f80..aff812db 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -13,56 +13,62 @@ .PHONY: doc doc-html doc-pdf doc-ps refman tutorial stdlib faq rectutorial -doc: doc-html doc-pdf doc-ps ide/index_urls.txt +doc: refman faq tutorial rectutorial stdlib ide/index_urls.txt 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.v.html + doc/faq/html/index.html doc/stdlib/html/index.html doc/RecTutorial/RecTutorial.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.v.pdf + doc/faq/FAQ.v.pdf doc/stdlib/Library.pdf doc/RecTutorial/RecTutorial.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.v.ps + doc/faq/FAQ.v.ps doc/stdlib/Library.ps doc/RecTutorial/RecTutorial.ps -refman: coq - $(MAKE) -f Makefile.stage3 refman-nodep - -refman-nodep:\ +refman: \ doc/refman/html/index.html doc/refman/Reference-Manual.ps doc/refman/Reference-Manual.pdf -tutorial:\ +tutorial: \ doc/tutorial/Tutorial.v.html doc/tutorial/Tutorial.v.ps doc/tutorial/Tutorial.v.pdf -stdlib: $(THEORIESVO) $(COQDOC) - $(MAKE) -f Makefile.stage3 stdlib-nodep - -stdlib-nodep:\ +stdlib: \ doc/stdlib/html/index.html doc/stdlib/Library.ps doc/stdlib/Library.pdf faq:\ doc/faq/html/index.html doc/faq/FAQ.v.ps doc/faq/FAQ.v.pdf rectutorial:\ - doc/RecTutorial/RecTutorial.v.html \ - doc/RecTutorial/RecTutorial.v.ps doc/RecTutorial/RecTutorial.v.pdf + doc/RecTutorial/RecTutorial.html \ + doc/RecTutorial/RecTutorial.ps doc/RecTutorial/RecTutorial.pdf ###################################################################### ### Implicit rules ###################################################################### +ifeq ($(QUICK),1) %.v.tex: %.tex (cd `dirname $<`; $(COQSRC)/$(COQTEX) $(COQTEXOPTS) `basename $<`) +else +%.v.tex: %.tex | $(COQTEX) $(COQTOPEXE) $(CONTRIBVO) $(CONTRIBCMO) $(THEORIESVO) + (cd `dirname $<`; $(COQSRC)/$(COQTEX) $(COQTEXOPTS) `basename $<`) +endif %.ps: %.dvi - (cd `dirname $<`; dvips -o `basename $@` `basename $<`) + (cd `dirname $<`; dvips -q -o `basename $@` `basename $<`) %.eps: %.png pngtopnm $< | pnmtops -equalpixels -noturn -rle > $@ ###################################################################### +# Macros for filtering outputs +###################################################################### + +HIDEBIBTEXINFO=| grep -v "^A level-1 auxiliary file" +SHOWMAKEINDEXERROR=egrep '^!! Input index error|^\*\* Input style error|^ --' + +###################################################################### # Common ###################################################################### @@ -75,55 +81,71 @@ doc/common/version.tex: config/Makefile # 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: $(DOCCOMMON) $(REFMANFILES) doc/refman/Reference-Manual.tex - (cd doc/refman;\ - $(LATEX) Reference-Manual;\ - $(BIBTEX) Reference-Manual;\ - $(LATEX) Reference-Manual;\ - $(MAKEINDEX) Reference-Manual;\ - $(MAKEINDEX) Reference-Manual.tacidx -o Reference-Manual.tacind;\ - $(MAKEINDEX) Reference-Manual.comidx -o Reference-Manual.comind;\ - $(MAKEINDEX) Reference-Manual.erridx -o Reference-Manual.errind;\ - $(LATEX) Reference-Manual;\ - $(LATEX) Reference-Manual) + @(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.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: $(DOCCOMMON) $(REFMANFILES) doc/refman/Reference-Manual.tex - (cd doc/refman; $(PDFLATEX) Reference-Manual.tex) + (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/headers.hva doc/refman/Reference-Manual.dvi # to ensure bbl file - (cd doc/refman; $(HEVEA) $(HEVEAOPTS) ./Reference-Manual.tex) +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 + $(INSTALLLIB) $< doc/refman + +doc/refman/styles.hva: doc/common/styles/html/$(HTMLSTYLE)/styles.hva + $(INSTALLLIB) $< doc/refman doc/refman/html/index.html: doc/refman/Reference-Manual.html $(REFMANPNGFILES) \ - doc/refman/cover.html doc/refman/index.html + 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 -o toc.html ../Reference-Manual.html) - $(INSTALLLIB) doc/refman/cover.html doc/refman/menu.html doc/refman/html - $(INSTALLLIB) doc/refman/index.html 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) Reference-Manual.tex; \ - $(HEVEA) $(HEVEAOPTS) ./Reference-Manual.tex) - + (cd doc/refman;\ + $(PDFLATEX) -interaction=batchmode Reference-Manual.tex;\ + ../tools/show_latex_messages -no-overfull Reference-Manual.log && \ + $(HEVEA) $(HEVEAOPTS) ./Reference-Manual.tex) ###################################################################### # Tutorial ###################################################################### doc/tutorial/Tutorial.v.dvi: $(DOCCOMMON) doc/tutorial/Tutorial.v.tex - (cd doc/tutorial; $(LATEX) Tutorial.v) + (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) 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) @@ -135,13 +157,16 @@ doc/tutorial/Tutorial.v.html: $(DOCCOMMON) doc/tutorial/Tutorial.v.tex doc/faq/FAQ.v.dvi: doc/common/version.tex doc/common/title.tex doc/faq/FAQ.v.tex (cd doc/faq;\ - $(LATEX) FAQ.v;\ - $(BIBTEX) FAQ.v;\ - $(LATEX) FAQ.v;\ - $(LATEX) FAQ.v) + $(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.png - (cd doc/faq; $(PDFLATEX) FAQ.v.tex) + (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 # to ensure FAQ.v.bbl (cd doc/faq; $(HEVEA) $(HEVEAOPTS) FAQ.v.tex) @@ -158,15 +183,24 @@ doc/faq/html/index.html: doc/faq/FAQ.v.html ### Standard library (browsable html format) -doc/stdlib/index-body.html: +ifeq ($(QUICK),1) +doc/stdlib/index-body.html: - rm -rf doc/stdlib/html $(MKDIR) doc/stdlib/html - $(COQDOC) -q -d doc/stdlib/html --multi-index --html \ + $(COQDOC) -q -d doc/stdlib/html --multi-index --html -g \ -R theories Coq $(THEORIESVO:.vo=.v) mv doc/stdlib/html/index.html doc/stdlib/index-body.html +else +doc/stdlib/index-body.html: | $(COQDOC) $(THEORIESVO) + - rm -rf doc/stdlib/html + $(MKDIR) doc/stdlib/html + $(COQDOC) -q -d doc/stdlib/html --multi-index --html -g \ + -R theories Coq $(THEORIESVO:.vo=.v) + mv doc/stdlib/html/index.html doc/stdlib/index-body.html +endif -doc/stdlib/index-list.html: doc/stdlib/index-list.html.template - COQTOP=$(COQSRC) ./doc/stdlib/make-library-index doc/stdlib/index-list.html +doc/stdlib/index-list.html: doc/stdlib/index-list.html.template doc/stdlib/make-library-index + ./doc/stdlib/make-library-index doc/stdlib/index-list.html doc/stdlib/html/index.html: doc/stdlib/index-list.html doc/stdlib/index-body.html doc/stdlib/index-trailer.html cat doc/stdlib/index-list.html > $@ @@ -175,34 +209,46 @@ doc/stdlib/html/index.html: doc/stdlib/index-list.html doc/stdlib/index-body.htm ### Standard library (light version, full version is definitely too big) -doc/stdlib/Library.coqdoc.tex: - $(COQSRC)/$(COQDOC) -q --gallina --body-only --latex --stdout \ +ifeq ($(QUICK),1) +doc/stdlib/Library.coqdoc.tex: + $(COQDOC) -q -boot --gallina --body-only --latex --stdout \ + -R theories Coq $(THEORIESLIGHTVO:.vo=.v) >> $@ +else +doc/stdlib/Library.coqdoc.tex: | $(COQDOC) $(THEORIESLIGHTVO) + $(COQDOC) -q -boot --gallina --body-only --latex --stdout \ -R theories Coq $(THEORIESLIGHTVO:.vo=.v) >> $@ +endif doc/stdlib/Library.dvi: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Library.tex (cd doc/stdlib;\ - $(LATEX) Library;\ - $(LATEX) Library) + $(LATEX) -interaction=batchmode Library;\ + $(LATEX) -interaction=batchmode Library > /dev/null;\ + ../tools/show_latex_messages Library.log) doc/stdlib/Library.pdf: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Library.dvi - (cd doc/stdlib; $(PDFLATEX) Library) + (cd doc/stdlib;\ + $(PDFLATEX) -interaction=batchmode Library;\ + ../tools/show_latex_messages Library.log) ###################################################################### # Tutorial on inductive types ###################################################################### -doc/RecTutorial/RecTutorial.v.dvi: doc/common/version.tex doc/common/title.tex doc/RecTutorial/RecTutorial.v.tex +doc/RecTutorial/RecTutorial.dvi: doc/common/version.tex doc/common/title.tex doc/RecTutorial/RecTutorial.tex (cd doc/RecTutorial;\ - $(LATEX) RecTutorial.v;\ - $(BIBTEX) RecTutorial.v;\ - $(LATEX) RecTutorial.v;\ - $(LATEX) RecTutorial.v) + $(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.v.pdf: doc/common/version.tex doc/common/title.tex doc/RecTutorial/RecTutorial.v.dvi - (cd doc/RecTutorial; $(PDFLATEX) RecTutorial.v.tex) +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.v.html: doc/RecTutorial/RecTutorial.v.tex - (cd doc/RecTutorial; $(HEVEA) $(HEVEAOPTS) RecTutorial.v) +doc/RecTutorial/RecTutorial.html: doc/RecTutorial/RecTutorial.tex + (cd doc/RecTutorial; $(HEVEA) $(HEVEAOPTS) RecTutorial) ###################################################################### # Index file for CoqIDE @@ -210,7 +256,7 @@ doc/RecTutorial/RecTutorial.v.html: doc/RecTutorial/RecTutorial.v.tex # Not robust, improve... ide/index_urls.txt: doc/refman/html/index.html - - rm ide/index_urls.txt + @ rm -f ide/index_urls.txt cat doc/refman/html/command-index.html doc/refman/html/tactic-index.html | grep li-indexenv | grep HREF | sed -e 's@.*<TT>\(.*\)</TT>.*, <A HREF="\(.*\)">.*@\1,\2@' > ide/index_urls.txt @@ -224,23 +270,23 @@ install-doc-meta: $(MKDIR) $(FULLDOCDIR) $(INSTALLLIB) doc/LICENSE $(FULLDOCDIR)/LICENSE.doc -install-doc-html: doc-html +install-doc-html: $(MKDIR) $(addprefix $(FULLDOCDIR)/html/, refman stdlib faq) $(INSTALLLIB) doc/refman/html/* $(FULLDOCDIR)/html/refman $(INSTALLLIB) doc/stdlib/html/* $(FULLDOCDIR)/html/stdlib - $(INSTALLLIB) doc/RecTutorial/RecTutorial.v.html $(FULLDOCDIR)/html/RecTutorial.html + $(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: doc-pdf doc-ps +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.v.pdf $(FULLDOCDIR)/pdf/RecTutorial.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.v.ps $(FULLDOCDIR)/ps/RecTutorial.ps + $(INSTALLLIB) doc/RecTutorial/RecTutorial.ps $(FULLDOCDIR)/ps/RecTutorial.ps $(INSTALLLIB) doc/faq/FAQ.v.ps $(FULLDOCDIR)/ps/FAQ.ps |