Yet another Makefile reform : a unique phase without nasty make tricks

 We're back to a unique build phase (as before e372b72), but without
 relying on the awkward include-deps-failed-lets-retry feature of make.
 Since PMP has made grammar/ self-contained, we could now build
 grammar.cma in a rather straightforward way, no need for
 a specific sub-call to $(MAKE) for that. The dependencies between
 files of grammar/ are stated explicitely, since .d files aren't
 fully available initially.

 Some Makefile simplifications, for instance remove the CAMLP4DEPS
 shell horror. Instead, we generalize the use of two different
 filename extensions :
  - a .mlp do not need grammar.cma (they are in grammar/ and tools/compat5*.mlp)
  - a .ml4 is now always preprocessed with grammar.cma (and q_constr.cmo),
    except coqide_main.ml4 and its specific rule

 Note that we do not generate .ml4.d anymore (thanks to the .mlp vs.
 .ml4 dichotomy)

2 files changed, 22 insertions, 27 deletions

diff --git a/dev/doc/build-system.dev.txt b/dev/doc/build-system.dev.txt
index af1120e97..fefcb0937 100644
--- a/dev/doc/build-system.dev.txt
+++ b/dev/doc/build-system.dev.txt
@@ -30,6 +30,11 @@ HISTORY:
     restricted set of .ml4 (see variable BUILDGRAMMAR).
   - then on the true target asked by the user.
 
+* June 2016 (Pierre Letouzey)
+  The files in grammar/ are now self-contained, we could compile
+  grammar.cma (and q_constr.cmo) directly, no need for a separate
+  subcall to make nor awkward include-failed-and-retry.
+
     
 ---------------------------------------------------------------------------
 
@@ -59,29 +64,14 @@ Cons:
 Makefiles hierachy
 ------------------
 
-Le Makefile a été séparé en plusieurs fichiers :
-
-- 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 : 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
----------------
+The Makefile is separated in several files :
 
-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.
+- Makefile: wrapper that triggers a call to Makefile.build, except for
+  clean and a few other little things doable without dependency analysis.
+- Makefile.common : variable definitions (mostly lists of files or
+  directories)
+- Makefile.build : contains compilation rules, and the "include" of dependencies
+- Makefile.doc : specific rules for compiling the documentation.
 
 
 FIND_VCS_CLAUSE
diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt
index 31d9875ad..4593a6ad5 100644
--- a/dev/doc/build-system.txt
+++ b/dev/doc/build-system.txt
@@ -113,15 +113,20 @@ Targets for cleaning various parts:
 
  - docclean: clean documentation
 
-.ml4 files
-----------
+.ml4/.mlp files
+---------------
 
-If a .ml4 file uses a grammar extension from Coq (such as grammar.cma
-or q_constr.cmo), it must contain a line like:
+There is now two kinds of preprocessed files : 
+ - a .mlp do not need grammar.cma (they are in grammar/ and tools/compat5*.mlp)
+ - a .ml4 is now always preprocessed with grammar.cma (and q_constr.cmo),
+   except coqide_main.ml4 and its specific rule
+
+This classification replaces the old mechanism of declaring the use
+of a grammar extension via a line of the form:
  (*i camlp4deps: "grammar.cma q_constr.cmo" i*)
 
 The use of (*i camlp4use: ... i*) to mention uses of standard
-extension such as IFDEF has been discontinued, the Makefile now
+extension such as IFDEF has also 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