Makefile: re-introduce 2 phases to avoid make strange -include's

Yet another revision of the build system. We avoid relying on the awkward
include-which-fails-but-works-finally-after-a-retry feature of gnu make.
This was working, but was quite hard to understand. Instead, we reuse
the idea of two explicit phases (as in 2007 and its stage{1,2,3}), but
in a lighter way. The main Makefile calls Makefile.build twice :
 - first for building grammar.cma (and q_constr.cmo), with a restricted
   set of .ml4 to consider (see variables BUILDGRAMMAR and ML4BASEFILES).
 - then on the true target(s) asked by the user (using the special variable
   MAKECMDGOALS).

In pratice, this should change very little to the concrete developper's life,
let me know otherwise. A few more messages of make due to the explicit
first sub-call, but no more strange "not ready yet" messages...

Btw: we should handle correctly now the parallel compilation of multiple
targets (e.g. make -jX foo bar). As reported by Pierre B, this was
triggering earlier two separate sub-calls to Makefile.build, one
for foo, the other for bar, with possibly nasty interactions in case
of parallelism.

In addition, some cleanup of Makefile.build, removal of useless :: rules,
etc etc.

4 files changed, 172 insertions, 342 deletions

diff --git a/Makefile b/Makefile
index 10fb51f62..6c03ae05f 100644
--- a/Makefile
+++ b/Makefile
@@ -59,11 +59,20 @@ define find
  $(shell find . $(FIND_VCS_CLAUSE) '(' -name $(1) ')' -print | sed 's|^\./||')
 endef
 
+define findx
+ $(shell find . $(FIND_VCS_CLAUSE) '(' -name $(1) ')' -exec $(2) {} \; | sed 's|^\./||')
+endef
+
+# We now discriminate .ml4 files according to their need of grammar.cma
+# or q_constr.cmo
+USEGRAMMAR := '(\*.*camlp4deps.*grammar'
+
 ## Files in the source tree
 
 YACCFILES:=$(call find, '*.mly')
 LEXFILES := $(call find, '*.mll')
 export MLLIBFILES := $(call find, '*.mllib')
+export ML4BASEFILES := $(call findx, '*.ml4', grep -L -e $(USEGRAMMAR))
 export ML4FILES := $(call find, '*.ml4')
 export CFILES := $(call find, '*.c')
 
@@ -77,13 +86,13 @@ EXISTINGMLI := $(call find, '*.mli')
 ## Files that will be generated
 
 GENML4FILES:= $(ML4FILES:.ml4=.ml)
-GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) \
-  tools/tolink.ml kernel/copcodes.ml
 GENMLIFILES:=$(YACCFILES:.mly=.mli)
 GENPLUGINSMOD:=$(filter plugins/%,$(MLLIBFILES:%.mllib=%_mod.ml))
+export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) \
+  tools/tolink.ml kernel/copcodes.ml $(GENPLUGINSMOD)
 export GENHFILES:=kernel/byterun/coq_jumptbl.h
 export GENVFILES:=theories/Numbers/Natural/BigN/NMake_gen.v
-export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) $(GENVFILES) $(GENPLUGINSMOD)
+export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) $(GENVFILES)
 
 # NB: all files in $(GENFILES) can be created initially, while
 # .ml files in $(GENML4FILES) might need some intermediate building.
@@ -95,8 +104,7 @@ define diff
  $(strip $(foreach f, $(1), $(if $(filter $(f),$(2)),,$f)))
 endef
 
-export MLEXTRAFILES := $(GENMLFILES) $(GENML4FILES) $(GENPLUGINSMOD)
-export MLSTATICFILES := $(call diff, $(EXISTINGML), $(MLEXTRAFILES))
+export MLSTATICFILES := $(call diff, $(EXISTINGML), $(GENMLFILES) $(GENML4FILES))
 export MLIFILES := $(sort $(GENMLIFILES) $(EXISTINGMLI))
 
 include Makefile.common
@@ -107,7 +115,7 @@ include Makefile.common
 
 NOARG: world
 
-.PHONY: NOARG help always
+.PHONY: NOARG help noconfig submake
 
 help:
 	@echo "Please use either"
@@ -131,17 +139,27 @@ endif
 
 # Apart from clean and tags, everything will be done in a sub-call to make
 # on Makefile.build. This way, we avoid doing here the -include of .d :
-# since they trigger some compilations, we do not want them for a mere clean
+# since they trigger some compilations, we do not want them for a mere clean.
+# Moreover, we regroup this sub-call in a common target named 'submake'.
+# This way, multiple user-given goals (cf the MAKECMDGOALS variable) won't
+# trigger multiple (possibly parallel) make sub-calls
 
 ifdef COQ_CONFIGURED
-%:: always
-	$(MAKE) --warn-undefined-variable --no-builtin-rules -f Makefile.build "$@"
+%:: submake ;
 else
-%:: always
-	@echo "Please run ./configure first" >&2; exit 1
+%:: noconfig ;
 endif
 
-always : ;
+MAKE_OPTS := --warn-undefined-variable --no-builtin-rules
+
+GRAM_TARGETS := grammar/grammar.cma grammar/q_constr.cmo
+
+submake:
+	$(MAKE) $(MAKE_OPTS) -f Makefile.build BUILDGRAMMAR=1 $(GRAM_TARGETS)
+	$(MAKE) $(MAKE_OPTS) -f Makefile.build $(MAKECMDGOALS)
+
+noconfig:
+	@echo "Please run ./configure first" >&2; exit 1
 
 # To speed-up things a bit, let's dissuade make to attempt rebuilding makefiles
 
@@ -165,7 +183,7 @@ cruftclean: ml4clean
 
 indepclean:
 	rm -f $(GENFILES)
-	rm -f $(COQTOPBYTE) $(CHICKENBYTE) bin/fake_ide
+	rm -f $(COQTOPBYTE) $(CHICKENBYTE) $(FAKEIDE)
 	find . \( -name '*~' -o -name '*.cm[ioat]' -o -name '*.cmti' \) -delete
 	rm -f */*.pp[iox] plugins/*/*.pp[iox]
 	rm -rf $(SOURCEDOCDIR)
@@ -234,7 +252,7 @@ devdocclean:
 # Emacs tags
 ###########################################################################
 
-.PHONY: tags
+.PHONY: tags printenv
 
 tags:
 	echo $(MLIFILES) $(MLSTATICFILES) $(ML4FILES) | sort -r | xargs \
diff --git a/Makefile.build b/Makefile.build
index 312db8ec9..760a4db72 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -14,7 +14,9 @@
 ###########################################################################
 
 # build the different subsystems: coq, coqide
-world: revision coq coqide
+world: revision coq coqide documentation
+
+.PHONY: world
 
 ###########################################################################
 # Includes
@@ -23,40 +25,29 @@ world: revision coq coqide
 include Makefile.common
 include Makefile.doc
 
-ifeq ($(LOCAL),true)
-install:
-	@echo "Nothing to install in a local build!"
+# In a first phase, we restrict to the basic .ml4 (the ones without grammar.cma)
+
+ifdef BUILDGRAMMAR
+ MLFILES := $(MLSTATICFILES) $(GENMLFILES) $(ML4BASEFILES:.ml4=.ml)
+ CURFILES := $(MLFILES) $(MLIFILES) $(ML4BASEFILES) grammar/grammar.mllib
 else
-install: install-coq install-coqide install-doc-$(WITHDOC)
+ MLFILES := $(MLSTATICFILES) $(GENMLFILES) $(ML4FILES:.ml4=.ml)
+ CURFILES := $(MLFILES) $(MLIFILES) $(ML4FILES) $(MLLIBFILES) $(CFILES) $(VFILES)
 endif
 
-install-doc-all: install-doc
-install-doc-no:
-
-world: doc-$(WITHDOC)
-doc-all: doc
-doc-no:
-
-.PHONY: world install install-doc-all install-doc-no doc-all doc-no
+CURDEPS:=$(addsuffix .d, $(CURFILES))
 
 # All dependency includes must be declared secondary, otherwise make will
 # delete them if it decided to build them by dependency instead of because
 # of include, and they will then be automatically deleted, leading to an
 # infinite loop.
 
-MLFILES:=$(MLSTATICFILES) $(MLEXTRAFILES)
-
-ALLDEPS:=$(addsuffix .d, \
-  $(ML4FILES) $(MLFILES) $(MLIFILES) $(CFILES) $(MLLIBFILES) $(VFILES))
+.SECONDARY: $(CURDEPS) $(GENFILES) $(ML4FILES:.ml4=.ml)
 
-.SECONDARY: $(ALLDEPS) $(GENFILES) $(ML4FILES:.ml4=.ml)
+# This include below will lauch the build of all concerned .d.
+# The - at front is for disabling warnings about currently missing ones.
 
-# NOTA: the -include below will lauch the build of all .d. Some of them
-# will _fail_ at first, this is to be expected (no grammar.cma initially).
-# These errors (see below "not ready yet") do not discourage make to
-# try again and finally succeed.
-
--include $(ALLDEPS)
+-include $(CURDEPS)
 
 
 ###########################################################################
@@ -205,11 +196,11 @@ kernel/copcodes.ml: kernel/byterun/coq_instruct.h
 
 .PHONY: coqbinaries coq coqlib coqlight states
 
-coqbinaries:: ${COQBINARIES} ${CSDPCERT} ${FAKEIDE}
+coqbinaries: ${COQBINARIES} ${CSDPCERT} ${FAKEIDE}
 
 coq: coqlib tools coqbinaries
 
-coqlib:: theories plugins
+coqlib: theories plugins
 
 coqlight: theories-light tools coqbinaries
 
@@ -300,7 +291,7 @@ plugins/micromega/csdpcert$(EXE): $(CSDPCERTCMO:.cmo=$(BESTOBJ))
 .PHONY: coqide coqide-binaries coqide-no coqide-byte coqide-opt coqide-files
 
 # target to build CoqIde
-coqide:: coqide-files coqide-binaries theories/Init/Prelude.vo
+coqide: coqide-files coqide-binaries theories/Init/Prelude.vo
 
 COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS)) $(COQIDEINCLUDES)
 
@@ -385,7 +376,7 @@ $(ALLSTDLIB).v:
 
 MAKE_TSOPTS=-C test-suite -s VERBOSE=$(VERBOSE)
 
-check:: validate test-suite
+check: validate test-suite
 
 test-suite: world $(ALLSTDLIB).v
 	$(MAKE) $(MAKE_TSOPTS) clean
@@ -493,7 +484,7 @@ theories/Numbers/Natural/BigN/NMake_gen.v: theories/Numbers/Natural/BigN/NMake_g
 
 printers: $(DEBUGPRINTERS)
 
-tools:: $(TOOLS) $(DEBUGPRINTERS) $(COQDEPBOOT)
+tools: $(TOOLS) $(DEBUGPRINTERS) $(COQDEPBOOT)
 
 # coqdep_boot : a basic version of coqdep, with almost no dependencies.
 
@@ -564,9 +555,31 @@ tools/compat5b.cmo: tools/compat5b.ml
 endif
 
 ###########################################################################
+# Documentation : cf Makefile.doc
+###########################################################################
+
+documentation: doc-$(WITHDOC)
+doc-all: doc
+doc-no:
+
+.PHONY: documentation doc-all doc-no
+
+###########################################################################
 # Installation
 ###########################################################################
 
+ifeq ($(LOCAL),true)
+install:
+	@echo "Nothing to install in a local build!"
+else
+install: install-coq install-coqide install-doc-$(WITHDOC)
+endif
+
+install-doc-all: install-doc
+install-doc-no:
+
+.PHONY: install install-doc-all install-doc-no
+
 #These variables are intended to be set by the caller to make
 #COQINSTALLPREFIX=
 #OLDROOT=
@@ -605,7 +618,7 @@ install-binaries: install-tools
 	$(MKDIR) $(FULLBINDIR)
 	$(INSTALLBIN) $(COQC) $(COQTOPBYTE) $(COQTOPEXE) $(CHICKEN) $(FULLBINDIR)
 
-install-tools::
+install-tools:
 	$(MKDIR) $(FULLBINDIR)
 	# recopie des fichiers de style pour coqide
 	$(MKDIR) $(FULLCOQLIB)/tools/coqdoc
@@ -683,18 +696,18 @@ install-latex:
 
 source-doc: mli-doc $(OCAMLDOCDIR)/coq.pdf
 
-$(OCAMLDOCDIR)/coq.tex:: $(DOCMLIS:.mli=.cmi)
+$(OCAMLDOCDIR)/coq.tex: $(DOCMLIS:.mli=.cmi)
 	$(OCAMLDOC) -latex -rectypes -I $(MYCAMLP4LIB) $(MLINCLUDES)\
 	$(DOCMLIS) -t "Coq mlis documentation" \
 	-intro $(OCAMLDOCDIR)/docintro -o $@
 
-mli-doc:: $(DOCMLIS:.mli=.cmi)
+mli-doc: $(DOCMLIS:.mli=.cmi)
 	$(OCAMLDOC) -html -rectypes -I $(MYCAMLP4LIB) $(MLINCLUDES)\
 	$(DOCMLIS) -d $(OCAMLDOCDIR)/html -colorize-code \
 	-t "Coq mlis documentation" -intro $(OCAMLDOCDIR)/docintro \
 	-css-style style.css
 
-ml-dot:: $(MLEXTRAFILES)
+ml-dot: $(MLFILES)
 	$(OCAMLDOC) -dot -dot-reduce -rectypes -I $(CAMLLIB) -I $(MYCAMLP4LIB) $(MLINCLUDES)\
 	$(filter $(addsuffix /%.ml,$(CORESRCDIRS)),$(MLFILES)) -o $(OCAMLDOCDIR)/coq.dot
 
@@ -884,11 +897,8 @@ plugins/%_mod.ml: plugins/%.mllib
 
 %.ml: %.ml4 | %.ml4.d tools/compat5.cmo tools/compat5b.cmo
 	$(SHOW)'CAMLP4O   $<'
-	$(HIDE)\
-	DEPS="$(call CAMLP4DEPS,$<)"; \
-	if ls $${DEPS} > /dev/null 2>&1; then \
-	$(CAMLP4O) $(PR_O) -I $(CAMLLIB) tools/compat5.cmo $${DEPS} $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< -o $@; \
-	else echo $< : Dependency $${DEPS} not ready yet; false; fi
+	$(HIDE)$(CAMLP4O) $(PR_O) -I $(CAMLLIB) tools/compat5.cmo \
+	  $(call CAMLP4DEPS,$<) $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< -o $@
 
 %.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP) | %.v.d
 	$(SHOW)'COQC      $<'
@@ -966,6 +976,10 @@ otags:
 
 ###########################################################################
 
+# To speed-up things a bit, let's dissuade make to attempt rebuilding makefiles
+
+Makefile Makefile.build Makefile.common config/Makefile : ;
+
 
 # For emacs: 
 # Local Variables: 
diff --git a/dev/doc/build-system.dev.txt b/dev/doc/build-system.dev.txt
index 3d9cba143..af1120e97 100644
--- a/dev/doc/build-system.dev.txt
+++ b/dev/doc/build-system.dev.txt
@@ -1,21 +1,38 @@
 
-Since July 2007, Coq features a build system overhauled by Pierre
-Corbineau and Lionel Elie Mamane.
-
----------------------------------------------------------------------
-WARNING:
-In March 2010 this build system has been heavily adapted by Pierre
-Letouzey. In particular there no more explicit stage1,2. Stage3
-was removed some time ago when coqdep was splitted into coqdep_boot
-and full coqdep. Ideas are still similar to what is describe below,
-but:
-1) .ml4 are explicitely turned into .ml files, which stay after build
-2) we let "make" handle the inclusion of .d without trying to guess
-   what could be done at what time. Some initial inclusions hence
-  _fail_, but "make" tries again later and succeed.
-
-TODO: remove obsolete sections below and better describe the new approach
------------------------------------------------------------------------
+
+HISTORY:
+-------
+
+* July 2007 (Pierre Corbineau & Lionel Elie Mamane).
+  Inclusion of a build system with 3 explicit phases:
+  - Makefile.stage1: ocamldep, sed, camlp4 without Coq grammar extension
+  - Makefile.stage2: camlp4 with grammar.cma or q_constr.cmo
+  - Makefile.stage3: coqdep (.vo)
+
+* March 2010 (Pierre Letouzey).
+  Revised build system. In particular, no more stage1,2,3 :
+  - Stage3 was removed some time ago when coqdep was splitted into
+    coqdep_boot and full coqdep.
+  - Stage1,2 were replaced by brutal inclusion of all .d at the start
+    of Makefile.build, without trying to guess what could be done at
+    what time. Some initial inclusions hence _fail_, but "make" tries
+    again later and succeed.
+  - Btw, .ml4 are explicitely turned into .ml files, which stay after build.
+    By default, they are in binary ast format, see READABLE_ML4 option.
+
+* February 2014 (Pierre Letouzey).
+  Another revision of the build system. We avoid relying on the awkward
+  include-which-fails-but-works-finally-after-a-retry feature of gnu make.
+  This was working, but was quite hard to understand. Instead, we reuse
+  the idea of two explicit phases, but in a lighter way than in 2007.
+  The main Makefile calls Makefile.build twice :
+  - first for building grammar.cma (and q_constr.cmo), with a
+    restricted set of .ml4 (see variable BUILDGRAMMAR).
+  - then on the true target asked by the user.
+
+    
+---------------------------------------------------------------------------
+
 
 This file documents internals of the implementation of the build
 system. For what a Coq developer needs to know about the build system,
@@ -24,68 +41,47 @@ see build-system.txt .
 .ml4 files
 ----------
 
-.ml files corresponding to .ml4 files are created to keep ocamldep
-happy only. To ensure they are not used for compilation, they contain
-invalid OCaml.
-
+.ml4 are converted to .ml by camlp4. By default, they are produced
+in the binary ast format understood by ocamlc/ocamlopt/ocamldep.
+Pros:
+ - faster than parsing clear-text source file.
+ - no risk of editing them by mistake instead of the .ml4
+ - the location in the binary .ml are those of the initial .ml4,
+   hence errors are properly reported in the .ml4.
+Cons:
+ - This format may depend on your ocaml version, they should be
+   cleaned if you change your build environment.
+ - Unreadable in case you want to inspect this generated code.
+   For that, use make with the READABLE_ML4=1 option to switch to
+   clear-text generated .ml.
 
-multi-stage build
------------------
 
-Le processus de construction est séparé en trois étapes qui correspondent
-aux outils nécessaires pour calculer les dépendances de cette étape:
-
-stage1: ocamldep, sed , camlp4 sans fichiers de Coq
-stage2: camlp4 avec grammar.cma et/ou q_constr.cmo
-stage3: coqdep (.vo)
+Makefiles hierachy
+------------------
 
 Le Makefile a été séparé en plusieurs fichiers :
 
-- Makefile: coquille vide qui délègue les cibles à la bonne étape sauf
-  clean et les fichiers pour emacs (car ils sont en quelque sorte en
-  "stage0": aucun calcul de dépendance nécessaire).
+- Makefile: coquille vide qui lançant Makefile.build sauf pour
+  clean et quelques petites choses ne nécessitant par de calculs
+  de dépendances.
 - Makefile.common : définitions des variables (essentiellement des
   listes de fichiers)
-- Makefile.build : les règles de compilation sans inclure de
-  dépendances
-- Makefile.stage* : fichiers qui incluent les dépendances calculables
-  à cette étape ainsi que Makefile.build.
-
-The build needs to be cut in stages because make will not take into
-account one include when making another include.
+- Makefile.build : contient les regles de compilation, ainsi que
+  le "include" des dépendances (restreintes ou non selon la variable
+  BUILDGRAMMAR).
+- Makefile.doc : regles specifiques à la compilation de la documentation.
 
 
 Parallélisation
 ---------------
 
-Le découpage en étapes veut dire que le makefile est un petit peu
-moins parallélisable que strictement possible en théorie: par exemple,
-certaines choses faites en stage2 pourraient être faites en parallèle
-avec des choses de stage1. Nous essayons de minimiser cet effet, mais
-nous ne l'avons pas complètement éliminé parce que cela mènerait à un
-makefile très complexe. La minimisation est principalement que si on
-demande un objet spécifique (par exemple "make parsing/g_constr.cmx"),
-il est fait dans l'étape la plus basse possible (simplement), mais si
-un objet est fait comme dépendance de la cible demandée (par exemple
-dans un "make world"), il est fait le plus tard possible (par exemple,
-tout code OCaml non nécessaire pour coqdep ni grammar.cma ni
-q_constr.cmo est compilé en stage3 lors d'un "make world"; cela permet
-le parallélisme de compilation de code OCaml et de fichiers Coq (.v)).
-
-Le "(simplement)" ci-dessus veut dire que savoir si un fichier non
-nécessaire pour grammar.cma/q_constr.cmo peut en fait être fait en
-stage1 est compliqué avec make, alors nous retombons en général sur le
-stage2. La séparation entre le stage2 et stage3 est plus facile, donc
-l'optimisation ci-dessus s'y applique pleinement.
-
-En d'autres mots, nous avons au niveau conceptuel deux assignations
-d'étape pour chaque fichier:
-
- - l'étape la plus petite où nous savons qu'il peut être fait.
- - l'étape la plus grande où il peut être fait.
-
-Mais seule la première est gérée explicitement, la seconde est
-implicite.
+Il y a actuellement un double appel interne à "make -f Makefile.build",
+d'abord pour construire grammar.cma/q_constr.cmo, puis le reste.
+Cela signifie que ce makefile est un petit peu moins parallélisable
+que strictement possible en théorie: par exemple, certaines choses
+faites lors du second make pourraient être faites en parallèle avec
+le premier. En pratique, ce premier make va suffisemment vite pour
+que cette limitation soit peu gênante.
 
 
 FIND_VCS_CLAUSE
diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt
index d7cf396ff..31d9875ad 100644
--- a/dev/doc/build-system.txt
+++ b/dev/doc/build-system.txt
@@ -1,26 +1,8 @@
-Since July 2007, Coq features a build system overhauled by Pierre
-Corbineau and Lionel Elie Mamane.
-
----------------------------------------------------------------------
-WARNING:
-In March 2010 this build system has been heavily adapted by Pierre
-Letouzey. In particular there no more explicit stage1,2. Stage3
-was removed some time ago when coqdep was splitted into coqdep_boot
-and full coqdep. Ideas are still similar to what is describe below,
-but:
-1) .ml4 are explicitely turned into .ml files, which stay after build
-2) we let "make" handle the inclusion of .d without trying to guess
-   what could be done at what time. Some initial inclusions hence
-  _fail_, but "make" tries again later and succeed.
-
-TODO: remove obsolete sections below and better describe the new approach
------------------------------------------------------------------------
 
 This file documents what a Coq developer needs to know about the build
 system. If you want to enhance the build system itself (or are curious
-about its implementation details), see build-system.dev.txt .
-
-The build system is not at its optimal state, see TODO section.
+about its implementation details), see build-system.dev.txt, and in
+particular its initial HISTORY section.
 
 
 FAQ: special features used in this Makefile
@@ -51,22 +33,10 @@ $(subst ...), $(patsubst ...), $(shell ...), $(foreach ...), $(if ...)
 * 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*
-
-
-Stages in build system
-----------------------
-
-The build system is separated into three stages, corresponding to the
-tool(s) necessary to compute the dependencies necessary at this stage:
-
-stage1: ocamldep, sed, camlp4 without Coq extensions
-stage2: camlp4 with grammar.cma and/or q_constr.cmo
-stage3: coqdep (.vo)
-
-The file "Makefile" itself serves as minimum stage for targets that
-should not need any dependency (such as *clean*).
+and even retries again if necessary, but doesn't care if this build
+finally fails. We used to rely on this "feature", but this should not
+be the case anymore. We kept "-include" instead of "include" for
+avoiding warnings about initially non-existant files.
 
 Changes (for old-timers)
 ------------------------
@@ -97,37 +67,11 @@ save precious time:
 
  - Always ask for what you want directly (e.g. bin/coqtop,
    foo/bar.cmo, ...), don't do "make world" and interrupt
-   it when it has done what you want. This will try to minimise the
-   stage at which what you ask for is done (instead of maximising it
-   in order to maximise parallelism of the build process).
-
+   it when it has done what you want.
    For example, if you only want to test whether bin/coqtop still
    builds (and eventually start it to test your bugfix or new
-   feature), don't do "make world" and interrupt it when bin/coqtop is
-   built. Use "make bin/coqtop" or "make coqbinaries" or something
-   like that. This will avoid entering the stage 3, and cut build
-   system overhead by 50% (1.2s instead of 2.4 on writer's machine).
-
- - If you want to avoid all .ml4 files being recompiled only because
-   grammar.cma was rebuilt, do "make ml4depclean" once and then use
-   NO_RECOMPILE_ML4=1.
-
- - The CM_STAGE1=1 option to make will build all .cm* files mentioned
-   as targets on the command line in stage1. Whether this will work is
-   your responsibility. It should work for .ml files that don't depend
-   (nor directly nor indirectly through transitive closure of the
-   dependencies) on any .ml4 file, or where those dependencies can be
-   safely ignored in the current situation (e.g. all these .ml4 files
-   don't need to be recompiled).
-
-   This will avoid entering the stage2 (a reduction of 33% in
-   overhead, 0.4s on the writer's machine).
-
- - To jump directly into a stage (e.g. because you know nothing is to
-   be done in stage 1 or (1 and 2) or because you know that the target
-   you give can be, in this situation, done in a lower stage than the
-   build system dares to), use GOTO_STAGE=n. This will jump into stage
-   n and try to do the targets you gave in that stage.
+   feature), use "make bin/coqtop" or "make coqbinaries" or something
+   like that.
 
  - To disable all dependency recalculation, use the NO_RECALC_DEPS=1
    option. It disables REcalculation of dependencies, not calculation
@@ -135,12 +79,6 @@ save precious time:
    still created, but it is not updated every time the source file
    (e.g. .ml) is changed.
 
-General speed improvements:
-
- - When building both the native and bytecode versions, the
-   KEEP_ML4_PREPROCESSED=1 option may reduce global compilation time
-   by running camlp4o only once on every .ml4 file, at the expense of
-   readability of compilation error messages for .ml4 files.
 
 Dependencies
 ------------
@@ -178,166 +116,30 @@ Targets for cleaning various parts:
 .ml4 files
 ----------
 
-The camlp4-preprocessed version of FOO.ml4 is FOO.ml4-preprocessed and
-can be obtained with:
- make FOO.ml4-preprocessed
-
 If a .ml4 file uses a grammar extension from Coq (such as grammar.cma
 or q_constr.cmo), it must contain a line like:
  (*i camlp4deps: "grammar.cma q_constr.cmo" i*)
 
-If it uses a standard grammar extension, it must contain a line like:
- (*i camlp4use: "pa_ifdef.cmo" i*)
-
-It can naturally contain both a camlp4deps and a camlp4use line. Both
-are used for preprocessing. It is thus _not_ necessary to add a
-specific rule for a .ml4 file in the Makefile.build just because it
-uses grammar extensions.
-
-By default, the build system is geared towards development that may
-use the Coq grammar extensions, but not development of Coq's grammar
-extensions themselves. This means that .ml4 files are compiled
-directly (using ocamlc/opt's -pp option), without use of an
-intermediary .ml (or .ml4-preprocessed) file. This is so that if a
-compilation error occurs, the location in the error message is a
-location in the .ml4 file. If you are modifying the grammar
-extensions, you may be more interested in the location of the error in
-the .ml4-preprocessed file, so that you can see what your new grammar
-extension made wrong. In that case, use the KEEP_ML4_PREPROCESSED=1
-option. This will make compilation of a .ml4 file a two-stage process:
-
-1) create the .ml4-preprocessed file with camlp4o
-2) compile it with straight ocamlc/opt without preprocessor
-
-and will instruct make not to delete .ml4-preprocessed files
-automatically just because they are intermediary files, so that you
-can inspect them.
-
-If you add a _new_ grammar extension to Coq:
-
- - if it can be built at stage1, that is the .ml4 file does not use a
-   Coq grammar extension itself, then add it, and all .cmo files it
-   needs to STAGE1_TARGETS and STAGE_ML4 in Makefile.common. See the
-   handling of grammar.cma and q_constr.cmo for an example.
-
- - if it cannot be built at stage1, that is the .ml4 file itself needs
-   to be preprocessed with a Coq camlp4 grammar extension, then,
-   congratulations, you need to add a new stage between stage1 and
-   stage2.
+The use of (*i camlp4use: ... i*) to mention uses of standard
+extension such as IFDEF has been discontinued, the Makefile now
+always calls camlp4 with pa_macros.cmo and a few others by default.
+
+For debugging a Coq grammar extension, it could be interesting
+to use the READABLE_ML4=1 option, otherwise the generated .ml are
+in an internal binary format (see build-system.dev.txt).
+
 
 New files
 ---------
 
 For a new file, in most cases, you just have to add it to the proper
-file list(s) in Makefile.common, such as ARITHVO or TACTICS.
+file list(s):
+ - For .ml, in the corresponding .mllib (e.g. kernel/kernel.mllib)
+   These files are also used by the experimental ocamlbuild plugin,
+   which is quite touchy about them : be careful with order,
+   duplicated entries, whitespace errors, and do not mention .mli there.
+ - For .v, in the corresponding vo.itarget (e.g theories/Init/vo.itarget)
+ - The definitions in Makefile.common might have to be adapted too.
+ - If your file needs a specific rule, add it to Makefile.build
 
 The list of all ml4 files is not handled manually anymore.
-
-Exceptions are:
-
- - The file is necessary at stage1, that it is necessary to build the
-   Coq camlp4 grammar extensions. In this case, make sure it ends up
-   in STAGE1_CMO and (for .ml4 files) STAGE1_ML4. See the handling of
-   grammar.cma and/or q_constr.cmo for an example.
-
- - if the file needs to be compiled with -rectypes, add it to
-   RECTYPESML in Makefile.common. If it is a .ml4 file, implement
-   RECTYPESML4 or '(*i ocamlflags i*)'; see TODO.
-
- - the file needs a specific Makefile entry; add it to Makefile.build
-
- - the files produced from the added file do not match an existing
-   pattern or entry in "Makefile". (All the common cases of
-   .ml{,i,l,y,4}, .v, .c, ... files that produces (respectively)
-   .cm[iox], .vo, .glob, .o, ... files with the same basename are
-   already covered.) In this case, see section "New targets".
-
-New targets
------------
-
-If you want to add:
-
- - a new PHONY target to the build system, that is a target that is
-   not the name of the file it creates,
-
- - a normal target is not already mapped to a stage by "Makefile"
-
- then:
-
- - add the necessary rule to Makefile.build, if any
- - add the target to STAGEn_TARGETS, with n being the smallest stage
-   it can be built at, that is:
-   * 1 for OCaml code that doesn't use any Coq camlp4 grammar extension
-   * 2 for OCaml code that uses (directly or indirectly) a Coq
-       camlp4 grammar extension. Indirectly means a dependency of it
-       does.
-   * 3 for Coq (.v) code.
-
-   *or*
-
-   add a pattern matching the target to the pattern lists for the
-   smallest stage it can be built at in "Makefile".
-
-TODO
-----
-
-delegate pa_extend.cmo to camlp4use statements and remove it from
-standard camlp4 options.
-
-maybe manage compilation flags (such as -rectypes or the CoqIDE ones)
-from a
- (*i ocamlflags: "-rectypes" i*)
-statement in the .ml(4) files themselves, like camlp4use. The CoqIDE
-files could have
- (*i ocamlflags: "${COQIDEFLAGS}" i*)
-and COQIDEFLAGS is still defined (and exported by) the Makefile.build.
-
-Clean up doc/Makefile
-
-config/Makefile looks like it contains a lot of unused variables,
-clean that up (are any maybe used by nightly scripts on
-pauillac?). Also, the COQTOP variable from config/Makefile (and used
-in contribs) has a very poorly chosen name, because "coqtop" is the
-name of a Coq executable! In the coq Makefiles, $(COQTOPEXE) is used
-to refer to that executable.
-
-Promote the granular .glob handling to official way of doing things
-for Coq developments, that is implement it in coq_makefile and the
-contribs. Here are a few hints:
-
->> Les fichiers de constantes produits par -dump-glob sont maintenant
->> produits par fichier et sont ensuite concaténés dans
->> glob.dump. Ilsont produits par défaut (avec les bonnes
->> dépendances).
-
-> C'est une chose que l'on voulait faire aussi.
-
-(J'ai testé et débogué ce concept sur CoRN dans les derniers mois.)
-
-> Est-ce que vous sauriez modifier coq_makefile pour qu'il procède de
-> la même façon
-
-Dans cette optique, il serait alors plus propre de changer coqdep pour
-qu'il produise directement l'output que nous mettons maintenant dans
-les .v.d (qui est celui de coqdoc post-processé avec sed).
-
-Si cette manière de gérer les glob devient le standard béni
-officiellement par "the Coq development team", ne voudrions nous pas
-changer coqc pour qu'il produise FOO.glob lors de la compilation de
-FOO.v par défaut (sans argument "-dump-glob")?
-
-> et que la production de a.html par coqdoc n'ait une dépendance qu'en
-> les a.v et a.glob correspondant ?
-
-Je crois que coqdoc exige un glob-dump unique, il convient donc de
-concaténer les .glob correspondants. Soit un glob-dump global par
-projet (par Makefile), soit un glob-dump global par .v(o), qui
-contient son .glob et ceux de tous les .v(o) atteignables par le
-graphe des dépendances. CoRN contient déjà un outil de calcul de
-partie atteignable du graphe des dépendances (il y est pour un autre
-usage, pour calculer les .v à mettre dans les différents tarballs sur
-http://corn.cs.ru.nl/download.html; les parties partielles sont
-définies par liste de fichiers .v + toutes leurs dépendances
-(in)directes), il serait alors adéquat de le mettre dans les tools de
-Coq.
-