Merge PR coq#17946: Use CWarnings in coqdep

Reviewed-by: SkySkimmer
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>

doc/changelog/09-cli-tools/17946-br-fix-coqdep-warn.rst

@@ -0,0 +1,6 @@
+- **Changed:**
+  Add a `coqdep` option `-w` to adjust warnings and allow turning then into
+  errors like the corresponding `coqc` option
+  (`#17946 <https://github.com/coq/coq/pull/17946>`_,
+  fixes `#10156 <https://github.com/coq/coq/issues/10156>`_,
+  by David Swasey and Rodolphe Lepigre).

lib/system.mli

@@ -41,6 +41,8 @@ val process_subdirectories : (unix_path -> string -> unit) -> unix_path -> unit
 
 (** {6 Files and load paths} *)
 
+val warn_cannot_open_dir : ?loc:Loc.t -> string -> unit
+
 (** Load path entries remember the original root
     given by the user. For efficiency, we keep the full path (field
     [directory]), the root path and the path relative to the root. *)

man/coqdep.1

@@ -82,8 +82,12 @@ Includes dependencies about .vos files.
 .TP
 .B \-dyndep (opt|byte|both|no|var)
 Set how dependencies over ML modules are printed.
+.TP
 .B \-m META
 Resolve plugin names using the META file.
+.TP
+.B \-w w1,...,wn
+Configure display of warnings as for coqc.
 
 .SH EXIT STATUS
 .IP "1"

test-suite/misc/coqdep-require-filter-categories/stderr.ref

@@ -1 +1,3 @@
-*** Warning: in file fA.v, library nonexistent is required and has not been found in the loadpath!
+Warning: in file fA.v, library
+         nonexistent is required and has not been found in the loadpath!
+         [module-not-found,filesystem,default]

test-suite/misc/external-deps/file1.notfound.deps

@@ -1,3 +1,5 @@
-*** Warning: in file misc/external-deps/file1.v, external file d1 is required from root foo.bar and has not been found in the loadpath!
+Warning: in file misc/external-deps/file1.v, external file d1 is required
+         from root foo.bar and has not been found in the loadpath!
+         [module-not-found,filesystem,default]
 misc/external-deps/file1.vo misc/external-deps/file1.glob misc/external-deps/file1.v.beautified misc/external-deps/file1.required_vo: misc/external-deps/file1.v 
 misc/external-deps/file1.vio: misc/external-deps/file1.v 

test-suite/misc/external-deps/file2.notfound.deps

@@ -1,3 +1,5 @@
-*** Warning: in file misc/external-deps/file2.v, external file d1 is required from root foo.bar and has not been found in the loadpath!
+Warning: in file misc/external-deps/file2.v, external file d1 is required
+         from root foo.bar and has not been found in the loadpath!
+         [module-not-found,filesystem,default]
 misc/external-deps/file2.vo misc/external-deps/file2.glob misc/external-deps/file2.v.beautified misc/external-deps/file2.required_vo: misc/external-deps/file2.v 
 misc/external-deps/file2.vio: misc/external-deps/file2.v 

tools/coqdep/coqdep.ml

@@ -11,9 +11,15 @@
 (** The basic parts of coqdep are in [Common]. *)
 open Coqdeplib
 
+let warn_home_dir =
+  let category = CWarnings.CoreCategories.filesystem in
+  CWarnings.create ~name:"cannot-locate-home-dir" ~category Pp.str
+
 let coqdep () =
   let open Common in
 
+  ignore (Feedback.(add_feeder (console_feedback_listener Format.err_formatter)));
+
   (* Initialize coqdep, add files to dependency computation *)
   if Array.length Sys.argv < 2 then Args.usage ();
   let args =
@@ -42,11 +48,11 @@ let coqdep () =
     let user_contrib = Boot.Env.(user_contrib env |> Path.to_string) in
     Loadpath.add_rec_dir_import (Loadpath.add_coqlib_known lst) stdlib ["Coq"];
     Loadpath.add_rec_dir_import (Loadpath.add_coqlib_known lst) plugins ["Coq"];
-    if Sys.file_exists user_contrib
-    then Loadpath.add_rec_dir_no_import (Loadpath.add_coqlib_known lst) user_contrib [];
-    List.iter (fun s -> Loadpath.add_rec_dir_no_import (Loadpath.add_coqlib_known lst) s [])
-      (Envars.xdg_dirs ~warn:(fun x -> Warning.give "%s" x));
-    List.iter (fun s -> Loadpath.add_rec_dir_no_import (Loadpath.add_coqlib_known lst) s []) Envars.coqpath;
+    if Sys.file_exists user_contrib then
+      Loadpath.add_rec_dir_no_import (Loadpath.add_coqlib_known lst) user_contrib [];
+    let add_dir s = Loadpath.add_rec_dir_no_import (Loadpath.add_coqlib_known lst) s [] in
+    List.iter add_dir (Envars.xdg_dirs ~warn:warn_home_dir);
+    List.iter add_dir Envars.coqpath
   end;
   if args.Args.sort then
     sort st

tools/coqdep/lib/args.ml

@@ -35,6 +35,10 @@ let make () =
   }
 
 
+let warn_unknown_option =
+  CWarnings.create ~name:"unknown-option"
+    Pp.(fun opt -> str "Unknown option \"" ++ str opt ++ str "\".")
+
 let usage () =
   let open Printf in
   eprintf " usage: coqdep [options] <filename>+\n";
@@ -52,6 +56,7 @@ let usage () =
   eprintf "  -coqlib dir : set the coq standard library directory\n";
   eprintf "  -dyndep (opt|byte|both|no|var) : set how dependencies over ML modules are printed\n";
   eprintf "  -m META : resolve plugins names using the META file\n";
+  eprintf "  -w (w1,..,wn) : configure display of warnings\n";
   exit 1
 
 let parse st args =
@@ -74,9 +79,13 @@ let parse st args =
     | "-coqlib" :: [] -> usage ()
     | "-dyndep" :: dyndep :: ll -> parse { st with dyndep } ll
     | "-m" :: m :: ll -> parse { st with meta_files = st.meta_files @ [m]} ll
+    | "-w" :: w :: ll ->
+      let w = if w = "none" then w else CWarnings.get_flags() ^ "," ^ w in
+      CWarnings.set_flags w;
+      parse st ll
     | ("-h"|"--help"|"-help") :: _ -> usage ()
     | opt :: ll when String.length opt > 0 && opt.[0] = '-' ->
-      Warning.give "unknown option %s" opt;
+      warn_unknown_option opt;
       parse st ll
     | f :: ll -> parse { st with files = f :: st.files } ll
     | [] -> st

tools/coqdep/lib/common.ml

@@ -44,18 +44,25 @@ let addQueue q v = q := v :: !q
 type what = Library | External
 let str_of_what = function Library -> "library" | External -> "external file"
 
-let warning_module_notfound ?(what=Library) from f s =
-  let what = str_of_what what in
-  match from with
-  | None ->
-    Warning.give "in file %s, %s %s is required and has not been found in the loadpath!"
-      f what (String.concat "." s)
-  | Some pth ->
-    Warning.give "in file %s, %s %s is required from root %s and has not been found in the loadpath!"
-      f what (String.concat "." s) (String.concat "." pth)
+let warning_module_notfound =
+  let warn (what, from, f, s) =
+    let open Pp in
+    str "in file " ++ str f ++ str ", " ++
+    str (str_of_what what) ++ spc () ++ str (String.concat "." s) ++ str " is required" ++
+    pr_opt (fun pth -> str "from root " ++ str (String.concat "." pth)) from ++
+    str " and has not been found in the loadpath!"
+  in
+  CWarnings.create ~name:"module-not-found"
+    ~category:CWarnings.CoreCategories.filesystem warn
 
-let warning_declare f s =
-  Warning.give "in file %s, declared ML module %s has not been found!" f s
+let warning_declare =
+  let warn (f, s) =
+    let open Pp in
+    str "in file " ++ str f ++ str ", declared ML module " ++ str s ++
+    str " has not been found!"
+  in
+  CWarnings.create ~name:"declared-module-not-found"
+    ~category:CWarnings.CoreCategories.filesystem warn
 
 let warn_if_clash ?(what=Library) exact file dir f1 = let open Format in function
   | f2::fl ->
@@ -180,7 +187,7 @@ let rec find_dependencies st basename =
                     add_dep (Dep_info.Dep.Require file_str)) files
               | None ->
                 if verbose && not (Loadpath.is_in_coqlib st ?from str) then
-                  warning_module_notfound from f str
+                  warning_module_notfound (Library, from, f, str)
             end
           in
           List.iter decl strl
@@ -205,7 +212,7 @@ let rec find_dependencies st basename =
                 | None ->
                   match Loadpath.search_mlpack_known st s with
                   | Some mldir -> declare ".cmo" (pick_mldir mldir) s
-                  | None -> warning_declare f str
+                  | None -> warning_declare (f,str)
               end
           in
           List.iter decl sl
@@ -235,7 +242,7 @@ let rec find_dependencies st basename =
           begin match safe_assoc st ~what:External (Some from) verbose f [str] with
           | Some (file :: _) -> add_dep (Dep_info.Dep.Other (canonize file))
           | Some [] -> assert false
-          | None -> warning_module_notfound ~what:External (Some from) f [str]
+          | None -> warning_module_notfound (External, Some from, f, [str])
           end
       done;
       List.rev !dependencies
@@ -326,12 +333,15 @@ let sort st =
   in
   List.iter (fun (name, _) -> loop name) !vAccu
 
+let warn_project_file =
+  let category = CWarnings.CoreCategories.filesystem in
+  CWarnings.create ~name:"project-file" ~category Pp.str
+
 let treat_coqproject st f =
   let open CoqProject_file in
   let iter_sourced f = List.iter (fun {thing} -> f thing) in
-  let warning_fn x = Warning.give "%s" x in
   let project =
-    try read_project_file ~warning_fn f
+    try read_project_file ~warning_fn:warn_project_file f
     with
     | Parsing_error msg -> Error.cannot_parse_project_file f msg
     | UnableToOpenProjectFile msg -> Error.cannot_open_project_file msg

tools/coqdep/lib/loadpath.ml

@@ -95,9 +95,6 @@ let register_dir_logpath, find_dir_logpath =
     (see discussion at PR #14718)
 *)
 
-let warning_cannot_open_dir dir =
-  Warning.give "cannot open %s" dir
-
 let add_directory recur add_file phys_dir log_dir =
   let root = (phys_dir, log_dir) in
   let stack = ref [] in
@@ -123,7 +120,7 @@ let add_directory recur add_file phys_dir log_dir =
         System.process_directory f phys_dir
       end
     else
-      warning_cannot_open_dir phys_dir
+      System.warn_cannot_open_dir phys_dir
   in
   aux phys_dir log_dir;
   List.iter (fun (phys_dir, log_dir, f) -> add_file root phys_dir log_dir f) !subdirfiles;
@@ -157,11 +154,19 @@ let rec cuts recur = function
     ([],if recur then suffixes true l else [true,l]) ::
     List.map (fun (fromtail,suffixes) -> (dir::fromtail,suffixes)) (cuts true tail)
 
+let warning_ml_clash =
+  let category = CWarnings.CoreCategories.filesystem in
+  CWarnings.create ~name:"multiple-matching-files" ~category
+    Pp.(fun (basename, suff, dir, dir') ->
+      str (basename ^ suff) ++ str " already found in " ++
+      str (match dir with None -> "." | Some d -> d) ++
+      str " (discarding " ++
+      str (System.((match dir' with None -> "." | Some d -> d) // basename)) ++
+      str suff ++ str ")"
+    )
 let warning_ml_clash x s suff s' suff' =
   if suff = suff' && not (same_path_opt s s') then
-    Warning.give "%s%s already found in %s (discarding %s%s)\n" x suff
-    (match s with None -> "." | Some d -> d)
-    System.((match s' with None -> "." | Some d -> d) // x) suff
+    warning_ml_clash (x,suff,s,s')
 
 type result =
   | ExactMatches of filename list