From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- Makefile.doc | 82 ++++++++++++++++++++++++++++++++++++++---------------------- 1 file changed, 52 insertions(+), 30 deletions(-) (limited to 'Makefile.doc') diff --git a/Makefile.doc b/Makefile.doc index f481d681..56daaa85 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -36,22 +36,20 @@ tutorial: \ 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 +faq: doc/faq/html/index.html doc/faq/FAQ.v.ps doc/faq/FAQ.v.pdf -rectutorial:\ - doc/RecTutorial/RecTutorial.html \ +rectutorial: doc/RecTutorial/RecTutorial.html \ doc/RecTutorial/RecTutorial.ps doc/RecTutorial/RecTutorial.pdf ###################################################################### ### Implicit rules ###################################################################### -ifeq ($(QUICK),1) +ifdef QUICK %.v.tex: %.tex (cd `dirname $<`; $(COQSRC)/$(COQTEX) $(COQTEXOPTS) `basename $<`) else -%.v.tex: %.tex | $(COQTEX) $(COQTOPEXE) $(CONTRIBVO) $(CONTRIBCMO) $(THEORIESVO) +%.v.tex: %.tex $(COQTEX) $(COQTOPEXE) $(PLUGINSVO) $(THEORIESVO) (cd `dirname $<`; $(COQSRC)/$(COQTEX) $(COQTEXOPTS) `basename $<`) endif @@ -68,6 +66,9 @@ 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 ###################################################################### @@ -81,11 +82,12 @@ 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 +doc/refman/Reference-Manual.dvi: $(REFMANFILES) doc/refman/Reference-Manual.tex @(cd doc/refman;\ $(LATEX) -interaction=batchmode Reference-Manual;\ $(BIBTEX) -terse Reference-Manual $(HIDEBIBTEXINFO);\ @@ -102,7 +104,7 @@ doc/refman/Reference-Manual.dvi: $(DOCCOMMON) $(REFMANFILES) doc/refman/Referenc $(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 +doc/refman/Reference-Manual.pdf: $(REFMANFILES) doc/refman/Reference-Manual.tex (cd doc/refman;\ $(PDFLATEX) -interaction=batchmode Reference-Manual.tex;\ ../tools/show_latex_messages -no-overfull Reference-Manual.log) @@ -125,7 +127,7 @@ doc/refman/html/index.html: doc/refman/Reference-Manual.html $(REFMANPNGFILES) \ $(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 + $(INSTALLLIB) doc/common/styles/html/$(HTMLSTYLE)/*.css doc/refman/html refman-quick: (cd doc/refman;\ @@ -169,7 +171,7 @@ doc/faq/FAQ.v.pdf: doc/common/version.tex doc/common/title.tex doc/faq/FAQ.v.dvi ../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) + (cd doc/faq; ($(HEVEA) $(HEVEAOPTS) FAQ.v.tex $(HEVEAFAQFILTER))) doc/faq/html/index.html: doc/faq/FAQ.v.html - rm -rf doc/faq/html @@ -183,44 +185,52 @@ doc/faq/html/index.html: doc/faq/FAQ.v.html ### Standard library (browsable html format) -ifeq ($(QUICK),1) -doc/stdlib/html/genindex.html: +ifdef QUICK +doc/stdlib/index-body.html: + - rm -rf doc/stdlib/html + $(MKDIR) doc/stdlib/html + $(COQDOC) -q -boot -d doc/stdlib/html --multi-index --html -g --utf8 \ + -R theories Coq $(THEORIESVO:.vo=.v) + mv doc/stdlib/html/index.html doc/stdlib/index-body.html else -doc/stdlib/html/genindex.html: | $(COQDOC) $(THEORIESVO) -endif +doc/stdlib/index-body.html: $(COQDOC) $(THEORIESVO) - rm -rf doc/stdlib/html $(MKDIR) doc/stdlib/html - $(COQDOC) -q -d doc/stdlib/html --with-header doc/common/styles/html/$(HTMLSTYLE)/header.html --with-footer doc/common/styles/html/$(HTMLSTYLE)/footer.html --multi-index --html -g \ + $(COQDOC) -q -boot -d doc/stdlib/html --multi-index --html -g --utf8 \ -R theories Coq $(THEORIESVO:.vo=.v) - mv doc/stdlib/html/index.html doc/stdlib/html/genindex.html + mv doc/stdlib/html/index.html doc/stdlib/index-body.html +endif 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/html/genindex.html doc/stdlib/index-list.html - cat doc/common/styles/html/$(HTMLSTYLE)/header.html doc/stdlib/index-list.html > $@ - cat doc/common/styles/html/$(HTMLSTYLE)/footer.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 > $@ + sed -n -e '//,/<\/table>/p' doc/stdlib/index-body.html >> $@ + cat doc/stdlib/index-trailer.html >> $@ ### Standard library (light version, full version is definitely too big) -ifeq ($(QUICK),1) +ifdef QUICK doc/stdlib/Library.coqdoc.tex: + $(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \ + -R theories Coq $(THEORIESLIGHTVO:.vo=.v) > $@ else -doc/stdlib/Library.coqdoc.tex: | $(COQDOC) $(THEORIESLIGHTVO) -endif - $(COQDOC) -q -boot --gallina --body-only --latex --stdout \ +doc/stdlib/Library.coqdoc.tex: $(COQDOC) $(THEORIESLIGHTVO) + $(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \ -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) -interaction=batchmode Library;\ $(LATEX) -interaction=batchmode Library > /dev/null;\ - ../tools/show_latex_messages Library.log) + ../tools/show_latex_messages -no-overfull Library.log) doc/stdlib/Library.pdf: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Library.dvi (cd doc/stdlib;\ $(PDFLATEX) -interaction=batchmode Library;\ - ../tools/show_latex_messages Library.log) + ../tools/show_latex_messages -no-overfull Library.log) ###################################################################### # Tutorial on inductive types @@ -248,21 +258,23 @@ doc/RecTutorial/RecTutorial.html: doc/RecTutorial/RecTutorial.tex # Not robust, improve... ide/index_urls.txt: doc/refman/html/index.html - @ 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@.*\(.*\).*, .*@\1,\2@' > ide/index_urls.txt + @ rm -f doc/refman/html/index_urls.txt + cat doc/refman/html/command-index.html doc/refman/html/tactic-index.html | grep li-indexenv | grep HREF | sed -e 's@.*\(.*\).*, .*@\1,\2@' > doc/refman/html/index_urls.txt ###################################################################### # Install all documentation files ###################################################################### -install-doc: install-doc-meta install-doc-html install-doc-printable +.PHONY: install-doc install-doc-meta install-doc-html install-doc-printable install-doc-index-url + +install-doc: install-doc-meta install-doc-html install-doc-printable install-doc-index-url install-doc-meta: $(MKDIR) $(FULLDOCDIR) $(INSTALLLIB) doc/LICENSE $(FULLDOCDIR)/LICENSE.doc -install-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 @@ -270,7 +282,7 @@ install-doc-html: $(INSTALLLIB) doc/faq/html/* $(FULLDOCDIR)/html/faq $(INSTALLLIB) doc/tutorial/Tutorial.v.html $(FULLDOCDIR)/html/Tutorial.html -install-doc-printable: +install-doc-printable: $(MKDIR) $(FULLDOCDIR)/ps $(FULLDOCDIR)/pdf $(INSTALLLIB) doc/refman/Reference-Manual.pdf \ doc/stdlib/Library.pdf $(FULLDOCDIR)/pdf @@ -282,3 +294,13 @@ install-doc-printable: $(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-url: + $(MKDIR) $(FULLDOCDIR)/ps $(FULLDOCDIR)/pdf + $(INSTALLLIB) doc/refman/html/index_urls.txt \ + $(FULLDOCDIR)/html/refman + +# For emacs: +# Local Variables: +# mode: makefile +# End: -- cgit v1.2.3