From 8e07227c5853de78eaed4577eefe908fb84507c0 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 28 Jun 2016 10:55:30 +0200 Subject: A new infrastructure for warnings. On the user side, coqtop and coqc take a list of warning names or categories after -w. No prefix means activate the warning, a "-" prefix means deactivate it, and "+" means turn the warning into an error. Special categories include "all", and "default" which contains the warnings enabled by default. We also provide a vernacular Set Warnings which takes the same flags as argument. Note that coqc now prints warnings. The name and category of a warning are printed with the warning itself. On the developer side, Feedback.msg_warning is still accessible, but the recommended way to print a warning is in two steps: 1) create it by: let warn_my_warning = CWarnings.create ~name:"my-warning" ~category:"my-category" (fun args -> Pp.strbrk ...) 2) print it by: warn_my_warning args --- library/goptions.ml | 43 +++++++++++++++++++++++-------------------- library/libobject.ml | 39 ++++++--------------------------------- library/libobject.mli | 1 - library/library.ml | 16 ++++++++++------ library/loadpath.ml | 13 +++++++++---- library/nametab.ml | 17 ++++++++++------- 6 files changed, 58 insertions(+), 71 deletions(-) (limited to 'library') diff --git a/library/goptions.ml b/library/goptions.ml index 4aa3a2a21..7bead0b63 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -233,6 +233,11 @@ with Not_found -> open Libobject open Lib +let warn_deprecated_option = + CWarnings.create ~name:"deprecated-option" ~category:"deprecated" + (fun key -> str "Option" ++ spc () ++ str (nickname key) ++ + strbrk " is deprecated") + let declare_option cast uncast { optsync=sync; optdepr=depr; optname=name; optkey=key; optread=read; optwrite=write } = check_key key; @@ -270,10 +275,7 @@ let declare_option cast uncast begin fun v -> add_anonymous_leaf (gdecl_obj v) end else write,write,write in - let warn () = - if depr then - Feedback.msg_warning (str "Option " ++ str (nickname key) ++ str " is deprecated") - in + let warn () = if depr then warn_deprecated_option key in let cread () = cast (read ()) in let cwrite v = warn (); write (uncast v) in let clwrite v = warn (); lwrite (uncast v) in @@ -304,19 +306,22 @@ let declare_stringopt_option = (* Setting values of options *) +let warn_unknown_option = + CWarnings.create ~name:"unknown-option" ~category:"option" + (fun key -> strbrk "There is no option " ++ + str (nickname key) ++ str ".") + let set_option_value locality check_and_cast key v = - let (name, depr, (_,read,write,lwrite,gwrite)) = - try get_option key - with Not_found -> - errorlabstrm "Goptions.set_option_value" - (str "There is no option " ++ str (nickname key) ++ str ".") - in - let write = match locality with - | None -> write - | Some true -> lwrite - | Some false -> gwrite - in - write (check_and_cast v (read ())) + let opt = try Some (get_option key) with Not_found -> None in + match opt with + | None -> warn_unknown_option key + | Some (name, depr, (_,read,write,lwrite,gwrite)) -> + let write = match locality with + | None -> write + | Some true -> lwrite + | Some false -> gwrite + in + write (check_and_cast v (read ())) let bad_type_error () = error "Bad type of value for this option." @@ -346,13 +351,11 @@ let check_unset_value v = function let set_int_option_value_gen locality = set_option_value locality check_int_value let set_bool_option_value_gen locality key v = - try set_option_value locality check_bool_value key v - with UserError (_,s) -> Feedback.msg_warning s + set_option_value locality check_bool_value key v let set_string_option_value_gen locality = set_option_value locality check_string_value let unset_option_value_gen locality key = - try set_option_value locality check_unset_value key () - with UserError (_,s) -> Feedback.msg_warning s + set_option_value locality check_unset_value key () let set_int_option_value = set_int_option_value_gen None let set_bool_option_value = set_bool_option_value_gen None diff --git a/library/libobject.ml b/library/libobject.ml index b12d2038a..3e08b38b1 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -12,18 +12,6 @@ open Util module Dyn = Dyn.Make(struct end) -(* The relax flag is used to make it possible to load files while ignoring - failures to incorporate some objects. This can be useful when one - wants to work with restricted Coq programs that have only parts of - the full capabilities, but may still be able to work correctly for - limited purposes. One example is for the graphical interface, that uses - such a limited Coq process to do only parsing. It loads .vo files, but - is only interested in loading the grammar rule definitions. *) - -let relax_flag = ref false;; - -let relax b = relax_flag := b;; - type 'a substitutivity = Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a @@ -114,31 +102,16 @@ let declare_object_full odecl = try declare_object_full odecl with e -> Errors.fatal_error (Errors.print e) (Errors.is_anomaly e) -let missing_tab = (Hashtbl.create 17 : (string, unit) Hashtbl.t) - (* this function describes how the cache, load, open, and export functions - are triggered. In relaxed mode, this function just return a meaningless - value instead of raising an exception when they fail. *) + are triggered. *) let apply_dyn_fun deflt f lobj = let tag = object_tag lobj in - try - let dodecl = - try - Hashtbl.find cache_tab tag - with Not_found -> - failwith "local to_apply_dyn_fun" in - f dodecl - with - Failure "local to_apply_dyn_fun" -> - if not (!relax_flag || Hashtbl.mem missing_tab tag) then - begin - Feedback.msg_warning - (Pp.str ("Cannot find library functions for an object with tag " - ^ tag ^ " (a plugin may be missing)")); - Hashtbl.add missing_tab tag () - end; - deflt + let dodecl = + try Hashtbl.find cache_tab tag + with Not_found -> assert false + in + f dodecl let cache_object ((_,lobj) as node) = apply_dyn_fun () (fun d -> d.dyn_cache_function node) lobj diff --git a/library/libobject.mli b/library/libobject.mli index dbe0de8f8..51b9af059 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -107,7 +107,6 @@ val subst_object : substitution * obj -> obj val classify_object : obj -> obj substitutivity val discharge_object : object_name * obj -> obj option val rebuild_object : obj -> obj -val relax : bool -> unit (** {6 Debug} *) diff --git a/library/library.ml b/library/library.ml index bc7723f48..cead90700 100644 --- a/library/library.ml +++ b/library/library.ml @@ -271,6 +271,12 @@ exception LibUnmappedDir exception LibNotFound type library_location = LibLoaded | LibInPath +let warn_several_object_files = + CWarnings.create ~name:"several-object-files" ~category:"require" + (fun (vi, vo) -> str"Loading" ++ spc () ++ str vi ++ + strbrk " instead of " ++ str vo ++ + strbrk " because it is more recent") + let locate_absolute_library dir = (* Search in loadpath *) let pref, base = split_dirpath dir in @@ -287,9 +293,8 @@ let locate_absolute_library dir = | [] -> raise LibNotFound | [file] -> file | [vo;vi] when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> - Feedback.msg_warning (str"Loading " ++ str vi ++ str " instead of " ++ - str vo ++ str " because it is more recent"); - vi + warn_several_object_files (vi, vo); + vi | [vo;vi] -> vo | _ -> assert false @@ -311,8 +316,7 @@ let locate_qualified_library ?root ?(warn = true) qid = | [lpath, file] -> lpath, file | [lpath_vo, vo; lpath_vi, vi] when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> - Feedback.msg_warning (str"Loading " ++ str vi ++ str " instead of " ++ - str vo ++ str " because it is more recent"); + warn_several_object_files (vi, vo); lpath_vi, vi | [lpath_vo, vo; _ ] -> lpath_vo, vo | _ -> assert false @@ -753,7 +757,7 @@ let save_library_to ?todo dir f otab = error "Could not compile the library to native code." with reraise -> let reraise = Errors.push reraise in - let () = Feedback.msg_warning (str "Removed file " ++ str f') in + let () = Feedback.msg_notice (str "Removed file " ++ str f') in let () = close_out ch in let () = Sys.remove f' in iraise reraise diff --git a/library/loadpath.ml b/library/loadpath.ml index 33c0f41e1..6f4d79430 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -50,6 +50,13 @@ let remove_load_path dir = let filter p = not (String.equal p.path_physical dir) in load_paths := List.filter filter !load_paths +let warn_overriding_logical_loadpath = + CWarnings.create ~name:"overriding-logical-loadpath" ~category:"loadpath" + (fun (phys_path, old_path, coq_path) -> + str phys_path ++ strbrk " was previously bound to " ++ + pr_dirpath old_path ++ strbrk "; it is remapped to " ++ + pr_dirpath coq_path) + let add_load_path phys_path coq_path ~implicit = let phys_path = CUnix.canonical_path_name phys_path in let filter p = String.equal p.path_physical phys_path in @@ -72,10 +79,8 @@ let add_load_path phys_path coq_path ~implicit = let () = (* Do not warn when overriding the default "-I ." path *) if not (DirPath.equal old_path Nameops.default_root_prefix) then - Feedback.msg_warning - (str phys_path ++ strbrk " was previously bound to " ++ - pr_dirpath old_path ++ strbrk "; it is remapped to " ++ - pr_dirpath coq_path) in + warn_overriding_logical_loadpath (phys_path, old_path, coq_path) + in true in if replace then begin diff --git a/library/nametab.ml b/library/nametab.ml index db902d625..f533bc791 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -82,6 +82,14 @@ module Make (U : UserName) (E : EqualityType) : NAMETREE struct type elt = E.t + (* A name became inaccessible, even with absolute qualification. + Example: + Module F (X : S). Module X. + The argument X of the functor F is masked by the inner module X. + *) + let masking_absolute n = + Flags.if_verbose Feedback.msg_info (str ("Trying to mask the absolute name \"" ^ U.to_string n ^ "\"!")) + type user_name = U.t type path_status = @@ -119,9 +127,7 @@ struct | Absolute (n,_) -> (* This is an absolute name, we must keep it otherwise it may become unaccessible forever *) - Feedback.msg_warning (str ("Trying to mask the absolute name \"" - ^ U.to_string n ^ "\"!")); - tree.path + masking_absolute n; tree.path | Nothing | Relative _ -> Relative (uname,o) else tree.path @@ -144,7 +150,6 @@ struct | Nothing | Relative _ -> mktree (Absolute (uname,o)) tree.map - let rec push_exactly uname o level tree = function | [] -> anomaly (Pp.str "Prefix longer than path! Impossible!") @@ -155,9 +160,7 @@ let rec push_exactly uname o level tree = function | Absolute (n,_) -> (* This is an absolute name, we must keep it otherwise it may become unaccessible forever *) - Feedback.msg_warning (str ("Trying to mask the absolute name \"" - ^ U.to_string n ^ "\"!")); - tree.path + masking_absolute n; tree.path | Nothing | Relative _ -> Relative (uname,o) in -- cgit v1.2.3