diff --git a/doc/changelog/09-cli-tools/17946-br-fix-coqdep-warn.rst b/doc/changelog/09-cli-tools/17946-br-fix-coqdep-warn.rst new file mode 100644 index 000000000000..7de32ab13edb --- /dev/null +++ b/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 `_, + fixes `#10156 `_, + by David Swasey and Rodolphe Lepigre). diff --git a/lib/system.mli b/lib/system.mli index 353113454e35..fb1c1b754922 100644 --- a/lib/system.mli +++ b/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. *) diff --git a/man/coqdep.1 b/man/coqdep.1 index 436ea269f961..673c93dde7a1 100644 --- a/man/coqdep.1 +++ b/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" diff --git a/test-suite/misc/coqdep-require-filter-categories/stderr.ref b/test-suite/misc/coqdep-require-filter-categories/stderr.ref index d324d8ca99b0..c83fb7a445a5 100644 --- a/test-suite/misc/coqdep-require-filter-categories/stderr.ref +++ b/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] diff --git a/test-suite/misc/external-deps/file1.notfound.deps b/test-suite/misc/external-deps/file1.notfound.deps index 5a6f45cc4950..5985cbc7b335 100644 --- a/test-suite/misc/external-deps/file1.notfound.deps +++ b/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 diff --git a/test-suite/misc/external-deps/file2.notfound.deps b/test-suite/misc/external-deps/file2.notfound.deps index 07d683a83a81..ae49c0228372 100644 --- a/test-suite/misc/external-deps/file2.notfound.deps +++ b/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 diff --git a/tools/coqdep/coqdep.ml b/tools/coqdep/coqdep.ml index 779a7f8c58ce..b49ba233bb70 100644 --- a/tools/coqdep/coqdep.ml +++ b/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 diff --git a/tools/coqdep/lib/args.ml b/tools/coqdep/lib/args.ml index 1120add565bb..c6d8575343c5 100644 --- a/tools/coqdep/lib/args.ml +++ b/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] +\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 diff --git a/tools/coqdep/lib/common.ml b/tools/coqdep/lib/common.ml index eedb97eda316..aa95547d08af 100644 --- a/tools/coqdep/lib/common.ml +++ b/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 diff --git a/tools/coqdep/lib/loadpath.ml b/tools/coqdep/lib/loadpath.ml index c777f499c11f..36b3ae85dbea 100644 --- a/tools/coqdep/lib/loadpath.ml +++ b/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 diff --git a/tools/coqdep/lib/warning.ml b/tools/coqdep/lib/warning.ml deleted file mode 100644 index 049b0fa0faca..000000000000 --- a/tools/coqdep/lib/warning.ml +++ /dev/null @@ -1,14 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* fprintf fmt "@]\n%!") err_formatter args diff --git a/tools/coqdep/lib/warning.mli b/tools/coqdep/lib/warning.mli deleted file mode 100644 index 9e6d02c02411..000000000000 --- a/tools/coqdep/lib/warning.mli +++ /dev/null @@ -1,11 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* 'a