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

6 files changed, 123 insertions, 56 deletions

diff --git a/Makefile b/Makefile
index b94cb34da..b3be1e813 100644
--- a/Makefile
+++ b/Makefile
@@ -24,6 +24,50 @@
 # by Emacs' next-error.
 ###########################################################################
 
+
+# Specific command-line options to this Makefile
+#
+# make GOTO_STAGE=N        # perform only stage N (with N=1,2,3)
+# make VERBOSE=1           # restore the raw echoing of commands
+# make NO_RECALC_DEPS=1    # avoid recomputing dependencies
+# make NO_RECOMPILE_LIB=1  # a coqtop rebuild does not trigger a stdlib rebuild
+#
+# Nota: the 1 above can be replaced by any non-empty value
+# More details in dev/doc/build-system*.txt
+
+
+# FAQ: special features used in this Makefile
+#
+# * Order-only dependencies: |
+#
+# Dependencies placed after a bar (|) should be built before
+# the current rule, but having one of them is out-of-date do not
+# trigger a rebuild of the current rule.
+# See http://www.gnu.org/software/make/manual/make.html#Prerequisite-Types
+#
+# * Annotation before commands: +/-/@
+#
+# a command starting by - is always successful (errors are ignored)
+# a command starting by + is runned even if option -n is given to make
+# a command starting by @ is not echoed before being runned
+#
+# * Custom functions
+#
+# Definition via "define foo" followed by commands (arg is $(1) etc)
+# Call via "$(call foo,arg1)"
+#
+# * Useful builtin functions
+#
+# $(subst ...), $(patsubst ...), $(shell ...), $(foreach ...)
+#
+# * Behavior of -include
+#
+# If the file given to -include doesn't exist, make tries to build it,
+# but doesn't care if this build fails. This can be quite surprising,
+# see in particular the -include in Makefile.stage*
+
+
+
 # !! Before using FIND_VCS_CLAUSE, please read how you should in the !!
 # !! FIND_VCS_CLAUSE section of dev/doc/build-system.dev.txt         !!
 export FIND_VCS_CLAUSE:='(' \
@@ -59,6 +103,9 @@ export CFILES   := $(shell find kernel/byterun $(FIND_VCS_CLAUSE) '(' -name '*.c
 
 export ML4FILESML:= $(ML4FILES:.ml4=.ml)
 
+# Nota: do not use the name $(MAKEFLAGS), it has a particular behavior
+MAKEFLGS:=--warn-undefined-variable --no-builtin-rules
+
 include Makefile.common
 
 NOARG: world
@@ -84,7 +131,7 @@ define stage-template
 	@echo '****************** Entering stage$(1) ******************'
 	@echo '*****************************************************'
 	@echo '*****************************************************'
-	+$(MAKE) -f Makefile.stage$(1) "$@"
+	+$(MAKE) $(MAKEFLGS) -f Makefile.stage$(1) "$@"
 endef
 else
 define stage-template
@@ -110,37 +157,26 @@ else
 
 .PHONY: stage1 stage2 stage3 world revision
 
-# This is to remove the built-in rule "%: %.o"
-# Otherwise, "make foo" recurses into stage1, trying to build foo.o .
-%: %.o
-
-%.o: always
+stage1 $(STAGE1_TARGETS) : always
 	$(call stage-template,1)
 
-#STAGE1_TARGETS includes all object files necessary for $(STAGE1)
-stage1 $(STAGE1_TARGETS): always
-	$(call stage-template,1)
-
-CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi %.cma %.cmxa %.cmxs %.dep.ps %.dot
-ifdef CM_STAGE1
-$(CAML_OBJECT_PATTERNS): always
-	$(call stage-template,1)
-
-%.ml4-preprocessed: stage1
-	$(call stage-template,2)
-else
-$(CAML_OBJECT_PATTERNS) %.ml4-preprocessed: stage1
-	$(call stage-template,2)
-endif
-
-stage2 $(STAGE2_TARGETS): stage1
+stage2 $(STAGE2_TARGETS) : stage1
 	$(call stage-template,2)
 
-%.vo %.glob states/% install-%: stage2
+stage3 $(STAGE3_TARGETS) : stage2
 	$(call stage-template,3)
 
-stage3 $(STAGE3_TARGETS): stage2
-	$(call stage-template,3)
+# Nota:
+# - world is one of the targets in $(STAGE3_TARGETS), hence launching 
+# "make" or "make world" leads to recursion into stage{1,2,3}
+# - the aim of stage1 is to build grammar.cma and q_constr.cmo
+# - the aim of stage2 is to build coqdep
+# More details in dev/doc/build-system*.txt
+
+
+# This is to remove the built-in rule "%: %.o" :
+%: %.o
+# Otherwise, "make foo" recurses into stage1, trying to build foo.o .
 
 endif #GOTO_STAGE
 
diff --git a/Makefile.build b/Makefile.build
index 5d5ff8533..364ea3503 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -34,14 +34,12 @@ endif
 NOARG: world
 
 # build and install the three subsystems: coq, coqide, pcoq
-ifeq ($(WITHDOC),all)
-world: revision coq coqide pcoq doc
-
-install: install-coq install-coqide install-pcoq install-doc
-else
 world: revision coq coqide pcoq
-
 install: install-coq install-coqide install-pcoq
+
+ifeq ($(WITHDOC),all)
+world: doc
+install: install-doc
 endif
 
 #install-manpages: install-coq-manpages install-pcoq-manpages
@@ -54,7 +52,7 @@ endif
 # or only abbreviated versions. 
 # Quiet mode is ON by default except if VERBOSE=1 option is given to make
 
-ifeq ($(VERBOSE),1)
+ifdef VERBOSE
  SHOW = @true ""
  HIDE = 
 else 
@@ -110,7 +108,9 @@ ifdef VALIDATE
 endif
 ifdef NO_RECOMPILE_LIB
  VO_TOOLS_ORDER_ONLY:=$(VO_TOOLS_DEP)
+ VO_TOOLS_STRICT:=
 else
+ VO_TOOLS_ORDER_ONLY:=
  VO_TOOLS_STRICT:=$(VO_TOOLS_DEP)
 endif
 
@@ -163,8 +163,6 @@ coqlight: theories-light tools coqbinaries
 
 states:: states/initial.coq
 
-plugins: $(PLUGINSOPT) $(PLUGINS)
-
 $(COQTOPOPT): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN)
 	$(SHOW)'COQMKTOP -o $@'	
 	$(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) -o $@
@@ -530,8 +528,7 @@ field: $(FIELDVO) $(FIELDCMA)
 fourier: $(FOURIERVO) $(FOURIERCMA)
 funind: $(FUNINDCMA) $(FUNINDVO)
 cc: $(CCVO) $(CCCMA)
-programs: $(PROGRAMSVO)
-subtac: $(SUBTACVO) $(SUBTACCMA)
+subtac: $(SUBTACCMA)
 rtauto: $(RTAUTOVO) $(RTAUTOCMA)
 
 ###########################################################################
@@ -720,8 +717,7 @@ install-latex:
 
 source-doc:
 	if !(test -d $(SOURCEDOCDIR)); then mkdir $(SOURCEDOCDIR); fi
-	$(OCAMLDOC) -html -rectypes $(LOCALINCLUDES) -d $(SOURCEDOCDIR) \
-	  `find . $(FIND_VCS_CLAUSE) '(' -name '*.ml' ')' -print`
+	$(OCAMLDOC) -html -rectypes $(LOCALINCLUDES) -d $(SOURCEDOCDIR) $(MLFILES)
 
 
 ###########################################################################
diff --git a/Makefile.common b/Makefile.common
index ce1fad6b2..7fd52594c 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: 
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:
diff --git a/Makefile.stage1 b/Makefile.stage1
index a558e3aa6..a60d388fc 100644
--- a/Makefile.stage1
+++ b/Makefile.stage1
@@ -18,8 +18,6 @@ include Makefile.build
 .SECONDARY: $(MLFILES:.ml=.ml.d)
 -include $(MLIFILES:.mli=.mli.d)
 .SECONDARY: $(MLIFILES:.mli=.mli.d)
--include $(MLLIBFILES:.mllib=.mllib.d)
-.SECONDARY: $(MLLIBFILES:.mli=.mllib.d)
 ##Depends upon the fact that all .ml4.d for stage1 files are empty
 -include $(STAGE1_ML4:.ml4=.ml4.ml.d)
 .SECONDARY: $(STAGE1_ML4:.ml4=.ml4.ml.d)
diff --git a/Makefile.stage2 b/Makefile.stage2
index 6fe020be9..81e192cfc 100644
--- a/Makefile.stage2
+++ b/Makefile.stage2
@@ -8,6 +8,8 @@
 
 include Makefile.stage1
 
+-include $(MLLIBFILES:.mllib=.mllib.d)
+.SECONDARY: $(MLLIBFILES:.mli=.mllib.d)
 -include $(ML4FILES:.ml4=.ml4.ml.d)
 .SECONDARY: $(ML4FILES:.ml4=.ml4.ml.d)