Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg

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