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)

12 files changed, 109 insertions, 105 deletions

diff --git a/Makefile b/Makefile
index c5415d9f6..17ff8041f 100644
--- a/Makefile
+++ b/Makefile
@@ -63,15 +63,10 @@ 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
 
 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')
 
@@ -150,10 +145,7 @@ endif
 
 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:
diff --git a/Makefile.build b/Makefile.build
index dbf60afb7..18b1e4fb4 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -25,29 +25,23 @@ world: revision coq coqide documentation
 include Makefile.common
 include Makefile.doc
 
-# In a first phase, we restrict to the basic .ml4 (the ones without grammar.cma)
+MLFILES := $(MLSTATICFILES) $(GENMLFILES) $(ML4FILES:.ml4=.ml)
+DEPENDENCIES := \
+ $(addsuffix .d, $(MLFILES) $(MLIFILES) $(MLLIBFILES) $(CFILES) $(VFILES))
 
-ifdef BUILDGRAMMAR
- MLFILES := $(MLSTATICFILES) $(GENMLFILES) $(ML4BASEFILES:.ml4=.ml)
- CURFILES := $(MLFILES) $(MLIFILES) $(ML4BASEFILES) grammar/grammar.mllib
-else
- MLFILES := $(MLSTATICFILES) $(GENMLFILES) $(ML4FILES:.ml4=.ml)
- CURFILES := $(MLFILES) $(MLIFILES) $(ML4FILES) $(MLLIBFILES) $(CFILES) $(VFILES)
-endif
+# This include below will lauch the build of all concerned .d.
+# The - at front is for disabling warnings about currently missing ones.
+# For creating the missing .d, make will recursively build things like
+# coqdep_boot (for the .v.d files) or grammar.cma (for .ml4 -> .ml -> .ml.d).
 
-CURDEPS:=$(addsuffix .d, $(CURFILES))
+-include $(DEPENDENCIES)
 
 # 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.
 
-.SECONDARY: $(CURDEPS) $(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.
-
--include $(CURDEPS)
+.SECONDARY: $(DEPENDENCIES) $(GENFILES) $(ML4FILES:.ml4=.ml)
 
 
 ###########################################################################
@@ -117,7 +111,7 @@ $(if $(findstring $@,$(PRIVATEBINARIES)),\
 $(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(CUSTOM) -o $@ $(1) $(addsuffix .cma,$(2)) $^)
 endef
 
-CAMLP4DEPS=$(shell LC_ALL=C sed -n -e 's@^(\*.*camlp4deps: "\(.*\)".*@\1@p' $(1) \#))
+CAMLP4DEPS:=tools/compat5.cmo grammar/grammar.cma grammar/q_constr.cmo
 ifeq ($(CAMLP4),camlp5)
 CAMLP4USE=pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION)
 else
@@ -139,7 +133,6 @@ else
 P4CMA:=camlp4lib.cma
 endif
 
-
 ###########################################################################
 # Infrastructure for the rest of the Makefile
 ###########################################################################
@@ -203,6 +196,74 @@ kernel/copcodes.ml: kernel/byterun/coq_instruct.h
 	sed -n -e '/^enum/p' -e 's/,//g' -e '/^  /p' $< | \
 	awk -f kernel/make-opcodes $(TOTARGET)
 
+
+###########################################################################
+#  grammar/grammar.cma
+###########################################################################
+
+## In this part, we compile grammar/grammar.cma (and grammar/q_constr.cmo)
+## without relying on .d dependency files, for bootstraping the creation
+## and inclusion of these .d files
+
+## Explicit dependencies for grammar stuff
+
+GRAMBASEDEPS := grammar/gramCompat.cmo grammar/q_util.cmi
+GRAMCMO := \
+ grammar/gramCompat.cmo grammar/q_util.cmo \
+ grammar/argextend.cmo grammar/tacextend.cmo grammar/vernacextend.cmo
+
+grammar/q_util.cmi : grammar/gramCompat.cmo
+grammar/argextend.cmo : $(GRAMBASEDEPS)
+grammar/q_constr.cmo : $(GRAMBASEDEPS)
+grammar/q_util.cmo : $(GRAMBASEDEPS)
+grammar/tacextend.cmo : $(GRAMBASEDEPS) grammar/argextend.cmo
+grammar/vernacextend.cmo : $(GRAMBASEDEPS) grammar/tacextend.cmo \
+ grammar/argextend.cmo
+
+## Ocaml compiler with the right options and -I for grammar
+
+GRAMC := $(OCAMLFIND) ocamlc $(CAMLFLAGS) $(CAMLDEBUG) $(USERFLAGS) \
+ -I $(MYCAMLP4LIB) -I grammar
+
+## Specific rules for grammar.cma
+
+grammar/grammar.cma : $(GRAMCMO)
+	$(SHOW)'Testing $@'
+	@touch test.mlp
+	$(HIDE)$(CAMLP4O) -I $(MYCAMLP4LIB) $^ -impl test.mlp -o test.ml
+	$(HIDE)$(GRAMC) test.ml -o test-grammar
+	@rm -f test-grammar test.*
+	$(SHOW)'OCAMLC -a $@'   
+	$(HIDE)$(GRAMC) $^ -linkall -a -o $@
+
+## Support of Camlp5 and Camlp5
+
+# NB: compatibility modules for camlp4:
+# - tools/compat5.cmo changes GEXTEND into EXTEND. Safe, always loaded
+# - tools/compat5b.cmo changes EXTEND into EXTEND Gram. Interact badly with
+#    syntax such that VERNAC EXTEND, we only load it in grammar/
+
+ifeq ($(CAMLP4),camlp4)
+ COMPATCMO:=tools/compat5.cmo tools/compat5b.cmo
+ GRAMP4USE:=$(COMPATCMO) -D$(CAMLVERSION)
+ GRAMPP:=$(CAMLP4O) -I $(MYCAMLP4LIB) $(GRAMP4USE) $(CAMLP4COMPAT) -impl
+else
+ COMPATCMO:=
+ GRAMP4USE:=$(COMPATCMO) pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION)
+ GRAMPP:=$(CAMLP4O) -I $(MYCAMLP4LIB) $(GRAMP4USE) $(CAMLP4COMPAT) -impl
+endif
+
+## Rules for standard .mlp and .mli files in grammar/
+
+grammar/%.cmo: grammar/%.mlp | $(COMPATCMO)
+	$(SHOW)'OCAMLC -c -pp $<'
+	$(HIDE)$(GRAMC) -c -pp '$(GRAMPP)' -impl $<
+
+grammar/%.cmi: grammar/%.mli
+	$(SHOW)'OCAMLC -c $<'
+	$(HIDE)$(GRAMC) -c $<
+
+
 ###########################################################################
 # Main targets (coqmktop, coqtop.opt, coqtop.byte)
 ###########################################################################
@@ -608,8 +669,8 @@ tools: $(TOOLS) $(DEBUGPRINTERS) $(OCAMLLIBDEP)
 # coqdep_boot : a basic version of coqdep, with almost no dependencies.
 
 # Here it is important to mention .ml files instead of .cmo in order
-# to avoid using implicit rules and hence .ml.d files that would need
-# coqdep_boot.
+# to avoid using implicit rules : at the time coqdep_boot is being built,
+# some .ml.d files may still be missing or not taken in account yet by make.
 
 COQDEPBOOTSRC := \
  lib/minisys.ml \
@@ -621,13 +682,13 @@ $(COQDEPBOOT): $(COQDEPBOOTSRC)
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml, -I tools, unix)
 
-OCAMLLIBDEPSRC:= tools/ocamllibdep.ml
+# Same for ocamllibdep
 
-$(OCAMLLIBDEP): $(OCAMLLIBDEPSRC)
+$(OCAMLLIBDEP): tools/ocamllibdep.ml
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml, -I tools, unix)
 
-# the full coqdep
+# The full coqdep (unused by this build, but distributed by make install)
 
 $(COQDEP): $(patsubst %.cma,%$(BESTLIB),$(COQDEPCMO:.cmo=$(BESTOBJ)))
 	$(SHOW)'OCAMLBEST -o $@'
@@ -681,8 +742,6 @@ tools/compat5b.cmo: tools/compat5b.mlp
 else
 tools/compat5.cmo: tools/compat5.ml
 	$(OCAMLC) -c $<
-tools/compat5b.cmo: tools/compat5b.ml
-	$(OCAMLC) -c $<
 endif
 
 ###########################################################################
@@ -901,15 +960,6 @@ dev/printers.cma: | dev/printers.mllib.d
 	$(SHOW)'OCAMLC -a $@'   
 	$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -thread $(SYSCMA) $(P4CMA) $^ -linkall -a -o $@
 
-grammar/grammar.cma: | grammar/grammar.mllib.d
-	$(SHOW)'Testing $@'
-	@touch test.ml4
-	$(HIDE)$(CAMLP4O) $(CAMLP4FLAGS) $^ -impl test.ml4 -o test.ml
-	$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) test.ml -o test-grammar
-	@rm -f test-grammar test.*
-	$(SHOW)'OCAMLC -a $@'   
-	$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $^ -linkall -a -o $@
-
 ide/coqide_main.ml: ide/coqide_main.ml4 config/Makefile # no camlp4deps here
 	$(SHOW)'CAMLP4O   $<'
 	$(HIDE)$(CAMLP4O) $(CAMLP4FLAGS) $(PR_O) $(CAMLP4USE) -D$(IDEINT) -impl $< -o $@
@@ -1039,15 +1089,10 @@ plugins/%_mod.ml: plugins/%.mllib
 	$(HIDE)sed -e "s/\([^ ]\{1,\}\)/let _=Mltop.add_known_module\"\1\" /g" $< > $@
 	$(HIDE)echo "let _=Mltop.add_known_module\"$(notdir $*)\"" >> $@
 
-# NB: compatibility modules for camlp4: 
-# - tools/compat5.cmo changes GEXTEND into EXTEND. Safe, always loaded
-# - tools/compat5b.cmo changes EXTEND into EXTEND Gram. Interact badly with
-#    syntax such that VERNAC EXTEND, we only load it for a few files via camlp4deps
-
-%.ml: %.ml4 | %.ml4.d tools/compat5.cmo tools/compat5b.cmo
+%.ml: %.ml4 | $(CAMLP4DEPS)
 	$(SHOW)'CAMLP4O   $<'
-	$(HIDE)$(CAMLP4O) $(CAMLP4FLAGS) $(PR_O) tools/compat5.cmo \
-	  $(call CAMLP4DEPS,$<) $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< -o $@
+	$(HIDE)$(CAMLP4O) $(CAMLP4FLAGS) $(PR_O) \
+	  $(CAMLP4DEPS) $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< -o $@
 
 %.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP) | %.v.d
 	$(SHOW)'COQC      $<'
@@ -1063,13 +1108,6 @@ endif
 # Dependencies
 ###########################################################################
 
-# .ml4.d contains the dependencies to generate the .ml from the .ml4
-# NOT to generate object code.
-
-%.ml4.d: $(D_DEPEND_BEFORE_SRC) %.ml4
-	$(SHOW)'CAMLP4DEPS $<'
-	$(HIDE)echo "$*.ml: $(if $(NO_RECOMPILE_ML4),$(ORDER_ONLY_SEP)) $(call CAMLP4DEPS,$<)" $(TOTARGET)
-
 # Since OCaml 3.12.1, we could use again ocamldep directly, thanks to
 # the option -ml-synonym
 
diff --git a/Makefile.common b/Makefile.common
index 2244e6867..5bf49ed76 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -63,7 +63,7 @@ CSDPCERT:=plugins/micromega/csdpcert$(EXE)
 CORESRCDIRS:=\
   config 	lib		kernel		kernel/byterun	library \
   proofs 	tactics 	pretyping	interp		stm \
-  toplevel	parsing	printing	grammar	        intf	engine	ltac
+  toplevel	parsing 	printing	intf	engine	ltac
 
 PLUGINS:=\
   omega		romega 		micromega 	quote \
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
diff --git a/grammar/argextend.ml4 b/grammar/argextend.mlp
index 8e06adce9..eaaa7f025 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.mlp
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4deps: "tools/compat5b.cmo" i*)
-
 open Q_util
 open GramCompat
 
diff --git a/grammar/gramCompat.ml4 b/grammar/gramCompat.mlp
index 6246da7bb..6246da7bb 100644
--- a/grammar/gramCompat.ml4
+++ b/grammar/gramCompat.mlp
diff --git a/grammar/q_constr.ml4 b/grammar/q_constr.mlp
index af90f5f2a..8e1587ec3 100644
--- a/grammar/q_constr.ml4
+++ b/grammar/q_constr.mlp
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4deps: "tools/compat5b.cmo" i*)
-
 open Q_util
 open GramCompat
 open Pcaml
diff --git a/grammar/q_util.ml4 b/grammar/q_util.mlp
index 2d5c40894..2d5c40894 100644
--- a/grammar/q_util.ml4
+++ b/grammar/q_util.mlp
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.mlp
index 8593bad5d..1d52a85a5 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.mlp
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4deps: "tools/compat5b.cmo" i*)
-
 (** Implementation of the TACTIC EXTEND macro. *)
 
 open Q_util
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.mlp
index 1611de39c..fa8610fb9 100644
--- a/grammar/vernacextend.ml4
+++ b/grammar/vernacextend.mlp
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4deps: "tools/compat5b.cmo" i*)
-
 (** Implementation of the VERNAC EXTEND macro. *)
 
 open Q_util
diff --git a/tools/compat5b.ml b/tools/compat5b.ml
deleted file mode 100644
index 37cb487c5..000000000
--- a/tools/compat5b.ml
+++ /dev/null
@@ -1,13 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* This file is meant for camlp5, for which there is nothing to
-   add to gain camlp5 compatibility :-).
-
-   See [compat5b.mlp] for the [camlp4] counterpart
-*)