utilisation de printf (simplif)

option -sort pour trier les .v selon les dépendances


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

1 files changed, 73 insertions, 67 deletions

diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 4880423468..48c6e282e6 100755
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -8,6 +8,7 @@
 
 (* $Id$ *)
 
+open Printf
 open Coqdep_lexer
 open Unix
 
@@ -15,19 +16,17 @@ let stderr = Pervasives.stderr
 let stdout = Pervasives.stdout
 
 let option_c = ref false
-
 let option_D = ref false
-
 let option_w = ref false
-
 let option_i = ref false
+let option_sort = ref false
 
 let suffixe = ref ".vo"
 let suffixe_spec = ref ".vi"
 
 let traite_fichier_ML md ext =
   try 
-    let chan = open_in (md^ext) in 
+    let chan = open_in (md ^ ext) in 
     let buf = Lexing.from_channel chan in 
     let deja_vu = ref [md] in
     let a_faire = ref "" in
@@ -69,9 +68,35 @@ let traite_fichier_ML md ext =
     (!a_faire, !a_faire_opt)
   with Sys_error _ -> ("","")
 
+let sort () = 
+  let seen = Hashtbl.create 97 in
+  let rec loop file =
+    let file = file_name file ^ ".v" in
+    if not (Hashtbl.mem seen file) then begin
+      Hashtbl.add seen file ();
+      let cin = open_in file in
+      let lb = Lexing.from_channel cin in
+      try
+	while true do
+	  match coq_action lb with
+	    | Require (_, s) ->
+		(try loop (s, List.assoc s !vAccu) with Not_found -> ())
+	    | RequireString (_, s) -> 
+		let s = Filename.basename s in
+		(try loop (s, List.assoc s !vAccu) with Not_found -> ())
+	    | _ -> 
+		()
+	done
+      with Fin_fichier ->
+	close_in cin;
+	printf "%s " file
+    end
+  in
+  List.iter loop !vAccu
+
 let warning_notfound f s =
-  output_string stderr ("*** Warning : in file " ^ f ^ ", the file ");
-  output_string stderr ( s ^ ".v is required and has not been found !\n");
+  eprintf "*** Warning : in file %s, the file " f;
+  eprintf "%s.v is required and has not been found !\n" s;
   flush stderr
 
 let traite_fichier_Coq f = 
@@ -89,9 +114,9 @@ let traite_fichier_Coq f =
 	        deja_vu_v := str :: !deja_vu_v;
                 try
                   let vdir = List.assoc str !vKnown in
-                  print_string " ";
-                  print_string (file_name (str,vdir));
-                  print_string (if spec then !suffixe_spec else !suffixe)
+                  printf " %s%s" 
+		    (file_name (str,vdir))
+                    (if spec then !suffixe_spec else !suffixe)
                 with Not_found -> 
                   begin 
 		    try let _ = List.assoc str !coqlibKnown in ()
@@ -103,9 +128,9 @@ let traite_fichier_Coq f =
 	        deja_vu_v := str :: !deja_vu_v;
                 try
                   let vdir = List.assoc str !vKnown in
-                  print_string " ";
-                  print_string (file_name (str,vdir));
-                  print_string (if spec then !suffixe_spec else !suffixe)
+                  printf " %s%s"
+                    (file_name (str,vdir))
+                    (if spec then !suffixe_spec else !suffixe)
                 with Not_found -> 
                   begin try  let _ = List.assoc s !coqlibKnown in ()
                   with Not_found -> warning_notfound f s end
@@ -117,9 +142,7 @@ let traite_fichier_Coq f =
 		     deja_vu_ml := str :: !deja_vu_ml;
                	     try
               	       let mldir = List.assoc str !mlKnown in
-              	       print_string " ";
-                       print_string (file_name (str,mldir));
-              	       print_string ".cmo"
+              	       printf " %s.cmo" (file_name (str,mldir))
               	     with Not_found -> () 
 		   end)
 		sl
@@ -140,8 +163,8 @@ let mL_dep_list b f =
 	while true do
 	  let (Use_module str) = caml_action buf in
 	  if str = b then begin
-	    output_string stderr ("*** Warning : in file "^f^" the");
-	    output_string stderr (" notation "^b^"__ is useless !\n");
+	    eprintf "*** Warning : in file %s the" f;
+	    eprintf " notation %s__ is useless !\n" b;
 	    flush stderr
 	  end else if List.mem str !deja_vu then 
 	    ()
@@ -157,35 +180,28 @@ let mL_dep_list b f =
     with Sys_error _ -> []
 
 let affiche_Declare f dcl = 
-  print_newline ();
-  print_string ("*** In file "^f^" : ");
-  print_newline ();
-  print_string "Declare ML Module";
-  List.iter (fun str -> print_string " ";
-	       print_char '"'; print_string str;
-	       print_char '"') dcl;
-  print_string ".";
-  print_newline();
+  printf "\n*** In file %s: \n" f;
+  printf "Declare ML Module";
+  List.iter (fun str -> printf " \"%s\"" str) dcl;
+  printf ".\n";
   flush stdout
 
 let warning_Declare f dcl =
-  output_string stderr ("*** Warning : in file "^f^", the ML modules");
-  output_string stderr " declaration should be\n";
-  output_string stderr "*** Declare ML Module";
-  List.iter (fun str -> output_string stderr " ";
-	       output_char stderr '"'; output_string stderr str;
-	       output_char stderr '"') dcl;
-  output_string stderr ".\n";
+  eprintf "*** Warning : in file %s, the ML modules" f;
+  eprintf " declaration should be\n";
+  eprintf "*** Declare ML Module";
+  List.iter (fun str -> eprintf " \"%s\"" str) dcl;
+  eprintf ".\n";
   flush stderr
 
 let traite_Declare f = 
   let decl_list = ref ([] : string list) in
   let rec treat = function
-    | s::ll -> 
+    | s :: ll -> 
 	if (List.mem_assoc s !mlKnown) & not (List.mem s !decl_list) then begin
        	  let mldir = List.assoc s !mlKnown in
 	  let fullname = file_name (s,mldir) in
-	  let depl = mL_dep_list s (fullname^".ml") in
+	  let depl = mL_dep_list s (fullname ^ ".ml") in
 	  treat depl;
 	  decl_list := s :: !decl_list
 	end;
@@ -215,7 +231,7 @@ let traite_Declare f =
 
 let file_mem (f,_,d) =
   let rec loop = function
-    | (f1,_,d1) :: l -> if f1 = f && d1 = d then true else loop l
+    | (f1,_,d1) :: l -> (f1 = f && d1 = d) || (loop l)
     | _ -> false
   in 
   loop
@@ -225,30 +241,20 @@ let mL_dependencies () =
     (fun ((name,ext,dirname) as pairname) ->
        let fullname = file_name (name,dirname) in
        let (dep,dep_opt) = traite_fichier_ML fullname ext in
-       print_string fullname; print_string ".cmo: "; 
-       print_string fullname; print_string ext;
-       if file_mem pairname !mliAccu then begin
-	 print_string " "; print_string fullname; print_string ".cmi"
-       end;
-       print_string dep;
-       print_newline ();
-       print_string fullname; print_string ".cmx: "; 
-       print_string fullname; print_string ext;
-       if file_mem pairname !mliAccu then begin
-	 print_string " "; print_string fullname; print_string ".cmi"
-       end;
-       print_string dep_opt;
-       print_newline ();
+       printf "%s.cmo: %s%s" fullname fullname ext;
+       if file_mem pairname !mliAccu then printf " %s.cmi" fullname;
+       printf "%s\n" dep;
+       printf "%s.cmx: %s%s" fullname fullname ext;
+       if file_mem pairname !mliAccu then printf " %s.cmi" fullname;
+       printf "%s\n" dep_opt;
        flush stdout)
     !mlAccu;
   List.iter
     (fun ((name,ext,dirname) as pairname) ->
        let fullname = file_name (name,dirname) in
        let (dep,_) = traite_fichier_ML fullname ext in
-       print_string fullname; print_string ".cmi: "; 
-       print_string fullname;print_string ext;
-       print_string dep;
-       print_newline ();
+       printf "%s.cmi: %s%s" fullname fullname ext;
+       printf "%s\n" dep;
        flush stdout)
     !mliAccu
 
@@ -256,13 +262,13 @@ let coq_dependencies () =
   List.iter
     (fun ((name,dirname) as pairname) ->
        let fullname = file_name pairname in
-       Printf.printf "%s%s: %s.v" fullname !suffixe fullname;
-       traite_fichier_Coq (fullname^".v");
-       print_newline ();
+       printf "%s%s: %s.v" fullname !suffixe fullname;
+       traite_fichier_Coq (fullname ^ ".v");
+       printf "\n";
        if !option_i then begin
-	 Printf.printf "%s%s: %s.v" fullname !suffixe_spec fullname;
-	 traite_fichier_Coq (fullname^".v");
-	 print_newline ();
+	 printf "%s%s: %s.v" fullname !suffixe_spec fullname;
+	 traite_fichier_Coq (fullname ^ ".v");
+	 printf "\n";
        end;
        flush stdout)
     !vAccu
@@ -283,9 +289,7 @@ let rec warning_mult suf l =
 	 let d' = Hashtbl.find tab f in
 	 if (Filename.dirname (file_name (f,d)))
       	   <> (Filename.dirname (file_name (f,d'))) then begin
-	     output_string stderr "*** Warning : the file ";
-	     output_string stderr (f ^ suf);
-	     output_string stderr " is defined twice !\n";
+	     eprintf "*** Warning : the file %s is defined twice!\n" (f ^ suf);
 	     flush stderr
 	   end
        with Not_found -> () end;
@@ -316,9 +320,9 @@ let all_subdirs dir =
   traverse dir; List.rev !l
 
 let usage () =
-  print_string 
+  eprintf
   "[ usage: coqdep [-w] [-I dir] [-coqlib dir] [-c] [-i] [-D] <filename>+ ]\n";
-  flush stdout;
+  flush stderr;
   exit 1
 
 let add_coqlib_known dir_name f =
@@ -414,6 +418,7 @@ let coqdep () =
       | "-D" :: ll -> option_D := true; parse ll
       | "-w" :: ll -> option_w := true; parse ll
       | "-i" :: ll -> option_i := true; parse ll
+      | "-sort" :: ll -> option_sort := true; parse ll
       | "-I" :: r :: ll -> add_directory r; parse ll
       | "-I" :: [] -> usage ()
       | "-R" :: r :: _ :: ll -> add_rec_directory r; parse ll
@@ -442,9 +447,10 @@ let coqdep () =
     warning_mult ".mli" !mliKnown;
     warning_mult ".ml" !mlKnown;
     warning_mult ".v" !vKnown;
-    if !option_c & not !option_D then mL_dependencies ();
+    if !option_sort then begin sort (); exit 0 end;
+    if !option_c && not !option_D then mL_dependencies ();
     if not !option_D then coq_dependencies ();
-    if !option_w or !option_D then declare_dependencies ()
+    if !option_w || !option_D then declare_dependencies ()
       
 let _ = Printexc.catch coqdep ()