Implement KEEP_ML4_PREPROCESSED option in build system

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10561 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 51 insertions, 14 deletions

diff --git a/Makefile b/Makefile
index 0da3ac091..be1ee4ef2 100644
--- a/Makefile
+++ b/Makefile
@@ -112,10 +112,10 @@ ifdef CM_STAGE1
 $(CAML_OBJECT_PATTERNS): always
 	$(call stage-template,1)
 
-%.ml4.preprocessed: stage1
+%.ml4-preprocessed: stage1
 	$(call stage-template,2)
 else
-$(CAML_OBJECT_PATTERNS) %.ml4.preprocessed: stage1
+$(CAML_OBJECT_PATTERNS) %.ml4-preprocessed: stage1
 	$(call stage-template,2)
 endif
 
@@ -177,7 +177,7 @@ clean-ide:
 	rm -f ide/utf8_convert.ml
 
 ml4clean:
-	rm -f $(ML4FILESML) $(ML4FILESML:.ml=.ml4.preprocessed)
+	rm -f $(ML4FILESML) $(ML4FILESML:.ml=.ml4-preprocessed)
 
 ml4depclean:
 	find . -name '*.ml4.d' | xargs rm -f
diff --git a/Makefile.build b/Makefile.build
index 08a8a7cbc..86211d0c3 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -721,11 +721,11 @@ toplevel/mltop.optml: toplevel/mltop.ml4 # no camlp4deps here
 
 define rectypes-rules-template
 $(1:.ml=.cmo): $(1) | $(1).d
-	$(SHOW)'OCAMLC    -rectypes $$<' 
+	$(SHOW)'OCAMLC   -rectypes $$<' 
 	$(HIDE)$(OCAMLC) -rectypes $(BYTEFLAGS) -c $$<
 
 $(1:.ml=.cmx): $(1) | $(1).d
-	$(SHOW)'OCAMLOPT  -rectypes $$<'
+	$(SHOW)'OCAMLOPT -rectypes $$<'
 	$(HIDE)$(OCAMLOPT) -rectypes $(OPTFLAGS) -c $$<
 
 endef
@@ -776,10 +776,25 @@ endif
 	$(SHOW)'CC        $<'
 	$(HIDE)$(CC) -o $@ $(CFLAGS) $(CINCLUDES)  -c $<
 
+ifdef KEEP_ML4_PREPROCESSED
+.PRECIOUS: %.ml4-preprocessed
+%.cmo: %.ml4-preprocessed | %.ml4.ml.d
+	$(SHOW)'OCAMLC    $<'
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -c -impl $<
+
+%.cmx: %.ml4-preprocessed | %.ml4.ml.d
+	$(SHOW)'OCAMLOPT  $<'
+	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -c -impl $<
+else
 %.cmo: %.ml4 | %.ml4.ml.d %.ml4.d
 	$(SHOW)'OCAMLC4   $<'
 	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4USE) $<` `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl" -c -impl $<
 
+%.cmx: %.ml4 | %.ml4.ml.d %.ml4.d
+	$(SHOW)'OCAMLOPT4 $<'
+	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4USE) $<` `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl" -c -impl $<
+endif
+
 %.cmo: %.ml | %.ml.d
 	$(SHOW)'OCAMLC    $<'
 	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -c $<
@@ -788,10 +803,6 @@ endif
 	$(SHOW)'OCAMLC    $<'
 	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -c $<
 
-%.cmx: %.ml4 | %.ml4.ml.d %.ml4.d
-	$(SHOW)'OCAMLOPT4 $<'
-	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4USE) $<` `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl" -c -impl $<
-
 %.cmx: %.ml | %.ml.d
 	$(SHOW)'OCAMLOPT  $<'
 	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -c $<
@@ -804,8 +815,8 @@ endif
 	$(SHOW)'OCAMLYACC $<'
 	$(HIDE)$(OCAMLYACC) $<
 
-%.ml4.preprocessed: %.ml4 | %.ml4.d
-	$(SHOW)'CAMLP4O $<'
+%.ml4-preprocessed: %.ml4 | %.ml4.d
+	$(SHOW)'CAMLP4O   $<'
 	$(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $@ \
 	  || ( RV=$$?; rm -f "$@"; exit $${RV} )
 
@@ -827,7 +838,7 @@ else
 endif
 %.ml4.d: $(D_DEPEND_BEFORE_SRC) %.ml4
 	$(SHOW)'CAMLP4DEPS $<'
-	$(HIDE)( echo -n '$*.cmo $*.cmx $*.ml4.ml.d: $(SEP)' && $(CAMLP4DEPS) "$<" ) > "$@" \
+	$(HIDE)( echo -n '$*.cmo $*.cmx $*.ml4.ml.d $*.ml4-preprocessed: $(SEP)' && $(CAMLP4DEPS) "$<" ) > "$@" \
 	  || ( RV=$$?; rm -f "$@"; exit $${RV} )
 
 %.ml4.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml4 $(D_DEPEND_AFTER_SRC) $(GENFILES) $(ML4FILES:.ml4=.ml) %.ml4.d
diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt
index e4ecf9e5f..f43e21963 100644
--- a/dev/doc/build-system.txt
+++ b/dev/doc/build-system.txt
@@ -90,6 +90,13 @@ save precious time:
    still created, but it is not updated every time the source file
    (e.g. .ml) is changes.
 
+General speed improvements:
+
+ - When building both the native and bytecode versions, the
+   KEEP_ML4_PREPROCESSED=1 option may reduce global compilation time
+   by running camp4o only once on every .ml4 file, at the expense of
+   readability of compilation error messages for .ml4 files.
+
 Dependencies
 ------------
 
@@ -126,9 +133,9 @@ Targets for cleaning various parts:
 .ml4 files
 ----------
 
-The camlp4-preprocessed version of FOO.ml4 is FOO.ml4.preprocessed and
+The camlp4-preprocessed version of FOO.ml4 is FOO.ml4-preprocessed and
 can be obtained with:
- make FOO.ml4.preprocessed
+ 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:
@@ -142,6 +149,25 @@ 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