A cleaner solution to "make deletes .ml4.d files -> infinite loop" problem

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

8 files changed, 18 insertions, 34 deletions

diff --git a/Makefile b/Makefile
index 6e17851a3a..7c94fb6548 100644
--- a/Makefile
+++ b/Makefile
@@ -57,14 +57,11 @@ define stage-template
 endef
 endif
 
-stage0: always
-	$(call stage-template,0)
-
-%.o: stage0
+%.o: always
 	$(call stage-template,1)
 
 #STAGE1_TARGETS includes all object files necessary for $(STAGE1)
-stage1 $(STAGE1_TARGETS): stage0
+stage1 $(STAGE1_TARGETS): always
 	$(call stage-template,1)
 
 %.cmo %.cmx %.cmi %.cma %.cmxa %.ml4.preprocessed: stage1
diff --git a/Makefile.build b/Makefile.build
index 3887dfdec7..38cdd53be6 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -849,7 +849,7 @@ endif
 	$(SHOW)'CCDEP     $<'
 	$(HIDE)$(CC) -MM -MG -MQ "$@" -MQ "$(<:.c=.o)" $(CFLAGS) $(CINCLUDES) $< > $@
 
-.PRECIOUS: %.ml %.mli %.d %.ml4.d kernel/copcodes.ml
+.SECONDARY: $(GENFILES)
 
 ###########################################################################
 # this sets up developper supporting stuff
diff --git a/Makefile.common b/Makefile.common
index 8c14d2b9e9..3bf6ae5028 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -440,6 +440,7 @@ MLIFILES := $(shell find . '(' -name '*.mli' ')' -printf '%P\n') \
   $(GENMLIFILES)
 ML4FILES := $(shell find . '(' -name '*.ml4' ')' -printf '%P\n')
 VFILES   := $(shell find . '(' -name '*.v'   ')' -printf '%P\n')
+CFILES   := $(shell find kernel/byterun -name '*.c' -printf '%p\n')
 
 ML4FILESML:= $(ML4FILES:.ml4=.ml)
 
@@ -786,7 +787,7 @@ STAGE1_TARGETS:= $(STAGE1) \
   $(filter-out parsing/q_constr.cmo,$(STAGE1_CMO)) \
   $(STAGE1_CMO:.cmo=.cmi) $(STAGE1_CMO:.cmo=.cmx) $(GENFILES) \
   source-doc revision toplevel/mltop.byteml toplevel/mltop.optml \
-  $(GRAMMARML4:.ml4=.ml4.preprocessed)
+  $(STAGE1_ML4:.ml4=.ml4.preprocessed)
 STAGE2_TARGETS:=$(COQBINARIES) lib kernel byterun library proofs tactics \
   interp parsing pretyping highparsing toplevel hightactics \
   coqide-binaries coqide-byte coqide-opt $(COQIDEOPT) $(COQIDEBYTE) $(COQIDE) \
diff --git a/Makefile.stage0 b/Makefile.stage0
deleted file mode 100644
index be13543205..0000000000
--- a/Makefile.stage0
+++ /dev/null
@@ -1,21 +0,0 @@
-#######################################################################
-#  v      #   The Coq Proof Assistant  /  The Coq Development Team    #
-# <O___,, #        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              #
-#   \VV/  #############################################################
-#    //   #      This file is distributed under the terms of the      #
-#         #       GNU Lesser General Public License Version 2.1       #
-#######################################################################
-
-include Makefile.build
-
-.PHONY: stage0
-stage0: $(ML4FILES:.ml4=.ml4.d)
-
-##Somehow, make decides to delete the .ml4.d files if they are -include'd.
-##This "stage0" hack to have them include'd, but no spurious error message
-##on bootstrap. GNU Make bug suspected.
-
-# For emacs: 
-# Local Variables: 
-# mode: makefile 
-# End:
diff --git a/Makefile.stage1 b/Makefile.stage1
index e085122064..a60d388fc6 100644
--- a/Makefile.stage1
+++ b/Makefile.stage1
@@ -8,13 +8,21 @@
 
 include Makefile.build
 
-include $(ML4FILES:.ml4=.ml4.d)
+# All 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.
+-include $(ML4FILES:.ml4=.ml4.d)
+.SECONDARY: $(ML4FILES:.ml4=.ml4.d)
 -include $(MLFILES:.ml=.ml.d)
+.SECONDARY: $(MLFILES:.ml=.ml.d)
 -include $(MLIFILES:.mli=.mli.d)
+.SECONDARY: $(MLIFILES:.mli=.mli.d)
 ##Depends upon the fact that all .ml4.d for stage1 files are empty
 -include $(STAGE1_ML4:.ml4=.ml4.ml.d)
--include parsing/q_constr.ml4.ml.d
--include $(shell find kernel/byterun -name '*.c' -printf '%p.d\n')
+.SECONDARY: $(STAGE1_ML4:.ml4=.ml4.ml.d)
+-include  $(CFILES:.c=.c.d)
+.SECONDARY: $(CFILES:.c=.c.d)
 
 .PHONY: stage1
 stage1: $(STAGE1)
diff --git a/Makefile.stage2 b/Makefile.stage2
index 97a10118ee..6fe020be9f 100644
--- a/Makefile.stage2
+++ b/Makefile.stage2
@@ -9,6 +9,7 @@
 include Makefile.stage1
 
 -include $(ML4FILES:.ml4=.ml4.ml.d)
+.SECONDARY: $(ML4FILES:.ml4=.ml4.ml.d)
 
 .PHONY: stage2
 stage2: $(COQDEP)
diff --git a/Makefile.stage3 b/Makefile.stage3
index f258ab2981..1b9d880f00 100644
--- a/Makefile.stage3
+++ b/Makefile.stage3
@@ -9,6 +9,7 @@
 include Makefile.stage2
 
 -include $(VFILES:.v=.v.d)
+.SECONDARY: $(VFILES:.v=.v.d)
 
 .PHONY: stage3
 stage3: world
diff --git a/dev/doc/build-system.dev.txt b/dev/doc/build-system.dev.txt
index 8fb036fc59..c825f088bc 100644
--- a/dev/doc/build-system.dev.txt
+++ b/dev/doc/build-system.dev.txt
@@ -37,9 +37,6 @@ Le Makefile a été séparé en plusieurs fichiers :
 The build needs to be cut in stages because make will not take into
 account one include when making another include.
 
-Because a weird not completely understood situation, there is actually
-a stage0, see the comment in Makefile.stage0.
-
 Parallélisation
 ---------------