Merge PR rocq-prover#17585: Revised warning API: warnings can have multiple categories

Reviewed-by: proux01
Ack-by: Zimmi48
Co-authored-by: proux01 <[email protected]>

Author: coqbot-app[bot]

dev/ci/user-overlays/17585-SkySkimmer-warn-api.sh

@@ -0,0 +1,9 @@
+overlay elpi https://github.com/SkySkimmer/coq-elpi warn-api 17585
+
+overlay equations https://github.com/SkySkimmer/Coq-Equations warn-api 17585
+
+overlay metacoq https://github.com/SkySkimmer/metacoq warn-api 17585
+
+overlay quickchick https://github.com/SkySkimmer/QuickChick warn-api 17585
+
+overlay smtcoq https://github.com/SkySkimmer/smtcoq warn-api 17585

doc/changelog/08-vernac-commands-and-options/17585-warn-api.rst

@@ -0,0 +1,4 @@
+- **Changed:**
+  warnings can now have multiple categories allowing for finer user control on which warning to enable, disable or treat as an error
+  (`#17585 <https://github.com/coq/coq/pull/17585>`_,
+  by Gaëtan Gilbert).

doc/plugin_tutorial/tuto0/src/g_tuto0.mlg

@@ -5,7 +5,9 @@ DECLARE PLUGIN "coq-plugin-tutorial.tuto0"
 open Pp
 open Ltac_plugin
 
-let tuto_warn = CWarnings.create ~name:"name" ~category:"category"
+let cat = CWarnings.create_category ~name:"plugin-tuto-cat" ()
+
+let tuto_warn = CWarnings.create ~name:"name" ~category:cat
                             (fun _ -> strbrk Tuto0_main.message)
 
 }

interp/constrintern.ml

@@ -277,7 +277,7 @@ let pr_scope_stack begin_of_sentence l =
       str "[" ++ prlist_with_sep pr_comma str l ++ str "]"
 
 let warn_inconsistent_scope =
-  CWarnings.create ~name:"inconsistent-scopes" ~category:"syntax"
+  CWarnings.create ~name:"inconsistent-scopes" ~category:CWarnings.CoreCategories.syntax
     (fun (id,scopes1,scopes2) ->
       (str "Argument " ++ Id.print id ++
        strbrk " was previously inferred to be in " ++
@@ -336,7 +336,7 @@ let mkGLambda ?loc (na,bk,t) body = DAst.make ?loc @@ GLambda (na, bk, t, body)
 (* Utilities for binders                                              *)
 
 let warn_shadowed_implicit_name =
-  CWarnings.create ~name:"shadowed-implicit-name" ~category:"syntax"
+  CWarnings.create ~name:"shadowed-implicit-name" ~category:CWarnings.CoreCategories.syntax
     Pp.(fun na -> str "Making shadowed name of implicit argument accessible by position.")
 
 let exists_name na l =
@@ -503,7 +503,7 @@ let restore_binders_impargs env l =
   List.fold_right pure_push_name_env l env
 
 let warn_ignoring_unexpected_implicit_binder_declaration =
-  CWarnings.create ~name:"unexpected-implicit-declaration" ~category:"syntax"
+  CWarnings.create ~name:"unexpected-implicit-declaration" ~category:CWarnings.CoreCategories.syntax
     Pp.(fun () -> str "Ignoring implicit binder declaration in unexpected position.")
 
 let check_implicit_meaningful ?loc k env =
@@ -1350,7 +1350,7 @@ let intern_qualid_for_pattern test_global intern_not qid pats =
     | None -> raise Not_found
 
 let warn_nonprimitive_projection =
-  CWarnings.create ~name:"nonprimitive-projection-syntax" ~category:"syntax" ~default:CWarnings.Disabled
+  CWarnings.create ~name:"nonprimitive-projection-syntax" ~category:CWarnings.CoreCategories.syntax ~default:CWarnings.Disabled
     Pp.(fun f -> pr_qualid f ++ str " used as a primitive projection but is not one.")
 
 let error_nonprojection_syntax ?loc qid =

interp/implicit_quantifiers.ml

@@ -200,7 +200,7 @@ let implicit_application env ty =
     CAst.make ?loc @@ CAppExpl ((id, inst), args), avoid
 
 let warn_ignoring_implicit_status =
-  CWarnings.create ~name:"ignoring_implicit_status" ~category:"implicits"
+  CWarnings.create ~name:"ignoring-implicit-status" ~category:CWarnings.CoreCategories.implicits
     (fun na ->
        strbrk "Ignoring implicit status of product binder " ++
        Name.print na ++ strbrk " and following binders")

interp/notation.ml

@@ -135,7 +135,7 @@ let init_scope_map () =
 (* Operations on scopes *)
 
 let warn_undeclared_scope =
-  CWarnings.create ~name:"undeclared-scope" ~category:"deprecated"
+  CWarnings.create ~name:"undeclared-scope" ~category:CWarnings.CoreCategories.deprecated
                    (fun (scope) ->
                     strbrk "Declaring a scope implicitly is deprecated; use in advance an explicit "
                     ++ str "\"Declare Scope " ++ str scope ++ str ".\".")
@@ -685,15 +685,15 @@ module Numbers = struct
 open PrimTokenNotation
 
 let warn_large_num =
-  CWarnings.create ~name:"large-number" ~category:"numbers"
+  CWarnings.create ~name:"large-number" ~category:CWarnings.CoreCategories.numbers
     (fun ty ->
       strbrk "Stack overflow or segmentation fault happens when " ++
       strbrk "working with large numbers in " ++ pr_qualid ty ++
       strbrk " (threshold may vary depending" ++
       strbrk " on your system limits and on the command executed).")
 
 let warn_abstract_large_num =
-  CWarnings.create ~name:"abstract-large-number" ~category:"numbers"
+  CWarnings.create ~name:"abstract-large-number" ~category:CWarnings.CoreCategories.numbers
     (fun (ty,f) ->
       strbrk "To avoid stack overflow, large numbers in " ++
       pr_qualid ty ++ strbrk " are interpreted as applications of " ++
@@ -909,7 +909,7 @@ let interp_int63 ?loc esig ind n =
   else error_overflow ?loc n
 
 let warn_inexact_float =
-  CWarnings.create ~name:"inexact-float" ~category:"parsing"
+  CWarnings.create ~name:"inexact-float" ~category:CWarnings.CoreCategories.parsing
     (fun (sn, f) ->
       Pp.strbrk
         (Printf.sprintf
@@ -1335,26 +1335,30 @@ let pr_optional_scope = function
   | LastLonelyNotation -> mt ()
   | NotationInScope scope -> spc () ++ strbrk "in scope" ++ spc () ++ str scope
 
+let w_nota_overridden =
+  CWarnings.create_warning
+    ~from:[CWarnings.CoreCategories.parsing] ~name:"notation-overridden" ()
+
 let warn_notation_overridden =
-  CWarnings.create ~name:"notation-overridden" ~category:"parsing"
-                   (fun (scope,ntn) ->
-                    str "Notation" ++ spc () ++ pr_notation ntn ++ spc ()
-                    ++ strbrk "was already used" ++ pr_optional_scope scope ++ str ".")
+  CWarnings.create_in w_nota_overridden
+    (fun (scope,ntn) ->
+       str "Notation" ++ spc () ++ pr_notation ntn ++ spc ()
+       ++ strbrk "was already used" ++ pr_optional_scope scope ++ str ".")
 
 let warn_deprecation_overridden =
-  CWarnings.create ~name:"notation-overridden" ~category:"parsing"
-                 (fun ((scope,ntn),old,now) ->
-                  match old, now with
-                  | None, None -> assert false
-                  | None, Some _ ->
-                    (str "Notation" ++ spc () ++ pr_notation ntn ++ pr_optional_scope scope ++ spc ()
-                    ++ strbrk "is now marked as deprecated" ++ str ".")
-                  | Some _, None ->
-                    (str "Cancelling previous deprecation of notation" ++ spc () ++
-                     pr_notation ntn ++ pr_optional_scope scope ++ str ".")
-                  | Some _, Some _ ->
-                    (str "Amending deprecation of notation" ++ spc () ++
-                     pr_notation ntn ++ pr_optional_scope scope ++ str "."))
+  CWarnings.create_in w_nota_overridden
+    (fun ((scope,ntn),old,now) ->
+       match old, now with
+       | None, None -> assert false
+       | None, Some _ ->
+         (str "Notation" ++ spc () ++ pr_notation ntn ++ pr_optional_scope scope ++ spc ()
+          ++ strbrk "is now marked as deprecated" ++ str ".")
+       | Some _, None ->
+         (str "Cancelling previous deprecation of notation" ++ spc () ++
+          pr_notation ntn ++ pr_optional_scope scope ++ str ".")
+       | Some _, Some _ ->
+         (str "Amending deprecation of notation" ++ spc () ++
+          pr_notation ntn ++ pr_optional_scope scope ++ str "."))
 
 let warn_override_if_needed (scopt,ntn) overridden data old_data =
   if overridden then warn_notation_overridden (scopt,ntn)
@@ -2471,12 +2475,12 @@ let toggle_notations_in_scope ~on found inscope ntn_pattern ntns =
           data) ntns
 
 let warn_abbreviation_not_bound_to_entry =
-  CWarnings.create ~name:"conflicting-abbreviation-entry" ~category:"query"
+  CWarnings.create ~name:"conflicting-abbreviation-entry" ~category:CWarnings.CoreCategories.syntax
                    (fun () ->
                     strbrk "Activation of abbreviations does not expect mentioning a grammar entry.")
 
 let warn_abbreviation_not_bound_to_scope =
-  CWarnings.create ~name:"conflicting-abbreviation-scope" ~category:"query"
+  CWarnings.create ~name:"conflicting-abbreviation-scope" ~category:CWarnings.CoreCategories.syntax
                    (fun () ->
                     strbrk "Activation of abbreviations does not expect mentioning a scope.")
 

kernel/nativeconv.ml

@@ -142,9 +142,13 @@ and conv_fix env lvl t1 f1 t2 f2 cu =
     else aux (i+1) (conv_val env CONV flvl fi1 fi2 cu) in
   aux 0 cu
 
+let w_native_disabled = CWarnings.create_warning
+    ~from:[CWarnings.CoreCategories.native_compiler] ~name:"native-compiler-disabled"
+    ()
+
 let warn_no_native_compiler =
   let open Pp in
-  CWarnings.create ~name:"native-compiler-disabled" ~category:"native-compiler"
+  CWarnings.create_in w_native_disabled
          (fun () -> strbrk "Native compiler is disabled," ++
                       strbrk " falling back to VM conversion test.")
 

kernel/nativeconv.mli

@@ -17,3 +17,5 @@ val native_conv : conv_pb -> Genlambda.evars -> types kernel_conversion_function
 (** A conversion function parametrized by a universe comparator. Used outside of
     the kernel. *)
 val native_conv_gen : conv_pb -> Genlambda.evars -> (types, 'a) generic_conversion_function
+
+val w_native_disabled : CWarnings.warning

kernel/typeops.ml

@@ -57,26 +57,37 @@ let infer_assumption env t ty =
   with TypeError _ ->
     error_assumption env (make_judge t ty)
 
-type bad_relevance =
-| BadRelevanceBinder of Sorts.relevance * rel_declaration
-| BadRelevanceCase of Sorts.relevance * Constr.t
+type ('constr,'types) bad_relevance =
+| BadRelevanceBinder of Sorts.relevance * ('constr,'types) Context.Rel.Declaration.pt
+| BadRelevanceCase of Sorts.relevance * 'constr
 
 let warn_bad_relevance_name = "bad-relevance"
-let warn_bad_relevance =
-  CWarnings.create ~name:warn_bad_relevance_name ~category:"debug" ~default:CWarnings.AsError
-    Pp.(function
-        | BadRelevanceCase _ ->  str "Bad relevance in case annotation."
-        | BadRelevanceBinder (_, na) -> str "Bad relevance for binder " ++ Name.print (RelDecl.get_name na) ++ str ".")
 
-let warn_bad_relevance_case ?loc env rlv case = match CWarnings.get_status ~name:warn_bad_relevance_name with
+let bad_relevance_warning =
+  CWarnings.create_warning ~name:warn_bad_relevance_name ~default:CWarnings.AsError ()
+
+let bad_relevance_msg = CWarnings.create_msg bad_relevance_warning ()
+
+let default_print_bad_relevance = function
+  | BadRelevanceCase _ -> Pp.str "Bad relevance in case annotation."
+  | BadRelevanceBinder (_, na) ->
+    Pp.(str "Bad relevance for binder " ++ Name.print (RelDecl.get_name na) ++ str ".")
+
+(* used eg in the checker *)
+let () = CWarnings.register_printer bad_relevance_msg
+    (fun (_env,b) -> default_print_bad_relevance b)
+
+let warn_bad_relevance_case ?loc env rlv case =
+  match CWarnings.warning_status bad_relevance_warning with
 | CWarnings.Disabled | CWarnings.Enabled ->
-  warn_bad_relevance ?loc (BadRelevanceCase (rlv, mkCase case))
+  CWarnings.warn bad_relevance_msg ?loc (env, BadRelevanceCase (rlv, mkCase case))
 | CWarnings.AsError ->
   error_bad_case_relevance env rlv case
 
-let warn_bad_relevance_binder ?loc env rlv bnd = match CWarnings.get_status ~name:warn_bad_relevance_name with
+let warn_bad_relevance_binder ?loc env rlv bnd =
+  match CWarnings.warning_status bad_relevance_warning with
 | CWarnings.Disabled | CWarnings.Enabled ->
-  warn_bad_relevance ?loc (BadRelevanceBinder (rlv, bnd))
+  CWarnings.warn bad_relevance_msg ?loc (env, BadRelevanceBinder (rlv, bnd))
 | CWarnings.AsError ->
   error_bad_binder_relevance env rlv bnd
 

kernel/typeops.mli

@@ -124,12 +124,15 @@ val type_of_prim_or_type : env -> Univ.Instance.t -> CPrimitives.op_or_type -> t
 val warn_bad_relevance_name : string
 (** Allow the checker to make this warning into an error. *)
 
-val warn_bad_relevance_binder
-  : ?loc:Loc.t
-  -> Environ.env
-  -> Sorts.relevance
-  -> Constr.rel_declaration
-  -> unit
+val bad_relevance_warning : CWarnings.warning
+(** Also used by the pretyper to define a message which uses the evar map. *)
+
+type ('constr,'types) bad_relevance =
+| BadRelevanceBinder of Sorts.relevance * ('constr,'types) Context.Rel.Declaration.pt
+| BadRelevanceCase of Sorts.relevance * 'constr
+
+val bad_relevance_msg : (env * (constr,types) bad_relevance) CWarnings.msg
+(** Used by the higher layers to register a nicer printer than the default. *)
 
 val should_invert_case : env -> case_info -> bool
 (** We have case inversion exactly when going from irrelevant nonempty

kernel/vconv.ml

@@ -181,7 +181,7 @@ and conv_arguments env ?from:(from=0) k args1 args2 cu =
 
 let warn_bytecode_compiler_failed =
   let open Pp in
-  CWarnings.create ~name:"bytecode-compiler-failed" ~category:"bytecode-compiler"
+  CWarnings.create ~name:"bytecode-compiler-failed" ~category:CWarnings.CoreCategories.bytecode_compiler
          (fun () -> strbrk "Bytecode compiler failed, " ++
                       strbrk "falling back to standard conversion")
 

lib/cDebug.ml

@@ -52,7 +52,7 @@ let get_flag flag = !flag
 
 let set_flag flag v = flag := v
 
-let warn_unknown_debug = CWarnings.create ~name:"unknown-debug-flag" ~category:"option"
+let warn_unknown_debug = CWarnings.create ~name:"unknown-debug-flag"
     Pp.(fun name -> str "There is no debug flag \"" ++ str name ++ str "\".")
 
 let get_flags () =