Merge PR coq#7437: [coqdep] Minor cleanups.

lib/coqProject_file.ml4

@@ -8,6 +8,14 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+(* This needs to go trou feedback as it is invoked from IDEs, but
+   ideally we would like to make this independent so it can be
+   bootstrapped. *)
+
+(* Note the problem with the error invokation below calling exit... *)
+(* let error msg = Feedback.msg_error msg *)
+let warning msg = Feedback.msg_warning Pp.(str msg)
+
 type arg_source = CmdLine | ProjectFile
 
 type 'a sourced = { thing : 'a; source : arg_source }
@@ -122,7 +130,7 @@ let process_cmd_line orig_dir proj args =
   let sourced x = { thing = x; source = if !parsing_project_file then ProjectFile else CmdLine } in
   let orig_dir = (* avoids turning foo.v in ./foo.v *)
     if orig_dir = "." then "" else orig_dir in
-  let error s = Format.eprintf "@[%a]@@\n%!" Pp.pp_with Pp.(str (s^".")); exit 1 in
+  let error s = (Format.eprintf "Error: @[%s@].@\n%!" s; exit 1) in
   let mk_path d =
     let p = CUnix.correct_path d orig_dir in
     { path = CUnix.remove_path_dot (post_canonize p);
@@ -140,7 +148,7 @@ let process_cmd_line orig_dir proj args =
   | ("-full"|"-opt") :: r -> aux { proj with use_ocamlopt =  true } r
   | "-install" :: d :: r ->
     if proj.install_kind <> None then
-      Feedback.msg_warning (Pp.str "-install set more than once.");
+      (warning "-install set more than once.@\n%!");
     let install = match d with
       | "user" -> UserInstall
       | "none" -> NoInstall
@@ -167,8 +175,7 @@ let process_cmd_line orig_dir proj args =
     let file = CUnix.remove_path_dot (CUnix.correct_path file orig_dir) in
     let () = match proj.project_file with
       | None -> ()
-      | Some _ -> Feedback.msg_warning (Pp.str
-	"Multiple project files are deprecated.")
+      | Some _ -> warning "Multiple project files are deprecated.@\n%!"
     in
     parsing_project_file := true;
     let proj = aux { proj with project_file = Some file } (parse file) in

tools/coqdep.ml

@@ -8,15 +8,24 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Printf
+open Format
 open Coqdep_lexer
 open Coqdep_common
-open System
+open Minisys
 
 (** The basic parts of coqdep (i.e. the parts used by [coqdep -boot])
     are now in [Coqdep_common]. The code that remains here concerns
     the other options. Calling this complete coqdep with the [-boot]
     option should be equivalent to calling [coqdep_boot].
+
+    As of today, this module depends on the following Coq modules:
+
+    - Flags
+    - Envars
+    - CoqProject_file
+
+    All of it for `coqlib` handling. Ideally we would like to clean
+    coqlib handling up so this can be bootstrapped earlier.
 *)
 
 let option_D = ref false
@@ -31,8 +40,7 @@ let warning_mult suf iter =
       let d' = Hashtbl.find tab f in
       if (Filename.dirname (file_name f d))
         <> (Filename.dirname (file_name f d')) then begin
-	  eprintf "*** Warning : the file %s is defined twice!\n" (f ^ suf);
-	  flush stderr
+          coqdep_warning "the file %s is defined twice!" (f ^ suf)
 	end
     with Not_found -> () end;
     Hashtbl.add tab f d
@@ -80,9 +88,7 @@ let mL_dep_list b f =
 	while true do
 	  let (Use_module str) = caml_action buf in
 	  if str = b then begin
-	    eprintf "*** Warning : in file %s the" f;
-	    eprintf " notation %s. is useless !\n" b;
-	    flush stderr
+            coqdep_warning "in file %s the notation %s. is useless !\n" f b
 	  end else
             if not (List.mem str !deja_vu) then addQueue deja_vu str
       	done; []
@@ -98,16 +104,13 @@ let affiche_Declare f dcl =
   printf "\n*** In file %s: \n" f;
   printf "Declare ML Module";
   List.iter (fun str -> printf " \"%s\"" str) dcl;
-  printf ".\n";
-  flush stdout
+  printf ".\n%!"
 
 let warning_Declare f dcl =
-  eprintf "*** Warning : in file %s, the ML modules" f;
-  eprintf " declaration should be\n";
+  eprintf "*** Warning : in file %s, the ML modules declaration should be\n" f;
   eprintf "*** Declare ML Module";
   List.iter (fun str -> eprintf " \"%s\"" str) dcl;
-  eprintf ".\n";
-  flush stderr
+  eprintf ".\n%!"
 
 let traite_Declare f =
   let decl_list = ref ([] : string list) in
@@ -149,7 +152,7 @@ let declare_dependencies () =
   List.iter
     (fun (name,_) ->
        traite_Declare (name^".v");
-       flush stdout)
+       pp_print_flush std_formatter ())
     (List.rev !vAccu)
 
 (** DAGs guaranteed to be transitive reductions *)
@@ -426,11 +429,11 @@ let coq_dependencies_dump chan dumpboxes =
     (DAG.empty, List.fold_left (fun ih (file, _) -> insert_raw_graph file ih) [] !vAccu,
     List.map fst !vAccu) !vAccu
   in
-  fprintf chan "digraph dependencies {\n"; flush chan;
+  fprintf chan "digraph dependencies {\n";
   if dumpboxes then print_graphs chan (pop_common_prefix graphs)
   else List.iter (fun (name, _) -> fprintf chan "\"%s\"[label=\"%s\"]\n" name (basename_noext name)) !vAccu;
   DAG.iter (fun name dep -> fprintf chan "\"%s\" -> \"%s\"\n" dep name) deps;
-  fprintf chan "}\n"
+  fprintf chan "}\n%!"
 
 end
 
@@ -498,7 +501,7 @@ let rec parse = function
   | "-suffix" :: s :: ll -> suffixe := s ; parse ll
   | "-suffix" :: [] -> usage ()
   | "-slash" :: ll ->
-    Printf.eprintf "warning: option -slash has no effect and is deprecated.\n";
+    coqdep_warning "warning: option -slash has no effect and is deprecated.";
     parse ll
   | "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll
   | "-dyndep" :: "opt" :: ll -> option_dynlink := Opt; parse ll
@@ -509,6 +512,9 @@ let rec parse = function
   | f :: ll -> treat_file None f; parse ll
   | [] -> ()
 
+(* Exception to be raised by Envars *)
+exception CoqlibError of string
+
 let coqdep () =
   if Array.length Sys.argv < 2 then usage ();
   if not Coq_config.has_natdynlink then option_dynlink := No;
@@ -520,18 +526,17 @@ let coqdep () =
   if !option_boot then begin
     add_rec_dir_import add_known "theories" ["Coq"];
     add_rec_dir_import add_known "plugins" ["Coq"];
-    add_caml_dir "tactics";
     add_rec_dir_import (fun _ -> add_caml_known) "theories" ["Coq"];
     add_rec_dir_import (fun _ -> add_caml_known) "plugins" ["Coq"];
   end else begin
-    Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg));
+    Envars.set_coqlib ~fail:(fun msg -> raise (CoqlibError msg));
     let coqlib = Envars.coqlib () in
     add_rec_dir_import add_coqlib_known (coqlib//"theories") ["Coq"];
     add_rec_dir_import add_coqlib_known (coqlib//"plugins") ["Coq"];
     let user = coqlib//"user-contrib" in
     if Sys.file_exists user then add_rec_dir_no_import add_coqlib_known user [];
     List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s [])
-      (Envars.xdg_dirs ~warn:(fun x -> Feedback.msg_warning (Pp.str x)));
+      (Envars.xdg_dirs ~warn:(fun x -> coqdep_warning "%s" x));
     List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s []) Envars.coqpath;
   end;
   List.iter (fun (f,d) -> add_mli_known f d ".mli") !mliAccu;
@@ -547,13 +552,13 @@ let coqdep () =
   | None -> ()
   | Some (box, file) ->
     let chan = open_out file in
-    try Graph.coq_dependencies_dump chan box; close_out chan
+    let chan_fmt = formatter_of_out_channel chan in
+    try Graph.coq_dependencies_dump chan_fmt box; close_out chan
     with e -> close_out chan; raise e
   end
 
 let _ =
   try
     coqdep ()
-  with CErrors.UserError(s,p) ->
-    let pp = (match s with | None -> p | Some s -> Pp.(str s ++ str ": " ++ p))  in
-    Format.eprintf "%a@\n%!" Pp.pp_with pp
+  with CoqlibError msg ->
+    eprintf "*** Error: %s@\n%!" msg

tools/coqdep_common.ml

@@ -8,9 +8,9 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Printf
-open Coqdep_lexer
+open Format
 open Unix
+open Coqdep_lexer
 open Minisys
 
 (** [coqdep_boot] is a stripped-down version of [coqdep], whose
@@ -20,14 +20,15 @@ open Minisys
     options (see for instance [option_dynlink] below).
 *)
 
+let coqdep_warning args =
+  eprintf "*** Warning: @[";
+  kfprintf (fun fmt -> fprintf fmt "@]\n%!") err_formatter args
+
 module StrSet = Set.Make(String)
 
 module StrList = struct type t = string list let compare = compare end
 module StrListMap = Map.Make(StrList)
 
-let stderr = Pervasives.stderr
-let stdout = Pervasives.stdout
-
 type dynlink = Opt | Byte | Both | No | Variable
 
 let option_c = ref false
@@ -114,8 +115,7 @@ let same_path_opt s s' =
 
 let warning_ml_clash x s suff s' suff' =
   if suff = suff' && not (same_path_opt s s') then
-  eprintf
-    "*** Warning: %s%s already found in %s (discarding %s%s)\n" x suff
+  coqdep_warning "%s%s already found in %s (discarding %s%s)\n" x suff
     (match s with None -> "." | Some d -> d)
     ((match s' with None -> "." | Some d -> d) // x) suff
 
@@ -180,13 +180,11 @@ let error_cannot_parse s (i,j) =
   exit 1
 
 let warning_module_notfound f s =
-  eprintf "*** Warning: in file %s, library %s is required and has not been found in the loadpath!\n%!"
+  coqdep_warning "in file %s, library %s is required and has not been found in the loadpath!"
     f (String.concat "." s)
 
 let warning_declare f s =
-  eprintf "*** Warning: in file %s, declared ML module " f;
-  eprintf "%s has not been found!\n" s;
-  flush stderr
+  coqdep_warning "in file %s, declared ML module %s has not been found!" f s
 
 let warning_clash file dir =
   match StrListMap.find dir !clash_v with
@@ -203,8 +201,7 @@ let warning_clash file dir =
   | _ -> assert false
 
 let warning_cannot_open_dir dir =
-  eprintf "*** Warning: cannot open %s\n" dir;
-  flush stderr
+  coqdep_warning "cannot open %s" dir
 
 let safe_assoc from verbose file k =
   if verbose && StrListMap.mem k !clash_v then warning_clash file k;
@@ -451,15 +448,13 @@ let mL_dependencies () =
        in
        let efullname = escape fullname in
        printf "%s.cmo:%s%s\n" efullname dep intf;
-       printf "%s.cmx:%s%s\n" efullname dep_opt intf;
-       flush stdout)
+       printf "%s.cmx:%s%s\n%!" efullname dep_opt intf)
     (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\n" (escape fullname) dep;
-       flush stdout)
+       printf "%s.cmi:%s\n%!" (escape fullname) dep)
     (List.rev !mliAccu);
   List.iter
     (fun (name,dirname) ->
@@ -468,8 +463,7 @@ let mL_dependencies () =
        let efullname = escape fullname in
        printf "%s_MLLIB_DEPENDENCIES:=%s\n" efullname (String.concat " " dep);
        printf "%s.cma:$(addsuffix .cmo,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname;
-       printf "%s.cmxa:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname;
-       flush stdout)
+       printf "%s.cmxa:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n%!" efullname efullname)
     (List.rev !mllibAccu);
   List.iter
     (fun (name,dirname) ->
@@ -483,7 +477,7 @@ let mL_dependencies () =
        List.iter (fun dep ->
          printf "%s.cmx : FOR_PACK=-for-pack %s\n" dep efullname_capital)
          dep;
-       flush stdout)
+       printf "%!")
     (List.rev !mlpackAccu)
 
 let coq_dependencies () =
@@ -496,8 +490,7 @@ let coq_dependencies () =
        printf "\n";
        printf "%s.vio: %s.v" ename ename;
        traite_fichier_Coq ".vio" true (name ^ ".v");
-       printf "\n";
-       flush stdout)
+       printf "\n%!")
     (List.rev !vAccu)
 
 let rec suffixes = function

tools/coqdep_common.mli

@@ -10,6 +10,8 @@
 
 module StrSet : Set.S with type elt = string
 
+val coqdep_warning : ('a, Format.formatter, unit, unit) format4 -> 'a
+
 (** [find_dir_logpath dir] Return the logical path of directory [dir]
     if it has been given one. Raise [Not_found] otherwise. In
     particular we can check if "." has been attributed a logical path