Améliorations utiles pour les Makefile répartis sur plusieurs répertoires

coqdep :
- fonction de "canonisation" du nom des cibles plus performante (elle
  traverse notamment les "..")

coq_makefile : 
- ajout automatique de "-I ." dans COQLIBS seulement si pas déjà déclaré
  (utile pour éviter les cibles en double dans coqdep en présence de -R)
- explicitation de "-byte" dans la cible "byte:" (son absence semble
  remonter à l'époque où l'exécution en byte était le défaut)



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

2 files changed, 43 insertions, 12 deletions

diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index a169414310..256515c515 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -81,7 +81,7 @@ coq_makefile [subdirectory] .... [file.v] ... [file.ml] ... [-custom
 
 let standard sds sps =
   print "byte:\n";
-  print "\t$(MAKE) all \"OPT=\"\n\n";
+  print "\t$(MAKE) all \"OPT=-byte\"\n\n";
   print "opt:\n";
   if !opt = "" then print "\t@echo \"WARNING: opt is disabled\"\n";
   print "\t$(MAKE) all \"OPT="; print !opt; print "\"\n\n";
@@ -209,6 +209,23 @@ let variables l =
   var_aux l;
   print "\n"
 
+let absolute_dir dir =
+  let current = Sys.getcwd () in
+  Sys.chdir dir;
+  let dir' = Sys.getcwd () in
+  Sys.chdir current;
+  dir'
+
+let is_prefix dir1 dir2 =
+  let l1 = String.length dir1 in
+  let l2 = String.length dir2 in
+  dir1 = dir2 or (l1 < l2 & String.sub dir2 0 l1 = dir1 & dir2.[l1] = '/')
+
+let is_included dir = function
+  | RInclude (dir',_) -> is_prefix (absolute_dir dir') (absolute_dir dir)
+  | Include dir' -> absolute_dir dir = absolute_dir dir'
+  | _ -> false
+
 let include_dirs l =
   let include_aux' includeR =
    let rec include_aux = function
@@ -221,8 +238,9 @@ let include_dirs l =
    in
     include_aux
   in
+  let l' = if List.exists (is_included ".") l then l else Include "." :: l in
   let i_ocaml = "-I ." :: (include_aux' false l) in
-  let i_coq   = "-I ." :: (include_aux' true  l) in
+  let i_coq   = include_aux' true l' in
   section "Libraries definition.";
   print "OCAMLLIBS="; print_list "\\\n  " i_ocaml; print "\n";
   print "COQLIBS=";   print_list "\\\n  " i_coq; print "\n\n"
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 423035fabb..9b9cde31ff 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -42,7 +42,7 @@ let file_concat l =
 (* Files specified on the command line *)
 let mlAccu  = ref ([] : (string * string * dir) list) 
 and mliAccu = ref ([] : (string * string * dir) list) 
-and vAccu   = ref ([] : string list)
+and vAccu   = ref ([] : (string * string) list)
 
 (* Queue operations *)
 let addQueue q v = q := v :: !q
@@ -97,6 +97,16 @@ let safe_assoc verbose file k =
   List.assoc k !vKnown
 
 
+let absolute_dir dir =
+  let current = Sys.getcwd () in
+  Sys.chdir dir;
+  let dir' = Sys.getcwd () in
+  Sys.chdir current;
+  dir'
+
+let absolute_file_name basename odir =
+  let dir = match odir with Some dir -> dir | None -> "." in
+  absolute_dir dir / basename
      
 let file_name = function
   | (s,None)     -> file_concat s 
@@ -152,9 +162,11 @@ let cut_prefix p s =
   let ls = String.length s in
   if ls >= lp && String.sub s 0 lp = p then String.sub s lp (ls - lp) else s
 
-let canonize f = match Sys.os_type with
-  | "Win32" when not !option_slash -> cut_prefix ".\\" f
-  | _ -> cut_prefix "./" f
+let canonize f =
+  let f' = absolute_dir (Filename.dirname f) / Filename.basename f in
+  match List.filter (fun (_,full) -> f' = full) !vAccu with
+    | (f,_) :: _ -> f
+    | _ -> f
 
 let sort () = 
   let seen = Hashtbl.create 97 in
@@ -181,7 +193,7 @@ let sort () =
 	printf "%s%s " file !suffixe
     end
   in
-  List.iter loop !vAccu
+  List.iter (fun (name,_) -> loop name) !vAccu
 
 let traite_fichier_Coq verbose f = 
   try 
@@ -352,7 +364,7 @@ let mL_dependencies () =
 
 let coq_dependencies () =
   List.iter
-    (fun name ->
+    (fun (name,_) ->
        printf "%s%s: %s.v" name !suffixe name;
        traite_fichier_Coq true (name ^ ".v");
        printf "\n";
@@ -366,7 +378,7 @@ let coq_dependencies () =
 
 let declare_dependencies () =
   List.iter
-    (fun name ->
+    (fun (name,_) ->
        traite_Declare (name^".v");      
        flush stdout)
     (List.rev !vAccu)
@@ -410,7 +422,7 @@ let all_subdirs root_dir log_dir =
 
 let usage () =
   eprintf
-  "[ usage: coqdep [-w] [-I dir] [-coqlib dir] [-c] [-i] [-D] <filename>+ ]\n";
+  "[ usage: coqdep [-w] [-I dir] [-R dir coqdir] [-coqlib dir] [-c] [-i] [-D] <filename>+ ]\n";
   flush stderr;
   exit 1
 
@@ -471,7 +483,8 @@ let coqdep () =
 	    addQueue mliAccu (basename,".mli",dirname)
 	  else if Filename.check_suffix name ".v" then
 	    let basename = Filename.chop_suffix name ".v" in
-	    addQueue vAccu (file_name ([basename], dirname))
+	    let name = file_name ([basename],dirname) in
+	    addQueue vAccu (name, absolute_file_name basename dirname)
       | _ -> ()
   in 
   let add_known phys_dir log_dir f =
@@ -526,7 +539,7 @@ let coqdep () =
       | f :: ll -> treat None f; parse ll
       | [] -> ()
   in
-  add_directory (".", []);
+(*  add_directory (".", []);*)
   parse (List.tl (Array.to_list Sys.argv));
   List.iter
     (fun (s,_) -> add_coqlib_directory s)