Many changes in the Makefile infrastructure + a beginning of ocamlbuild

 * generalize the use of .mllib to build all cma, not only in plugins/
 * the .mllib in plugins/ now mention Bruno's new _mod.ml files
 * lots of .cmo enumerations in Makefile.common are removed, since
   they are now in .mllib
 * the list of .cmo/.cmi can be retreive via a shell script line,
   see for instance rule install-library
 * Tolink.core_objs and Tolink.ide now contains ocaml _modules_, not
   _files_
 * a -I option to coqdep_boot allows to control piority of includes
   (some files with the same names in kernel and checker ...)

 This is quite a lot of changes, you know who to blame / report to
 if something breaks.

 ... and last but not least I've started playing with ocamlbuild.
 The myocamlbuild.ml is far from complete now, but it already allows
 to build coqtop.{opt,byte} here. See comments at the top of
 myocamlbuild.ml, and don't hesitate to contribute, either for completing
 or simplifying it !

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

3 files changed, 48 insertions, 35 deletions

diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml
index 59fe701aa..d259c3be5 100644
--- a/tools/coqdep_boot.ml
+++ b/tools/coqdep_boot.ml
@@ -22,19 +22,24 @@ 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 *)
+   | "-I" :: r :: ll ->
+       (* To solve conflict (e.g. same filename in kernel and checker)
+          we allow to state an explicit order *)
+       add_dir add_known r [];
+       norecdir_list:=r::!norecdir_list;
+       parse ll
   | f :: ll -> treat_file None f; parse ll
   | [] -> ()
 
 let coqdep_boot () =
   if Array.length Sys.argv < 2 then exit 1;
   parse (List.tl (Array.to_list Sys.argv));
-  add_rec_dir add_known "theories" ["Coq"];
-  add_rec_dir add_known "plugins" ["Coq"];
-  List.iter (fun (f,d) -> add_mli_known f d) !mliAccu;
-  List.iter (fun (f,d) -> add_mllib_known f d) !mllibAccu;
-  List.iter (fun (f,_,d) -> add_ml_known f d) !mlAccu;
-  warning_mult ".mli" iter_mli_known;
-  warning_mult ".ml" iter_ml_known;
+  if !option_c then
+    add_rec_dir add_known "." []
+  else begin
+    add_rec_dir add_known "theories" ["Coq"];
+    add_rec_dir add_known "plugins" ["Coq"];
+  end;
   if !option_c then mL_dependencies ();
   coq_dependencies ()
 
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 67a200921..7ac57a4f5 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -27,6 +27,8 @@ let option_noglob = ref false
 let option_slash = ref false
 let option_natdynlk = ref true
 
+let norecdir_list = ref ([]:string list)
+
 let suffixe = ref ".vo"
 
 type dir = string option
@@ -98,7 +100,7 @@ let safe_hash_add clq q (k,v) =
 
 let mkknown () =
   let h = (Hashtbl.create 19 : (string, dir) Hashtbl.t) in
-  let add x s = Hashtbl.add h x s
+  let add x s = if Hashtbl.mem h x then () else Hashtbl.add h x s
   and iter f = Hashtbl.iter f h
   and search x =
     try Some (Hashtbl.find h (String.uncapitalize x))
@@ -302,27 +304,32 @@ let mL_dependencies () =
     (fun (name,ext,dirname) ->
        let fullname = file_name name dirname in
        let (dep,dep_opt) = traite_fichier_ML fullname ext in
-       let intf =
-	 if List.mem (name,dirname) !mliAccu then " "^fullname^".cmi" else ""
+       let intf = match search_mli_known name with
+	 | None -> ""
+	 | Some mldir -> " "^(file_name name mldir)^".cmi"
        in
-       printf "%s.cmo: %s%s%s%s\n" fullname fullname ext intf dep;
-       printf "%s.cmx: %s%s%s%s\n" fullname fullname ext intf dep_opt;
-       flush stdout)
+       if dep<>"" || intf<>"" then begin
+	 printf "%s.cmo:%s%s\n" fullname dep intf;
+	 printf "%s.cmx:%s%s\n" fullname dep_opt intf;
+	 flush stdout;
+       end)
     (List.rev !mlAccu);
   List.iter
     (fun (name,dirname) ->
        let fullname = file_name name dirname in
        let (dep,_) = traite_fichier_ML fullname ".mli" in
-       printf "%s.cmi: %s.mli%s\n" fullname fullname dep;
+       if dep<>"" then printf "%s.cmi:%s\n" fullname dep;
        flush stdout)
     (List.rev !mliAccu);
   List.iter
     (fun (name,dirname) ->
        let fullname = file_name name dirname in
        let (dep,dep_opt) = traite_fichier_mllib fullname ".mllib" in
-       printf "%s.cma:%s\n" fullname dep;
-       printf "%s.cmxa %s.cmxs:%s\n" fullname fullname dep_opt;
-       flush stdout)
+       if dep<>"" then begin
+	 printf "%s.cma:%s\n" fullname dep;
+	 printf "%s.cmxa %s.cmxs:%s\n" fullname fullname dep_opt;
+	 flush stdout
+       end)
     (List.rev !mllibAccu)
 
 let coq_dependencies () =
@@ -382,9 +389,13 @@ let rec add_directory recur add_file phys_dir log_dir =
       let f = readdir dirh in
       (* we avoid . .. and all hidden files and subdirs (e.g. .svn, _darcs) *)
       if f.[0] <> '.' && f.[0] <> '_' then
-        let phys_f = phys_dir//f in
+        let phys_f = if phys_dir = "." then f else phys_dir//f in
 	match try (stat phys_f).st_kind with _ -> S_BLK with
-	  | S_DIR when recur -> add_directory recur add_file phys_f (log_dir@[f])
+	  | S_DIR when recur ->
+	      if List.mem phys_f !norecdir_list then ()
+	      else
+		let log_dir' = if log_dir = [] then ["Coq"] else log_dir@[f] in
+		add_directory recur add_file phys_f log_dir'
 	  | S_REG -> add_file phys_dir log_dir f
 	  | _ -> ()
     done
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
index 6d6a804da..3c7d09e1f 100755
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -34,15 +34,18 @@
   let mllist = ref ([] : string list)
 
   let field_name s = String.sub s 1 (String.length s - 1)
+
 }
 
 let space = [' ' '\t' '\n' '\r']
 let lowercase = ['a'-'z' '\223'-'\246' '\248'-'\255']
 let uppercase = ['A'-'Z' '\192'-'\214' '\216'-'\222']
-let identchar = 
+let identchar =
   ['A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9']
 let coq_ident = ['a'-'z' '_' '0'-'9' 'A'-'Z']+
 let coq_field = '.'['a'-'z' '_' '0'-'9' 'A'-'Z']+
+let caml_up_ident = uppercase identchar*
+let caml_low_ident = lowercase identchar*
 let dot = '.' ( space+ | eof)
 
 rule coq_action = parse
@@ -66,13 +69,14 @@ rule coq_action = parse
       { coq_action lexbuf }
 
 and caml_action = parse
-  | [' ' '\010' '\013' '\009' '\012'] +
-      { caml_action lexbuf }
-  | "open" [' ' '\010' '\013' '\009' '\012']*
-        { caml_opened_file lexbuf }
-  | lowercase identchar*
+  | space +
       { caml_action lexbuf }
-  | uppercase identchar*
+  | "open" space* (caml_up_ident as id)
+        { Use_module (String.uncapitalize id) }
+  | "module" space+ caml_up_ident
+        { caml_action lexbuf }
+  | caml_low_ident { caml_action lexbuf }
+  | caml_up_ident
       { ml_module_name := Lexing.lexeme lexbuf;
         qual_id lexbuf }
   | ['0'-'9']+
@@ -213,18 +217,11 @@ and modules = parse
   | _   { (Declare (List.rev !mllist)) }   
 
 and qual_id = parse
-  | '.' [^ '.' '(' '['] { Use_module (String.uncapitalize !ml_module_name) }
+  | '.' [^ '.' '(' '['] {
+      Use_module (String.uncapitalize !ml_module_name) }
   | eof { raise Fin_fichier }
   | _ { caml_action lexbuf }
 
-and caml_opened_file = parse
-  | uppercase identchar*
-      { let lex = (Lexing.lexeme lexbuf) in 
-        let str = String.sub lex 0 (String.length lex) in
-        (Use_module (String.uncapitalize str)) }
-  | eof {raise Fin_fichier }
-  | _ { caml_action lexbuf }
-
 and mllib_list = parse
   | coq_ident { let s = String.uncapitalize (Lexing.lexeme lexbuf)
 		in s :: mllib_list lexbuf }