Simplification de la construction du .depend:

 - make ou make world entraînent la construction de .depend et .depend.coq;
 - suppression des cibles .depend et .depend.coq (au profit de depend et dependcoq)
 - suppression de la dépendance de depend avec les .ml (inutile)



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

2 files changed, 24 insertions, 34 deletions

diff --git a/.depend.coq b/.depend.coq
index 887cd4f73..72416e2c7 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -363,7 +363,7 @@ theories/Ints/num/GenDiv.vo: theories/Ints/num/GenDiv.v theories/ZArith/ZArith.v
 theories/Ints/num/GenSqrt.vo: theories/Ints/num/GenSqrt.v theories/ZArith/ZArith.vo theories/Ints/Z/ZAux.vo theories/Ints/Z/ZDivModAux.vo theories/Ints/Z/ZPowerAux.vo theories/Ints/Basic_type.vo theories/Ints/num/GenBase.vo
 theories/Ints/num/GenLift.vo: theories/Ints/num/GenLift.v theories/ZArith/ZArith.vo theories/Ints/Z/ZAux.vo theories/Ints/Z/ZPowerAux.vo theories/Ints/Z/ZDivModAux.vo theories/Ints/Z/Zmod.vo theories/Ints/Basic_type.vo theories/Ints/num/GenBase.vo
 theories/Ints/num/Zn2Z.vo: theories/Ints/num/Zn2Z.v theories/ZArith/ZArith.vo theories/Ints/Z/ZAux.vo theories/Ints/Z/ZDivModAux.vo theories/Ints/Basic_type.vo theories/Ints/num/GenBase.vo theories/Ints/num/GenAdd.vo theories/Ints/num/GenSub.vo theories/Ints/num/GenMul.vo theories/Ints/num/GenSqrt.vo theories/Ints/num/GenLift.vo theories/Ints/num/GenDivn1.vo theories/Ints/num/GenDiv.vo theories/Ints/num/ZnZ.vo
-theories/Ints/num/Nbasic.vo: theories/Ints/num/Nbasic.v theories/ZArith/ZArith.vo theories/Ints/Basic_type.vo
+theories/Ints/num/Nbasic.vo: theories/Ints/num/Nbasic.v theories/ZArith/ZArith.vo theories/Ints/Z/ZAux.vo theories/Ints/Z/ZDivModAux.vo theories/Ints/Basic_type.vo
 theories/Ints/num/NMake.vo: theories/Ints/num/NMake.v theories/ZArith/ZArith.vo theories/Ints/Basic_type.vo theories/Ints/num/ZnZ.vo theories/Ints/num/Zn2Z.vo theories/Ints/num/Nbasic.vo theories/Ints/num/GenMul.vo theories/Ints/num/GenDivn1.vo
 theories/Ints/BigN.vo: theories/Ints/BigN.v theories/Ints/Int31.vo theories/Ints/num/NMake.vo theories/Ints/num/ZnZ.vo
 theories/Ints/num/ZMake.vo: theories/Ints/num/ZMake.v theories/ZArith/ZArith.vo
diff --git a/Makefile b/Makefile
index 98d88f6b1..92f453590 100644
--- a/Makefile
+++ b/Makefile
@@ -42,7 +42,7 @@ help:
 
 
 # build and install the three subsystems: coq, coqide, pcoq
-world: .depend .depend.coq
+world: depend dependcoq
 	$(MAKE) worldnodep
 
 worldnodep: revision coq coqide pcoq
@@ -251,7 +251,7 @@ NEWRINGCMO=\
 
 DPCMO=contrib/dp/dp_why.cmo contrib/dp/dp_zenon.cmo \
       contrib/dp/dp.cmo contrib/dp/g_dp.cmo
-beforedepend:: contrib/dp/dp_zenon.ml
+BEFOREDEPEND+= contrib/dp/dp_zenon.ml
 
 FIELDCMO=\
   contrib/field/field.cmo 
@@ -404,9 +404,7 @@ kernel/copcodes.ml: kernel/byterun/coq_instruct.h
 	kernel/byterun/coq_instruct.h | \
 	awk -f kernel/make-opcodes > kernel/copcodes.ml
 
-bytecompfile : kernel/byterun/coq_jumptbl.h kernel/copcodes.ml
-
-beforedepend:: bytecompfile
+BEFOREDEPEND+= kernel/byterun/coq_jumptbl.h kernel/copcodes.ml
 
 clean ::
 	rm -f kernel/byterun/coq_jumptbl.h kernel/copcodes.ml
@@ -478,7 +476,7 @@ scripts/tolink.ml: Makefile
 	$(HIDE)echo "let core_objs = \""$(OBJSCMO)"\"" >> $@
 	$(HIDE)echo "let ide = \""$(COQIDECMO)"\"" >> $@
 
-beforedepend:: scripts/tolink.ml
+BEFOREDEPEND+= scripts/tolink.ml
 
 # coqc
 
@@ -642,9 +640,9 @@ COQIDECMO=ide/utils/okey.cmo ide/utils/config_file.cmo \
 
 COQIDECMX=$(COQIDECMO:.cmo=.cmx)
 COQIDEFLAGS=-thread -I +lablgtk2
-beforedepend:: ide/config_lexer.ml ide/find_phrase.ml ide/highlight.ml
-beforedepend:: ide/config_parser.mli ide/config_parser.ml
-beforedepend:: ide/utf8_convert.ml
+BEFOREDEPEND+= ide/config_lexer.ml ide/find_phrase.ml ide/highlight.ml
+BEFOREDEPEND+= ide/config_parser.mli ide/config_parser.ml
+BEFOREDEPEND+= ide/utf8_convert.ml
 
 COQIDEVO=ide/utf8.vo
 
@@ -1225,7 +1223,7 @@ $(COQDEP): $(COQDEPCMO)
 	$(SHOW)'OCAMLC -o $@'
 	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ unix.cma $(COQDEPCMO) $(OSDEPLIBS)
 
-beforedepend:: tools/coqdep_lexer.ml $(COQDEP)
+BEFOREDEPEND+= tools/coqdep_lexer.ml $(COQDEP)
 
 GALLINACMO=tools/gallina_lexer.cmo tools/gallina.cmo
 
@@ -1233,7 +1231,7 @@ $(GALLINA): $(GALLINACMO)
 	$(SHOW)'OCAMLC -o $@'
 	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ $(GALLINACMO)
 
-beforedepend:: tools/gallina_lexer.ml
+BEFOREDEPEND+= tools/gallina_lexer.ml
 
 $(COQMAKEFILE): tools/coq_makefile.cmo
 	$(SHOW)'OCAMLC -o $@'
@@ -1243,13 +1241,13 @@ $(COQTEX): tools/coq-tex.cmo
 	$(SHOW)'OCAMLC -o $@'
 	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma tools/coq-tex.cmo
 
-beforedepend:: tools/coqwc.ml
+BEFOREDEPEND+= tools/coqwc.ml
 
 $(COQWC): tools/coqwc.cmo
 	$(SHOW)'OCAMLC -o $@'
 	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ tools/coqwc.cmo
 
-beforedepend:: tools/coqdoc/pretty.ml tools/coqdoc/index.ml
+BEFOREDEPEND+= tools/coqdoc/pretty.ml tools/coqdoc/index.ml
 
 COQDOCCMO=$(CONFIG) tools/coqdoc/cdglobals.cmo tools/coqdoc/alpha.cmo \
 	tools/coqdoc/index.cmo tools/coqdoc/output.cmo \
@@ -1552,9 +1550,9 @@ ML4FILES +=parsing/g_minicoq.ml4 \
 	   parsing/g_decl_mode.ml4
 
 
-# beforedepend:: $(GRAMMARCMO)
+# BEFOREDEPEND+= $(GRAMMARCMO)
 
-# beforedepend:: parsing/pcoq.ml parsing/extend.ml
+# BEFOREDEPEND+= parsing/pcoq.ml parsing/extend.ml
 
 # File using pa_ifdef and only necessary for parsing ml files
 
@@ -1716,6 +1714,9 @@ archclean::
 	$(SHOW)'OCAMLC4   $<'
 	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl" -c -impl $<
 
+%.ml: %.ml4
+	$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo pr_o.cmo `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $@ || rm -f $@
+
 #.v.vo:
 #	$(BOOTCOQTOP) -compile $*
 
@@ -1777,14 +1778,11 @@ cleanconfig::
 # Dependencies
 ###########################################################################
 
-.PHONY: alldepend beforedepend dependcoq dependp4 ml4filesml
+.PHONY: alldepend dependcoq scratchdepend
 
 alldepend: depend dependcoq 
 
-dependcoq: beforedepend
-	$(MAKE) MAKEDEPEND=1 .depend.coq
-
-.depend.coq:
+dependcoq:
 	$(COQDEP) -coqlib . -R theories Coq -R contrib Coq $(COQINCLUDES) \
 	 $(ALLFSETS:.vo=.v) $(ALLREALS:.vo=.v) $(ALLVO:.vo=.v) > .depend.coq
 
@@ -1806,24 +1804,17 @@ scratchdepend: dependp4
 ML4FILESML = $(ML4FILES:.ml4=.ml)
 
 # Expresses dependencies of the .ml4 files w.r.t their grammars
-\.depend.camlp4: $(ML4FILES)
-	$(MAKE) dependp4
 
-dependp4:
+.PHONY: dependp4
+dependp4: $(ML4FILES)
 	rm -f .depend.camlp4
 	for f in $(ML4FILES); do \
 	  printf "%s" `dirname $$f`/`basename $$f .ml4`".ml: " >> .depend.camlp4; \
 	  echo `$(CAMLP4DEPS) $$f` >> .depend.camlp4; \
 	done
 
-# Produce the .ml files using Makefile.dep
-ml4filesml: .depend.camlp4
-	$(MAKE) -f Makefile.dep $(ML4FILESML)
-
-\.depend: */*.mli */*/*.mli */*.ml */*/*.ml $(ML4FILES) kernel/byterun/*.c
-	$(MAKE) MAKEDEPEND=1 depend
-
-depend: beforedepend dependp4 ml4filesml
+.PHONY: depend
+depend: $(BEFOREDEPEND) dependp4 $(ML4FILESML)
 # 1. We express dependencies of the .ml files w.r.t their grammars
 # 2. Then we are able to produce the .ml files using Makefile.dep
 # 3. We compute the dependencies inside the .ml files using ocamldep
@@ -1855,10 +1846,9 @@ devel:
 	$(MAKE) -f dev/Makefile.devel setup-devel
 	$(MAKE) $(DEBUGPRINTERS)
 
-ifndef MAKEDEPEND
 -include .depend
 -include .depend.coq
-endif
+-include .depend.camlp4
 
 clean::
 	find . -name "\.#*" -exec rm -f {} \;