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)

1 files changed, 12 insertions, 22 deletions

diff --git a/dev/doc/build-system.dev.txt b/dev/doc/build-system.dev.txt
index af1120e97b..fefcb0937a 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