Makefile: the .ml of .ml4 are now produced explicitely (in binary ast form)

- This way, the Makefile.build gets shorter and simplier, with a few nasty
   hacks removed.
 - In particular, we stop creating dummy .ml of .ml4 early "to please ocamldep".
   Instead, we now use ocamldep -modules, and process its output via coqdep_boot.
   This ways, *.cm* of .ml4 are correctly located, even when some .ml files
   aren't generated yet.
 - There is no risk of editing the .ml of a .ml4 by mistake, since it is by
   default in a binary format (cf pr_o.cmo and variable READABLE_ML4).
   M-x next-error still open the right .ml4 at the right location.
 - mltop.byteml is now mltop.ml, while mltop.optml keeps its name
 - .ml of .ml4 are added to .gitignore

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

1 files changed, 42 insertions, 66 deletions

diff --git a/Makefile.build b/Makefile.build
index fe69326d7f..4303798ee6 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -86,6 +86,12 @@ TIMECMD=	# is "'time -p'" to get compilation time of .v
 
 BOOTCOQTOP:=$(TIMECMD) $(BESTCOQTOP) -boot $(COQOPTS)
 
+ifdef READABLE_ML4
+ PR_O = pr_o.cmo
+else
+ PR_O =
+endif
+
 ###########################################################################
 # Infrastructure for the rest of the Makefile
 ###########################################################################
@@ -662,25 +668,23 @@ parsing/grammar.cma: | parsing/grammar.mllib.d
 
 # toplevel/mltop.ml4 (ifdef Byte)
 
-toplevel/mltop.cmo: toplevel/mltop.byteml | toplevel/mltop.ml4.ml.d toplevel/mltop.ml4.d
-	$(SHOW)'OCAMLC    $<'	
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -c -impl $< -o $@
+## NB: mltop.ml correspond to the byte version (and hence need no special rules)
+## while the opt version is in mltop.optml. Since mltop.optml uses mltop.ml.d
+## as dependency file, be sure to import the same modules in the different sections
+## of the ml4
 
-toplevel/mltop.cmx: toplevel/mltop.optml | toplevel/mltop.ml4.ml.d toplevel/mltop.ml4.d
-	$(SHOW)'OCAMLOPT  $<'	
+toplevel/mltop.cmx: toplevel/mltop.optml | toplevel/mltop.ml.d toplevel/mltop.ml4.d
+	$(SHOW)'OCAMLOPT    $<'
 	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -c -impl $< -o $@
 
-## This works dependency-wise because the dependencies of the
-## .{opt,byte}ml files are those we deduce from the .ml4 file.
-## In other words, the Byte-only code doesn't import a new module.
-toplevel/mltop.byteml: toplevel/mltop.ml4 config/Makefile # no camlp4deps here
-	$(SHOW)'CAMLP4O   $<'	
-	$(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` \
+toplevel/mltop.ml: toplevel/mltop.ml4 config/Makefile # no camlp4deps here
+	$(SHOW)'CAMLP4O   $<'
+	$(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) $(PR_O) `$(CAMLP4USE) $<` \
 	  -DByte -DHasDynlink -impl $< $(TOTARGET)
 
-toplevel/mltop.optml: toplevel/mltop.ml4 config/Makefile # no camlp4deps here 
-	$(SHOW)'CAMLP4O   $<'	
-	$(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` \
+toplevel/mltop.optml: toplevel/mltop.ml4 config/Makefile # no camlp4deps here
+	$(SHOW)'CAMLP4O   $<'
+	$(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) $(PR_O) `$(CAMLP4USE) $<` \
 	  $(NATDYNLINKDEF) -impl $< $(TOTARGET)
 
 # pretty printing of the revision number when compiling a checked out
@@ -750,25 +754,6 @@ checker/%.cmi: checker/%.mli | checker/%.mli.d
 	$(SHOW)'OCAMLC    $<'
 	$(HIDE)cd $(dir $<) && $(OCAMLC) -ccopt "$(CFLAGS)" -c $(notdir $<)
 
-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 $<
@@ -808,9 +793,9 @@ plugins/%_mod.ml: plugins/%.mllib
 
 .SECONDARY: $(filter plugins/%,$(MLLIBFILES:%.mllib=%_mod.ml))
 
-%.ml4-preprocessed: %.ml4 | %.ml4.d
+%.ml: %.ml4 | %.ml4.d
 	$(SHOW)'CAMLP4O   $<'
-	$(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< $(TOTARGET)
+	$(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) $(PR_O) `$(CAMLP4USE) $<` `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< $(TOTARGET)
 
 %.vo %.glob: %.v states/initial.coq $(INITPLUGINSBEST) $(VO_TOOLS_STRICT) | %.v.d  $(VO_TOOLS_ORDER_ONLY)
 	$(SHOW)'COQC      $<'
@@ -833,58 +818,49 @@ ifdef NO_RECOMPILE_ML4
 else
   SEP:=
 endif
+
+# We now use coqdep_boot to wrap around ocamldep -modules, since it is aware
+# of .ml4 files
+
+OCAMLDEP_NG = $(COQDEPBOOT) -mldep $(OCAMLDEP)
+
 %.ml4.d: $(D_DEPEND_BEFORE_SRC) %.ml4
 	$(SHOW)'CAMLP4DEPS $<'
-	$(HIDE)( printf "%s" '$*.cmo $*.cmx $*.ml4.ml.d $*.ml4-preprocessed: $(SEP)' && $(CAMLP4DEPS) "$<" ) $(TOTARGET)
-
-%.ml4.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml4 $(D_DEPEND_AFTER_SRC) $(GENFILES) $(ML4FILESML) %.ml4.d
-#Critical section:
-# Nobody (in a make -j) should touch the .ml file here.
-	$(SHOW)'OCAMLDEP4 $<'
-	$(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< -o $*.ml \
-	  || ( RV=$$?; rm -f "$*.ml"; exit $${RV} )
-	$(HIDE)$(OCAMLDEP) $(DEPFLAGS) $*.ml | sed '' $(TOTARGET)
-	$(HIDE)echo "let keep_ocamldep_happy Do_not_compile_me = assert false" > $*.ml
-#End critical section
-
-checker/%.ml.d: $(D_DEPEND_BEFORE_SRC) checker/%.ml $(D_DEPEND_AFTER_SRC)
+	$(HIDE)( printf "%s" '$*.ml: $(SEP)' && $(CAMLP4DEPS) "$<" ) $(TOTARGET)
+
+checker/%.ml.d: $(D_DEPEND_BEFORE_SRC) checker/%.ml $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES)
 	$(SHOW)'OCAMLDEP  $<'
-	$(HIDE)$(OCAMLDEP) -slash $(LOCALCHKLIBS) "$<" | sed '' $(TOTARGET)
+	$(HIDE)$(OCAMLDEP_NG) -slash $(LOCALCHKLIBS) "$<" $(TOTARGET)
 
-checker/%.mli.d: $(D_DEPEND_BEFORE_SRC) checker/%.mli $(D_DEPEND_AFTER_SRC)
+checker/%.mli.d: $(D_DEPEND_BEFORE_SRC) checker/%.mli $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES)
 	$(SHOW)'OCAMLDEP  $<'
-	$(HIDE)$(OCAMLDEP) -slash $(LOCALCHKLIBS) "$<" | sed '' $(TOTARGET)
+	$(HIDE)$(OCAMLDEP_NG) -slash $(LOCALCHKLIBS) "$<" $(TOTARGET)
 
-%.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml $(D_DEPEND_AFTER_SRC) $(GENFILES) $(ML4FILESML)
+%.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES)
 	$(SHOW)'OCAMLDEP  $<'
-	$(HIDE)$(OCAMLDEP) $(DEPFLAGS) "$<" | sed '' $(TOTARGET)
+	$(HIDE)$(OCAMLDEP_NG) $(DEPFLAGS) "$<" $(TOTARGET)
 
-%.mli.d: $(D_DEPEND_BEFORE_SRC) %.mli $(D_DEPEND_AFTER_SRC) $(GENFILES) $(ML4FILESML)
+%.mli.d: $(D_DEPEND_BEFORE_SRC) %.mli $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES)
 	$(SHOW)'OCAMLDEP  $<'
-	$(HIDE)$(OCAMLDEP) $(DEPFLAGS) "$<" | sed '' $(TOTARGET)
+	$(HIDE)$(OCAMLDEP_NG) $(DEPFLAGS) "$<" $(TOTARGET)
 
-checker/%.mllib.d: $(D_DEPEND_BEFORE_SRC) checker/%.mllib $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT)
+checker/%.mllib.d: $(D_DEPEND_BEFORE_SRC) checker/%.mllib $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES)
 	$(SHOW)'COQDEP  $<'
-	$(HIDE)$(COQDEPBOOT) -slash -boot -I checker -c "$<" $(TOTARGET)
+	$(HIDE)$(COQDEPBOOT) -slash -I checker -c "$<" $(TOTARGET)
 
-%.mllib.d: $(D_DEPEND_BEFORE_SRC) %.mllib $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT)
+%.mllib.d: $(D_DEPEND_BEFORE_SRC) %.mllib $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES)
 	$(SHOW)'COQDEP  $<'
-	$(HIDE)$(COQDEPBOOT) -slash -boot -I kernel -I tools/coqdoc -c "$<" $(TOTARGET)
-
-## Veerry nasty hack to keep ocamldep happy
-%.ml: | %.ml4
-	$(SHOW)'TOUCH     $@'
-	$(HIDE)echo "let keep_ocamldep_happy Do_not_compile_me = assert false" $(TOTARGET)
+	$(HIDE)$(COQDEPBOOT) -slash -I kernel -I tools/coqdoc -c "$<" $(TOTARGET)
 
 %.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENVFILES)
 	$(SHOW)'COQDEP    $<'
-	$(HIDE)$(COQDEPBOOT) $(DEPNATDYN) -slash -boot "$<" $(TOTARGET)
+	$(HIDE)$(COQDEPBOOT) $(DEPNATDYN) -slash "$<" $(TOTARGET)
 
 %.c.d: $(D_DEPEND_BEFORE_SRC) %.c $(D_DEPEND_AFTER_SRC) $(GENHFILES)
 	$(SHOW)'CCDEP     $<'
 	$(HIDE)$(CC) -MM -MQ "$@" -MQ "$(<:.c=.o)" $(CFLAGS) -isystem $(CAMLHLIB) $< $(TOTARGET)
 
-.SECONDARY: $(GENFILES)
+.SECONDARY: $(GENFILES) $(ML4FILESML)
 
 ###########################################################################
 # this sets up developper supporting stuff