Makefile: fix ignored errors, several attempts to clarify things

 * I encountered error messages during compilation, for instance
 ocamlopt complaining about non-existing coq_config.cmi when compiling
 coq_config.ml. Moreover, make was _not_ stopping at these errors
 (WTF?!). After some debug, it turned out to be (indirectly) my fault:
 I placed earlier the inclusion of the new .mllib.d in
 Makefile.stage1, but this is too early, coqdep, which is used to
 compute these files, isn't built yet. Due to the semantics of
 "-include", make tries to build it, fails with the above error,
 and goes on happily. Arrgh. After moving the inclusion of these
 .mllib.d to Makefile.stage2, everything seems to work ok now.

 * Since we're using such "nice" non-trivial features of make, I've
 started a small FAQ section about them at the beginning of Makefile

 * Recursive calls to make are now done with two options:
 --no-builtin-rules : let's avoid builtin rules like "%:%.o" ...
 --warn-undefined-variable : using a non-defined variable isn't
  necessarily bad, but I found a few bugs with this option, and
  I suggest we keep it.

 * Clarified the rules about stage* in Makefile and their
 STAGE*_TARGETS variables in Makefile.common. Now a newcomer _might_
 have a chance to grasp in less than a day what's going on ...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11983 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 12 insertions, 6 deletions

diff --git a/Makefile.doc b/Makefile.doc
index 2190ebf69..cf849dadf 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -45,11 +45,11 @@ rectutorial: doc/RecTutorial/RecTutorial.html \
 ### 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) $(CONTRIBVO) $(THEORIESVO)
 	(cd `dirname $<`; $(COQSRC)/$(COQTEX) $(COQTEXOPTS) `basename $<`)
 endif
 
@@ -87,7 +87,7 @@ doc/common/version.tex: config/Makefile
 
 # 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 +102,7 @@ doc/refman/Reference-Manual.dvi: $(DOCCOMMON) $(REFMANFILES) doc/refman/Referenc
 	$(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)
+	../tools/show_latex_messages -no-overfull Reference-Manual.log)
 
 doc/refman/Reference-Manual.pdf: $(REFMANFILES) doc/refman/Reference-Manual.tex
 	(cd doc/refman;\
@@ -185,7 +185,7 @@ doc/faq/html/index.html: doc/faq/FAQ.v.html
 
 ### Standard library (browsable html format)
 
-ifeq ($(QUICK),1)
+ifdef QUICK
 doc/stdlib/index-body.html:
 	- rm -rf doc/stdlib/html
 	$(MKDIR) doc/stdlib/html
@@ -211,7 +211,7 @@ 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)
 
-ifeq ($(QUICK),1)
+ifdef QUICK
 doc/stdlib/Library.coqdoc.tex:
 	$(COQDOC) -q -boot --gallina --body-only --latex --stdout \
             -R theories Coq $(THEORIESLIGHTVO:.vo=.v) >> $@
@@ -292,3 +292,9 @@ 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
+
+
+# For emacs:
+# Local Variables:
+# mode: makefile
+# End: