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

6 files changed, 58 insertions, 71 deletions

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