Revised warning API: warnings can have multiple categories

and categories can have subcategories, and also be used as warning names.

The terminology here means:
- warning: a name with a status (off/on/error)
- category: a name which contains categories and warnings, where
  "contain" means when it appears in the flag list it stands for all
  its elements.
- hybrid: a name which has its own status and may also contain
  categories and warnings.

In the implementation type `warning` is for both pure warnings and for
hybrids.
Type `category` internally includes some pure warnings, but the
exposed API only exposes it with pure categories and hybrids.

When a warning is in multiple categories (including transitively,
except "all") we print all of them. This may be a bit verbose (see
test changes) but still reasonable IMO. The categories would be pretty
undiscoverable without this.

----------

This allows us to have more specific warning names for deprecations
than just "deprecated-since-8.16". For instance with
`Arith.Minus.minus_n_O` we get
`deprecated-notation-since-8.16,deprecated-since-8.16,deprecated-notation,deprecated,default`.

We may want to instead create the warning name based on the specific
thing which is deprecated and warning_name_if_no_since instead a
common category, getting something like
`deprecated-Coq.Arith.Minus.minus_n_O,deprecated-notation,deprecated-since-8.16,deprecated,default`.

The code would be more complex so not sure if good idea.

----------

It also makes "default" almost a normal category (the way to get
included in "default" is still by the `default` argument instead of
including it in the category list).

BTW maybe it would be useful to have separate categories for
default-off default-on and default-error?

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.query
                    (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.query
                    (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

@@ -63,7 +63,7 @@ type bad_relevance =
 
 let warn_bad_relevance_name = "bad-relevance"
 let warn_bad_relevance =
-  CWarnings.create ~name:warn_bad_relevance_name ~category:"debug" ~default:CWarnings.AsError
+  CWarnings.create ~name:warn_bad_relevance_name ~category:CWarnings.CoreCategories.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 ".")

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" ~category:CWarnings.CoreCategories.option
     Pp.(fun name -> str "There is no debug flag \"" ++ str name ++ str "\".")
 
 let get_flags () =