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, 38 insertions, 9 deletions

diff --git a/Makefile.common b/Makefile.common
index ce1fad6b2b..7fd52594c4 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -33,6 +33,9 @@ CHICKEN:=bin/coqchk$(EXE)
 ifneq ($(HASNATDYNLINK),false)
   DYNLINKCMXA:=dynlink.cmxa
   NATDYNLINKDEF:=-DHasDynlink
+else
+  DYNLINKCMXA:=
+  NATDYNLINKDEF:=
 endif
 
 INSTALLBIN:=install
@@ -120,7 +123,7 @@ REFMANTEXFILES:=$(addprefix doc/refman/, \
 
 REFMANEPSFILES:=doc/refman/coqide.eps doc/refman/coqide-queries.eps
 
-REFMANFILES:=$(REFMANTEXFILES) $(COMMON) $(REFMANEPSFILES) doc/refman/biblio.bib
+REFMANFILES:=$(REFMANTEXFILES) $(DOCCOMMON) $(REFMANEPSFILES) doc/refman/biblio.bib
 
 REFMANPNGFILES:=$(REFMANEPSFILES:.eps=.png)
 
@@ -268,11 +271,15 @@ ifneq ($(HASNATDYNLINK),false)
  CONTRIBSTATIC:=
  INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) $(DPCMA) \
 	$(XMLCMA) $(FUNINDCMA) $(SUBTACCMA)
- PLUGINS:=$(CONTRIBS)
  INITPLUGINSOPT:=$(INITPLUGINS:.cma=.cmxs)
+ PLUGINS:=$(CONTRIBS)
  PLUGINSOPT:=$(PLUGINS:.cma=.cmxs)
 else
  CONTRIBSTATIC:=$(CONTRIBS)
+ INITPLUGINS:=
+ INITPLUGINSOPT:=
+ PLUGINS:=
+ PLUGINSOPT:=
 endif
 
 CMA:=$(CLIBS) $(CAMLP4OBJS)
@@ -793,27 +800,49 @@ DATE=$(shell LANG=C date +"%B %Y")
 
 SOURCEDOCDIR=dev/source-doc
 
-## Targets forwarded by Makefile to a specific stage
+CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi %.cma %.cmxa %.cmxs %.dep.ps %.dot
+
+### Targets forwarded by Makefile to a specific stage:
+
+## Enumeration of targets that require being done at stage1
+
 STAGE1_TARGETS:= $(STAGE1) \
   $(filter-out parsing/q_constr.cmo,$(STAGE1_CMO)) \
   $(STAGE1_CMO:.cmo=.cmi) $(STAGE1_CMO:.cmo=.cmx) $(GENFILES) \
   source-doc revision toplevel/mltop.byteml toplevel/mltop.optml \
-  $(STAGE1_ML4:.ml4=.ml4-preprocessed)
+  $(STAGE1_ML4:.ml4=.ml4-preprocessed) %.o
+
+ifdef CM_STAGE1
+ STAGE1_TARGETS+=$(CAML_OBJECT_PATTERNS)
+endif
+
+## Enumeration of targets that require being done at stage2
+
 STAGE2_TARGETS:=$(COQBINARIES) lib kernel byterun library proofs tactics \
   interp parsing pretyping highparsing toplevel hightactics \
   coqide-binaries coqide-byte coqide-opt $(COQIDEOPT) $(COQIDEBYTE) $(COQIDE) \
   pcoq-binaries $(COQINTERFACE) $(CSDPCERT) coqbinaries pcoq $(TOOLS) tools \
-  printers debug initplugins plugins
+  printers debug initplugins plugins %.ml4-preprocessed
+
+ifndef CM_STAGE1
+ STAGE2_TARGETS+=$(CAML_OBJECT_PATTERNS)
+endif
+
+## Enumeration of targets that require being done at stage3
+
 VO_TARGETS:=logic arith bool narith zarith qarith lists strings sets \
   fsets allfsets relations wellfounded ints reals allreals \
   setoids sorting natural integer rational numbers noreal \
   omega micromega ring setoid_ring dp xml extraction field fourier \
-  funind cc programs subtac rtauto
-DOC_TARGETS:=doc doc-html doc-ps doc-pdf stdlib refman tutorial faq rectutorial refman-quick refman-nodep stdlib-nodep
+  funind cc subtac rtauto
+
+DOC_TARGETS:=doc doc-html doc-ps doc-pdf stdlib refman tutorial faq \
+  rectutorial refman-quick refman-nodep stdlib-nodep
+
 STAGE3_TARGETS:=world install coqide coqide-files coq coqlib \
   coqlight states pcoq-files check init theories theories-light contrib \
-  $(DOC_TARGETS) $(VO_TARGETS) validate
-
+  $(DOC_TARGETS) $(VO_TARGETS) validate \
+  %.vo %.glob states/% install-%
 
 # For emacs: 
 # Local Variables: