New option -glob for coqdep, in order to avoid nasty tricks with sed in Makefile

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

3 files changed, 10 insertions, 23 deletions

diff --git a/Makefile.build b/Makefile.build
index 53acb99bf2..0a336b8744 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -850,24 +850,9 @@ endif
 	$(HIDE)echo "let keep_ocamldep_happy Do_not_compile_me = assert false" > $@ \
 	  || ( RV=$$?; rm -f "$@"; exit $${RV} )
 
-# Another nasty hack. The making of .v.d files is split in two so that
-# make notices if coqdep fails (returns an error exit code). If we
-# just make %.v.d directly from %.v with
-#	$(HIDE)$(COQDEP) -coqlib . -R theories Coq -R contrib Coq $(COQINCLUDES) \
-#  "$<" | sed 's/\(.*\)\.vo[[:space:]]*:/\1.vo \1.glob:/' > "$@"
-# then the exit code of the whole pipe is the exit code of ... sed,
-# that is always 0. And make doesn't notice that coqdep failed and
-# merrily accepts that the .v.d file is just empty.
-# We could also make a complex shell script with ERR trapping and all
-# that, but more complex and fragile than this.
-# make will delete .raw files because they are intermediate.
-%.v.d.raw: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEP)
+%.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEP)
 	$(SHOW)'COQDEP    $<'
-	$(HIDE)$(COQDEP) -slash -coqlib . -R theories Coq -R contrib Coq $(COQINCLUDES) "$<" > "$@" \
-	  || ( RV=$$?; rm -f "$@"; exit $${RV} )
-
-%.v.d: %.v.d.raw
-	$(HIDE)sed 's/\(.*\)\.vo[[:space:]]*:/\1.vo \1.glob:/' < "$<" > "$@" \
+	$(HIDE)$(COQDEP) -glob -slash -coqlib . -R theories Coq -R contrib Coq $(COQINCLUDES) "$<" > "$@" \
 	  || ( RV=$$?; rm -f "$@"; exit $${RV} )
 
 %.c.d: $(D_DEPEND_BEFORE_SRC) %.c $(D_DEPEND_AFTER_SRC) $(GENHFILES)
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index 8e3e0aa45d..9b95bf7cd7 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -138,10 +138,9 @@ let implicit () =
     print "%.html: %.v %.glob\n\t$(COQDOC) -glob-from $*.glob  -html $< -o $@\n\n";
     print "%.g.tex: %.v\n\t$(COQDOC) -latex -g $< -o $@\n\n";
     print "%.g.html: %.v %.glob\n\t$(COQDOC) -glob-from $*.glob -html -g $< -o $@\n\n";
-    print "%.v.d.raw: %.v\n";
-    print "\t$(COQDEP) -slash $(COQLIBS) \"$<\" > \"$@\"\\\n\t  || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n";
-    print "%.v.d: %.v.d.raw\n";
-    print "\t$(HIDE)sed 's/\\(.*\\)\\.vo[[:space:]]*:/\\1.vo \\1.glob:/' < \"$<\" > \"$@\" \\\n\t  || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"
+    print "%.v.d: %.v\n";
+    print "\t$(COQDEP) -glob -slash $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n";
+
   and ml_suffixes =
     if !some_mlfile then 
       [ ".mli"; ".ml"; ".cmo"; ".cmi"; ".cmx" ]
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 35608cd640..2ce73cef2c 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -22,6 +22,7 @@ let option_D = ref false
 let option_w = ref false
 let option_i = ref false
 let option_sort = ref false
+let option_glob = ref false
 let option_slash = ref false
 
 let suffixe = ref ".vo"
@@ -365,11 +366,12 @@ let mL_dependencies () =
 let coq_dependencies () =
   List.iter
     (fun (name,_) ->
-       printf "%s%s: %s.v" name !suffixe name;
+       let glob = if !option_glob then " "^name^".glob" else "" in 
+       printf "%s%s%s: %s.v" name !suffixe glob name;
        traite_fichier_Coq true (name ^ ".v");
        printf "\n";
        if !option_i then begin
-	 printf "%s%s: %s.v" name !suffixe_spec name;
+	 printf "%s%s%s: %s.v" name !suffixe_spec glob name;
 	 traite_fichier_Coq false (name ^ ".v");
 	 printf "\n";
        end;
@@ -527,6 +529,7 @@ let coqdep () =
       | "-w" :: ll -> option_w := true; parse ll
       | "-i" :: ll -> option_i := true; parse ll
       | "-sort" :: ll -> option_sort := true; parse ll
+      | "-glob" :: ll -> option_glob := true; parse ll
       | "-I" :: r :: ll -> add_directory (r, []); parse ll
       | "-I" :: [] -> usage ()
       | "-R" :: r :: ln :: ll -> add_rec_directory r ln; parse ll