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

9 files changed, 130 insertions, 93 deletions

diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 3fa600ac2..836f1982d 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -283,6 +283,10 @@ let register_automation_tac tac = my_automation_tac:= tac
 
 let automation_tac = Proofview.tclBIND (Proofview.tclUNIT ()) (fun () -> !my_automation_tac)
 
+let warn_insufficient_justification =
+  CWarnings.create ~name:"declmode-insufficient-justification" ~category:"declmode"
+    (fun () -> strbrk "Insufficient justification.")
+
 let justification tac gls=
     tclORELSE
       (tclSOLVE [tclTHEN tac (Proofview.V82.of_tactic assumption)])
@@ -291,7 +295,7 @@ let justification tac gls=
 	   error "Insufficient justification."
 	 else
 	   begin
-	     Feedback.msg_warning (str "Insufficient justification.");
+             warn_insufficient_justification ();
 	     daimon_tac gls
 	   end) gls
 
@@ -1219,6 +1223,9 @@ let hrec_for fix_id per_info gls obj_id =
   let hd2 = applist (mkVar fix_id,args@[obj]) in
     compose_lam rc (Reductionops.whd_beta gls.sigma hd2)
 
+let warn_missing_case =
+  CWarnings.create ~name:"declmode-missing-case" ~category:"declmode"
+    (fun () -> strbrk "missing case")
 
 let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
   match tree, objs  with
@@ -1293,8 +1300,8 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
 	       end;
 	       match bro with
 		   None ->
-		     Feedback.msg_warning (str "missing case");
-		     tacnext (mkMeta 1)
+                     warn_missing_case ();
+                     tacnext (mkMeta 1)
 		 | Some (sub_ids,tree) ->
 		     let br_args =
 		       List.filter
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index a03be5743..94981d0e1 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -583,8 +583,8 @@ let rec locate_ref = function
 	| None, Some r -> let refs,mps = locate_ref l in r::refs,mps
 	| Some mp, None -> let refs,mps = locate_ref l in refs,mp::mps
 	| Some mp, Some r ->
-	    warning_both_mod_and_cst q mp r;
-	    let refs,mps = locate_ref l in refs,mp::mps
+           warning_ambiguous_name (q,mp,r);
+           let refs,mps = locate_ref l in refs,mp::mps
 
 (*s Recursive extraction in the Coq toplevel. The vernacular command is
     \verb!Recursive Extraction! [qualid1] ... [qualidn]. Also used when
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 560fe5aea..81dfa603d 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -295,81 +295,94 @@ let pr_long_global ref = pr_path (Nametab.path_of_global ref)
 
 let err s = errorlabstrm "Extraction" s
 
+let warn_extraction_axiom_to_realize =
+  CWarnings.create ~name:"extraction-axiom-to-realize" ~category:"extraction"
+         (fun axioms ->
+          let s = if Int.equal (List.length axioms) 1 then "axiom" else "axioms" in
+          strbrk ("The following "^s^" must be realized in the extracted code:")
+                   ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global axioms)
+                   ++ str "." ++ fnl ())
+
+let warn_extraction_logical_axiom =
+  CWarnings.create ~name:"extraction-logical-axiom" ~category:"extraction"
+         (fun axioms ->
+          let s =
+            if Int.equal (List.length axioms) 1 then "axiom was" else "axioms were"
+          in
+          (strbrk ("The following logical "^s^" encountered:") ++
+             hov 1 (spc () ++ prlist_with_sep spc safe_pr_global axioms ++ str ".\n")
+           ++ strbrk "Having invalid logical axiom in the environment when extracting"
+           ++ spc () ++ strbrk "may lead to incorrect or non-terminating ML terms." ++
+             fnl ()))
+
 let warning_axioms () =
   let info_axioms = Refset'.elements !info_axioms in
-  if List.is_empty info_axioms then ()
-  else begin
-    let s = if Int.equal (List.length info_axioms) 1 then "axiom" else "axioms" in
-    Feedback.msg_warning
-      (str ("The following "^s^" must be realized in the extracted code:")
-       ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global info_axioms)
-       ++ str "." ++ fnl ())
-  end;
+  if not (List.is_empty info_axioms) then
+    warn_extraction_axiom_to_realize info_axioms;
   let log_axioms = Refset'.elements !log_axioms in
-  if List.is_empty log_axioms then ()
-  else begin
-    let s = if Int.equal (List.length log_axioms) 1 then "axiom was" else "axioms were"
-    in
-    Feedback.msg_warning
-      (str ("The following logical "^s^" encountered:") ++
-       hov 1
-         (spc () ++ prlist_with_sep spc safe_pr_global log_axioms ++ str ".\n")
-       ++
-       str "Having invalid logical axiom in the environment when extracting" ++
-       spc () ++ str "may lead to incorrect or non-terminating ML terms." ++
-       fnl ())
-  end
+  if not (List.is_empty log_axioms) then
+    warn_extraction_logical_axiom log_axioms
+
+let warn_extraction_opaque_accessed =
+  CWarnings.create ~name:"extraction-opaque-accessed" ~category:"extraction"
+    (fun lst -> strbrk "The extraction is currently set to bypass opacity, " ++
+                  strbrk "the following opaque constant bodies have been accessed :" ++
+                  lst ++ str "." ++ fnl ())
+
+let warn_extraction_opaque_as_axiom =
+  CWarnings.create ~name:"extraction-opaque-as-axiom" ~category:"extraction"
+    (fun lst -> strbrk "The extraction now honors the opacity constraints by default, " ++
+	 strbrk "the following opaque constants have been extracted as axioms :" ++
+	 lst ++ str "." ++ fnl () ++
+	 strbrk "If necessary, use \"Set Extraction AccessOpaque\" to change this."
+	 ++ fnl ())
 
 let warning_opaques accessed =
   let opaques = Refset'.elements !opaques in
-  if List.is_empty opaques then ()
-  else
+  if not (List.is_empty opaques) then
     let lst = hov 1 (spc () ++ prlist_with_sep spc safe_pr_global opaques) in
-    if accessed then
-      Feedback.msg_warning
-	(str "The extraction is currently set to bypass opacity,\n" ++
-	 str "the following opaque constant bodies have been accessed :" ++
-	 lst ++ str "." ++ fnl ())
-    else
-      Feedback.msg_warning
-	(str "The extraction now honors the opacity constraints by default,\n" ++
-	 str "the following opaque constants have been extracted as axioms :" ++
-	 lst ++ str "." ++ fnl () ++
-	 str "If necessary, use \"Set Extraction AccessOpaque\" to change this."
-	 ++ fnl ())
-
-let warning_both_mod_and_cst q mp r =
- Feedback.msg_warning
-   (str "The name " ++ pr_qualid q ++ str " is ambiguous, " ++
-    str "do you mean module " ++
-    pr_long_mp mp ++
-    str " or object " ++
-    pr_long_global r ++ str " ?" ++ fnl () ++
-    str "First choice is assumed, for the second one please use " ++
-    str "fully qualified name." ++ fnl ())
+    if accessed then warn_extraction_opaque_accessed lst
+    else warn_extraction_opaque_as_axiom lst
+
+let warning_ambiguous_name =
+  CWarnings.create ~name:"extraction-ambiguous-name" ~category:"extraction"
+    (fun (q,mp,r) -> strbrk "The name " ++ pr_qualid q ++ strbrk " is ambiguous, " ++
+                       strbrk "do you mean module " ++
+                       pr_long_mp mp ++
+                       strbrk " or object " ++
+                       pr_long_global r ++ str " ?" ++ fnl () ++
+                       strbrk "First choice is assumed, for the second one please use " ++
+                       strbrk "fully qualified name." ++ fnl ())
 
 let error_axiom_scheme r i =
   err (str "The type scheme axiom " ++ spc () ++
        safe_pr_global r ++ spc () ++ str "needs " ++ int i ++
        str " type variable(s).")
 
+let warn_extraction_inside_module =
+  CWarnings.create ~name:"extraction-inside-module" ~category:"extraction"
+      (fun () -> strbrk "Extraction inside an opened module is experimental." ++
+       strbrk "In case of problem, close it first.")
+
+
 let check_inside_module () =
   if Lib.is_modtype () then
     err (str "You can't do that within a Module Type." ++ fnl () ++
 	 str "Close it and try again.")
   else if Lib.is_module () then
-    Feedback.msg_warning
-      (str "Extraction inside an opened module is experimental.\n" ++
-       str "In case of problem, close it first.\n")
+    warn_extraction_inside_module ()
 
 let check_inside_section () =
   if Lib.sections_are_opened () then
     err (str "You can't do that within a section." ++ fnl () ++
 	 str "Close it and try again.")
 
-let warning_id s =
-  Feedback.msg_warning (str ("The identifier "^s^
-		    " contains __ which is reserved for the extraction"))
+let warn_extraction_reserved_identifier =
+  CWarnings.create ~name:"extraction-reserved-identifier" ~category:"extraction"
+    (fun s -> strbrk ("The identifier "^s^
+                " contains __ which is reserved for the extraction"))
+
+let warning_id s = warn_extraction_reserved_identifier s
 
 let error_constant r =
   err (safe_pr_global r ++ str " is not a constant.")
@@ -447,12 +460,15 @@ let error_remaining_implicit k =
        str "You might also try Unset Extraction SafeImplicits to force" ++
        fnl() ++ str "the extraction of unsafe code and review it manually.")
 
+let warn_extraction_remaining_implicit =
+  CWarnings.create ~name:"extraction-remaining-implicit" ~category:"extraction"
+    (fun s -> strbrk ("At least an implicit occurs after extraction : "^s^".") ++ fnl () ++
+     strbrk "Extraction SafeImplicits is unset, extracting nonetheless,"
+     ++ strbrk "but this code is potentially unsafe, please review it manually.")
+
 let warning_remaining_implicit k =
   let s = msg_of_implicit k in
-  Feedback.msg_warning
-    (str ("At least an implicit occurs after extraction : "^s^".") ++ fnl () ++
-     str "Extraction SafeImplicits is unset, extracting nonetheless," ++ fnl ()
-     ++ str "but this code is potentially unsafe, please review it manually.")
+  warn_extraction_remaining_implicit s
 
 let check_loaded_modfile mp = match base_mp mp with
   | MPfile dp ->
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 62c20bd3a..15a08756c 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -21,8 +21,7 @@ val safe_basename_of_global : global_reference -> Id.t
 
 val warning_axioms : unit -> unit
 val warning_opaques : bool -> unit
-val warning_both_mod_and_cst :
- qualid -> module_path -> global_reference -> unit
+val warning_ambiguous_name : ?loc:Loc.t -> qualid * module_path * global_reference -> unit
 val warning_id : string -> unit
 val error_axiom_scheme : global_reference -> int -> 'a
 val error_constant : global_reference -> 'a
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index cec3505a9..95095b09c 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -120,6 +120,11 @@ let pr_firstorder_using_raw _ _ _ l = str "using " ++ prlist_with_sep pr_comma p
 let pr_firstorder_using_glob _ _ _ l = str "using " ++ prlist_with_sep pr_comma (pr_or_var (fun x -> (pr_global (snd x)))) l
 let pr_firstorder_using_typed _ _ _ l = str "using " ++ prlist_with_sep pr_comma pr_global l
 
+let warn_deprecated_syntax =
+  CWarnings.create ~name:"firstorder-deprecated-syntax" ~category:"deprecated"
+    (fun () -> Pp.strbrk "Deprecated syntax; use \",\" as separator")
+
+
 ARGUMENT EXTEND firstorder_using
   TYPED AS reference_list
   PRINTED BY pr_firstorder_using_typed
@@ -130,8 +135,7 @@ ARGUMENT EXTEND firstorder_using
 | [ "using" reference(a) ] -> [ [a] ]
 | [ "using" reference(a) "," ne_reference_list_sep(l,",") ] -> [ a::l ]
 | [ "using" reference(a) reference(b) reference_list(l) ] -> [
-    Flags.if_verbose
-      Feedback.msg_warning (Pp.str "Deprecated syntax; use \",\" as separator");
+    warn_deprecated_syntax ();
     a::b::l
   ]
 | [ ] -> [ [] ]
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 893baad8c..93a89330e 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -198,15 +198,13 @@ let warning_error names e =
   let (e, _) = Cerrors.process_vernac_interp_error (e, Exninfo.null) in
   match e with
     | Building_graph e ->
-	Feedback.msg_warning
-	  (str "Cannot define graph(s) for " ++
-	     h 1 (pr_enum Libnames.pr_reference names) ++
-	     if do_observe () then (spc () ++ Errors.print e) else mt ())
+       let names = pr_enum Libnames.pr_reference names in
+       let error = if do_observe () then (spc () ++ Errors.print e) else mt () in
+       warn_cannot_define_graph (names,error)
     | Defining_principle e ->
-	Feedback.msg_warning
-	  (str "Cannot define principle(s) for "++
-	     h 1 (pr_enum Libnames.pr_reference names) ++
-	     if do_observe () then Errors.print e else mt ())
+       let names = pr_enum Libnames.pr_reference names in
+       let error = if do_observe () then Errors.print e else mt () in
+       warn_cannot_define_principle (names,error)
     | _ -> raise e
 
 
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 1c5eb1621..2ebbb34e4 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -227,6 +227,11 @@ let prepare_body ((name,_,args,types,_),_) rt =
 let process_vernac_interp_error e =
   fst (Cerrors.process_vernac_interp_error (e, Exninfo.null))
 
+let warn_funind_cannot_build_inversion =
+  CWarnings.create ~name:"funind-cannot-build-inversion" ~category:"funind"
+    (fun e' -> strbrk "Cannot build inversion information" ++
+                 if do_observe () then (fnl() ++ Errors.print e') else mt ())
+
 let derive_inversion fix_names =
   try
     let evd' = Evd.from_env (Global.env ()) in 
@@ -269,14 +274,20 @@ let derive_inversion fix_names =
 	lind;
       with e when Errors.noncritical e ->
       let e' = process_vernac_interp_error e in
-      Feedback.msg_warning
-	(str "Cannot build inversion information" ++
-	   if do_observe () then (fnl() ++ Errors.print e') else mt ())
+      warn_funind_cannot_build_inversion e'
   with e when Errors.noncritical e ->
-      let e' = process_vernac_interp_error e in
-      Feedback.msg_warning
-	(str "Cannot build inversion information (early)" ++
-	   if do_observe () then (fnl() ++ Errors.print e') else mt ())       
+    let e' = process_vernac_interp_error e in
+    warn_funind_cannot_build_inversion e'
+
+let warn_cannot_define_graph =
+  CWarnings.create ~name:"funind-cannot-define-graph" ~category:"funind"
+    (fun (names,error) -> strbrk "Cannot define graph(s) for " ++
+      h 1 names ++ error)
+
+let warn_cannot_define_principle =
+  CWarnings.create ~name:"funind-cannot-define-principle" ~category:"funind"
+  (fun (names,error) -> strbrk "Cannot define induction principle(s) for "++
+      h 1 names ++ error)
 
 let warning_error names e =
   let e = process_vernac_interp_error e in
@@ -294,15 +305,11 @@ let warning_error names e =
   in
   match e with
     | Building_graph e ->
-      Feedback.msg_warning
-	(str "Cannot define graph(s) for " ++
-	   h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
-	   e_explain e)
+       let names = prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names in
+       warn_cannot_define_graph (names,e_explain e)
     | Defining_principle e ->
-      Feedback.msg_warning
-	(str "Cannot define principle(s) for "++
-	   h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
-	   e_explain e)
+       let names = prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names in
+       warn_cannot_define_principle (names,e_explain e)
     | _ -> raise e
 
 let error_error names e =
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index e72069140..1c27bdfac 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -1,5 +1,9 @@
 open Misctypes
 
+val warn_cannot_define_graph : ?loc:Loc.t -> Pp.std_ppcmds * Pp.std_ppcmds -> unit
+
+val warn_cannot_define_principle : ?loc:Loc.t -> Pp.std_ppcmds * Pp.std_ppcmds -> unit
+
 val do_generate_principle :  
   bool -> 
   (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> 
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
index 3142c8cf0..89305838b 100644
--- a/plugins/syntax/nat_syntax.ml
+++ b/plugins/syntax/nat_syntax.ml
@@ -26,14 +26,16 @@ open Errors
 
 let threshold = of_int 5000
 
+let warn_large_nat =
+  CWarnings.create ~name:"large-nat" ~category:"numbers"
+    (fun () -> strbrk "Stack overflow or segmentation fault happens when " ++
+                 strbrk "working with large numbers in nat (observed threshold " ++
+                 strbrk "may vary from 5000 to 70000 depending on your system " ++
+                 strbrk "limits and on the command executed).")
+
 let nat_of_int dloc n =
   if is_pos_or_zero n then begin
-      if less_than threshold n then
-	Feedback.msg_warning
-	  (strbrk "Stack overflow or segmentation fault happens when " ++
-	   strbrk "working with large numbers in nat (observed threshold " ++
-	   strbrk "may vary from 5000 to 70000 depending on your system " ++
-	   strbrk "limits and on the command executed).");
+      if less_than threshold n then warn_large_nat ();
       let ref_O = GRef (dloc, glob_O, None) in
       let ref_S = GRef (dloc, glob_S, None) in
       let rec mk_nat acc n =