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

3 files changed, 28 insertions, 3 deletions

diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml
index b7f6ec250..2798e4af6 100644
--- a/tools/coqdep_boot.ml
+++ b/tools/coqdep_boot.ml
@@ -22,6 +22,8 @@ let rec parse = function
   | "-natdynlink" :: "no" :: ll -> option_natdynlk := false; parse ll
   | "-c" :: ll -> option_c := true; parse ll
   | "-boot" :: ll -> parse ll (* We're already in boot mode by default *)
+  | "-mldep" :: ocamldep :: ll ->
+      option_mldep := Some ocamldep; option_c := true; parse ll
   | "-I" :: r :: ll ->
        (* To solve conflict (e.g. same filename in kernel and checker)
           we allow to state an explicit order *)
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 8756d864d..95c794ca7 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -26,6 +26,7 @@ let option_c = ref false
 let option_noglob = ref false
 let option_slash = ref false
 let option_natdynlk = ref true
+let option_mldep = ref None
 
 let norecdir_list = ref ([]:string list)
 
@@ -176,7 +177,22 @@ let depend_ML str =
 	(" "^mlifile^".cmi"," "^mlifile^".cmi")
     | None, None -> "", ""
 
-let traite_fichier_ML md ext =
+let soustraite_fichier_ML dep md ext =
+  try
+    let chan = open_process_in (dep^" -modules "^md^ext) in
+    let list = ocamldep_parse (Lexing.from_channel chan) in
+    let a_faire = ref "" in
+    let a_faire_opt = ref "" in
+    List.iter
+      (fun str ->
+	 let byte,opt = depend_ML str in
+	 a_faire := !a_faire ^ byte;
+	 a_faire_opt := !a_faire_opt ^ opt)
+      (List.rev list);
+    (!a_faire, !a_faire_opt)
+  with Sys_error _ -> ("","")
+
+let autotraite_fichier_ML md ext =
   try
     let chan = open_in (md ^ ext) in
     let buf = Lexing.from_channel chan in
@@ -201,6 +217,11 @@ let traite_fichier_ML md ext =
     (!a_faire, !a_faire_opt)
   with Sys_error _ -> ("","")
 
+let traite_fichier_ML md ext =
+  match !option_mldep with
+    | Some dep -> soustraite_fichier_ML dep md ext
+    | None -> autotraite_fichier_ML md ext
+
 let traite_fichier_mllib md ext =
   try
     let chan = open_in (md ^ ext) in
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
index 89eeed54a..74c556a7d 100755
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -225,8 +225,10 @@ and qual_id = parse
 and mllib_list = parse
   | coq_ident { let s = String.uncapitalize (Lexing.lexeme lexbuf)
 		in s :: mllib_list lexbuf }
+  | "*predef*" { mllib_list lexbuf }
   | space+ { mllib_list lexbuf }
   | eof { [] }
 
-
-
+and ocamldep_parse = parse
+  | [^ ':' ]* ':' { mllib_list lexbuf }
+  | _ { [] }