Remove low-value warning categories

SkySkimmer · SkySkimmer · commit 805fdc3d2041 · 2023-05-26T17:42:46.000+02:00
diff --git a/interp/implicit_quantifiers.ml b/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:CWarnings.CoreCategories.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")
diff --git a/interp/notation.ml b/interp/notation.ml
@@ -2475,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:CWarnings.CoreCategories.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:CWarnings.CoreCategories.query
+  CWarnings.create ~name:"conflicting-abbreviation-scope" ~category:CWarnings.CoreCategories.syntax
                    (fun () ->
                     strbrk "Activation of abbreviations does not expect mentioning a scope.")
 
diff --git a/kernel/typeops.ml b/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:CWarnings.CoreCategories.debug ~default:CWarnings.AsError
+  CWarnings.create ~name:warn_bad_relevance_name ~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 ".")
diff --git a/lib/cDebug.ml b/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:CWarnings.CoreCategories.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 () =
diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml
@@ -377,38 +377,23 @@ module CoreCategories = struct
   let automation = make "automation"
   let bytecode_compiler = make "bytecode-compiler"
   let coercions = make "coercions"
-  let debug = make "debug"
   let deprecated = make "deprecated"
-  let dev = make "dev"
   let extraction = make "extraction"
   let filesystem = make "filesystem"
   let fixpoints = make "fixpoints"
   let fragile = make "fragile"
   let funind = make "funind"
   let implicits = make "implicits"
-  let loadpath = make "loadpath"
   let ltac = make "ltac"
   let ltac2 = make "ltac2"
-  let modules = make "modules"
   let native_compiler = make "native-compiler"
-  let non_interactive = make "non-interactive"
-  let notation = make "notation"
   let numbers = make "numbers"
-  let option = make "option"
   let parsing = make "parsing"
-  let pattern_matching = make "pattern-matching"
   let pedantic = make "pedantic"
-  let query = make "query"
   let records = make "records"
-  let require = make "require"
-  let schemes = make "schemes"
-  let scope = make "scope"
   let ssr = make "ssr"
   let syntax = make "syntax"
   let tactics = make "tactics"
-  let typechecker = make "typechecker"
-  let typeclasses = make "typeclasses"
-  let universes = make "universes"
   let vernacular = make "vernacular"
 
 end
diff --git a/lib/cWarnings.mli b/lib/cWarnings.mli
@@ -92,38 +92,23 @@ module CoreCategories : sig
   val automation : category
   val bytecode_compiler : category
   val coercions : category
-  val debug : category
   val deprecated : category
-  val dev : category
   val extraction : category
   val filesystem : category
   val fixpoints : category
   val fragile : category
   val funind : category
   val implicits : category
-  val loadpath : category
   val ltac : category
   val ltac2 : category
-  val modules : category
   val native_compiler : category
-  val non_interactive : category
-  val notation : category
   val numbers : category
-  val option : category
   val parsing : category
-  val pattern_matching : category
   val pedantic : category
-  val query : category
   val records : category
-  val require : category
-  val schemes : category
-  val scope : category
   val ssr : category
   val syntax : category
   val tactics : category
-  val typechecker : category
-  val typeclasses : category
-  val universes : category
   val vernacular : category
 
 end
diff --git a/lib/system.ml b/lib/system.ml
@@ -207,8 +207,8 @@ let is_in_path lpath filename =
   with Not_found -> false
 
 let warn_path_not_found =
-  CWarnings.create ~name:"path-not-found" ~category:CWarnings.CoreCategories.filesystem
-  (fun () -> str "system variable PATH not found")
+  CWarnings.create ~name:"PATH-not-found"
+  (fun () -> str "Environment variable PATH not set")
 
 let is_in_system_path filename =
   try
diff --git a/library/goptions.ml b/library/goptions.ml
@@ -427,7 +427,7 @@ let declare_interpreted_string_option_and_ref ~stage ~depr ~key ~(value:'a) from
 
 let warn_unknown_option =
   CWarnings.create
-    ~name:"unknown-option" ~category:CWarnings.CoreCategories.option
+    ~name:"unknown-option"
     Pp.(fun key -> strbrk "There is no flag or option with this name: \"" ++
                   str (nickname key) ++ str "\".")
 
diff --git a/library/summary.ml b/library/summary.ml
@@ -83,14 +83,10 @@ let freeze_summaries ~marshallable sum_map =
   HMap.map map sum_map
 
 let warn_summary_out_of_scope =
-  let name = "summary-out-of-scope" in
-  let category = CWarnings.CoreCategories.dev in
-  let default = CWarnings.Disabled in
-  CWarnings.create ~name ~category ~default (fun name ->
-    Pp.str (Printf.sprintf
-      "A Coq plugin was loaded inside a local scope (such as a Section). It is recommended to load plugins at the start of the file. Summary entry: %s"
-      name)
-    )
+  CWarnings.create ~name:"summary-out-of-scope" ~default:Disabled Pp.(fun name ->
+      str "A Coq plugin was loaded inside a local scope (such as a Section)." ++ spc() ++
+      str "It is recommended to load plugins at the start of the file." ++ spc() ++
+      str "Summary entry: " ++ str name)
 
 let unfreeze_summaries ?(partial=false) sum_map summaries =
   (* We must be independent on the order of the map! *)
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
@@ -561,7 +561,7 @@ let set_pattern_catch_all_var ?loc eqn = function
     eqn
 
 let warn_named_multi_catch_all =
-  CWarnings.create ~name:"unused-pattern-matching-variable" ~category:CWarnings.CoreCategories.pattern_matching
+  CWarnings.create ~name:"unused-pattern-matching-variable"
          (fun id ->
           strbrk "Unused variable " ++ Id.print id
           ++ strbrk " might be a misspelled constructor. Use _ or _"
diff --git a/pretyping/coercionops.ml b/pretyping/coercionops.ml
@@ -304,7 +304,7 @@ let install_path_comparator f = path_comparator := f
 let compare_path env sigma cl p q = !path_comparator env sigma cl p q
 
 let warn_ambiguous_path =
-  CWarnings.create ~name:"ambiguous-paths" ~category:CWarnings.CoreCategories.typechecker
+  CWarnings.create ~name:"ambiguous-paths" ~category:CWarnings.CoreCategories.coercions
     (fun l -> prlist_with_sep fnl (fun (c,p,q) ->
          str"New coercion path " ++ print_path (c,p) ++
          if List.is_empty q then
diff --git a/pretyping/structures.ml b/pretyping/structures.ml
@@ -195,7 +195,7 @@ let keep_true_projections projs =
   List.map_filter filter projs
 
 let warn_projection_no_head_constant =
-  CWarnings.create ~name:"projection-no-head-constant" ~category:CWarnings.CoreCategories.typechecker
+  CWarnings.create ~name:"projection-no-head-constant" ~category:CWarnings.CoreCategories.records
          (fun (sign,env,t,ref,proji_sp) ->
           let env = Environ.push_rel_context sign env in
           let con_pp = Nametab.pr_global_env Id.Set.empty ref in
@@ -244,7 +244,7 @@ let compute_canonical_projections env ~warn (gref,ind) =
     ) [] lpj projs
 
 let warn_redundant_canonical_projection =
-  CWarnings.create ~name:"redundant-canonical-projection" ~category:CWarnings.CoreCategories.typechecker
+  CWarnings.create ~name:"redundant-canonical-projection" ~category:CWarnings.CoreCategories.records
          (fun (hd_val,prj,new_can_s,old_can_s) ->
           strbrk "Ignoring canonical projection to " ++ hd_val
           ++ strbrk " by " ++ prj ++ strbrk " in "
diff --git a/stm/stm.ml b/stm/stm.ml
@@ -1111,7 +1111,7 @@ end = struct (* {{{ *)
         | Cont acc -> next acc
 
   let undo_costly_in_batch_mode =
-    CWarnings.create ~name:"undo-batch-mode" ~category:CWarnings.CoreCategories.non_interactive Pp.(fun v ->
+    CWarnings.create ~name:"undo-batch-mode" Pp.(fun v ->
         str "Command " ++ Ppvernac.pr_vernac v ++
         str (" is not recommended in batch mode. In particular, going back in the document" ^
              " is not efficient in batch mode due to Coq not caching previous states for memory optimization reasons." ^
diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml
@@ -38,7 +38,7 @@ let cbv_vm env sigma c =
   end
 
 let warn_native_compute_disabled =
-  CWarnings.create ~name:"native-compute-disabled" ~category:CWarnings.CoreCategories.native_compiler
+  CWarnings.create_in Nativeconv.w_native_disabled
   (fun () ->
    strbrk "native_compute disabled at configure time; falling back to vm_compute.")
 
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
@@ -193,8 +193,7 @@ end
 Arguments stray N
 File "./output/Cases.v", line 253, characters 4-5:
 Warning: Unused variable B might be a misspelled constructor. Use _ or _B to
-silence this warning.
-[unused-pattern-matching-variable,pattern-matching,default]
+silence this warning. [unused-pattern-matching-variable,default]
 File "./output/Cases.v", line 266, characters 33-40:
 The command has indeed failed with message:
 Application of arguments to a recursive notation not supported in patterns.
@@ -254,13 +253,10 @@ end
      : J' bool (true, true) -> nat * nat
 File "./output/Cases.v", line 313, characters 3-4:
 Warning: Unused variable x might be a misspelled constructor. Use _ or _x to
-silence this warning.
-[unused-pattern-matching-variable,pattern-matching,default]
+silence this warning. [unused-pattern-matching-variable,default]
 File "./output/Cases.v", line 314, characters 6-7:
 Warning: Unused variable y might be a misspelled constructor. Use _ or _y to
-silence this warning.
-[unused-pattern-matching-variable,pattern-matching,default]
+silence this warning. [unused-pattern-matching-variable,default]
 File "./output/Cases.v", line 314, characters 3-4:
 Warning: Unused variable x might be a misspelled constructor. Use _ or _x to
-silence this warning.
-[unused-pattern-matching-variable,pattern-matching,default]
+silence this warning. [unused-pattern-matching-variable,default]
diff --git a/test-suite/output/DebugFlags.out b/test-suite/output/DebugFlags.out
@@ -1,6 +1,6 @@
 File "./output/DebugFlags.v", line 1, characters 0-33:
 Warning: There is no debug flag "ThisFlagDoesNotExist".
-[unknown-debug-flag,option,default]
+[unknown-debug-flag,default]
 Debug: [Cbv] Unfolding Coq.Init.Datatypes.id
      = tt
      : unit
diff --git a/test-suite/output/Warnings.out b/test-suite/output/Warnings.out
@@ -1,4 +1,4 @@
 File "./output/Warnings.v", line 4, characters 0-22:
 Warning: Projection value has no head constant: let H := tt in True in
 canonical instance a of b, ignoring it.
-[projection-no-head-constant,typechecker,default]
+[projection-no-head-constant,records,default]
diff --git a/test-suite/output/bug_16224.out b/test-suite/output/bug_16224.out
@@ -5,7 +5,7 @@ use '#[global] Existing Instance field.' for compatibility with Coq < 8.17).
 Beware that the default locality for '::' is #[export], as opposed to
 #[global] for ':>' currently. Add an explicit #[global] attribute to the
 field if you need to keep the current behavior. For example: "Class foo := {
-#[global] field :: bar }." [future-coercion-class-field,records,default]
+#[global] field :: bar }." [future-coercion-class-field,deprecated,default]
 [rc] : Rc >-> A (reversible)
 [ric] : Ric >-> A (reversible)
 ric : Ric -> A
diff --git a/test-suite/output/bug_5222.out b/test-suite/output/bug_5222.out
@@ -4,7 +4,7 @@
   True = (nil : T1 nat)
 File "./output/bug_5222.v", line 16, characters 2-40:
 Warning: C2 does not respect the uniform inheritance condition.
-[uniform-inheritance,typechecker,default]
+[uniform-inheritance,coercions,default]
 1 goal
   
   ============================
diff --git a/test-suite/output/coercions_nonuniform.out b/test-suite/output/coercions_nonuniform.out
@@ -1,9 +1,9 @@
 File "./output/coercions_nonuniform.v", line 22, characters 0-21:
 Warning: f does not respect the uniform inheritance condition.
-[uniform-inheritance,typechecker,default]
+[uniform-inheritance,coercions,default]
 File "./output/coercions_nonuniform.v", line 55, characters 0-17:
 Warning: f' does not respect the uniform inheritance condition.
-[uniform-inheritance,typechecker,default]
+[uniform-inheritance,coercions,default]
 File "./output/coercions_nonuniform.v", line 71, characters 7-17:
 The command has indeed failed with message:
 This command does not support this attribute: nonuniform.
diff --git a/test-suite/output/interleave_options_bad_order.out b/test-suite/output/interleave_options_bad_order.out
@@ -1,4 +1,4 @@
 While loading initial state:
 Warning: There is no flag or option with this name: "Extraction Optimize".
-[unknown-option,option,default]
+[unknown-option,default]
 Extraction Optimize is on
diff --git a/test-suite/output/relaxed_ambiguous_paths.out b/test-suite/output/relaxed_ambiguous_paths.out
@@ -1,11 +1,11 @@
 File "./output/relaxed_ambiguous_paths.v", line 13, characters 0-29:
 Warning:
 New coercion path [g1; f2] : A >-> B' is ambiguous with existing 
-[f1; g2] : A >-> B'. [ambiguous-paths,typechecker,default]
+[f1; g2] : A >-> B'. [ambiguous-paths,coercions,default]
 File "./output/relaxed_ambiguous_paths.v", line 14, characters 0-29:
 Warning:
 New coercion path [h1; f3] : B >-> C' is ambiguous with existing 
-[f2; h2] : B >-> C'. [ambiguous-paths,typechecker,default]
+[f2; h2] : B >-> C'. [ambiguous-paths,coercions,default]
 [f1] : A >-> A'
 [g1] : A >-> B
 [f1; g2] : A >-> B'
@@ -21,7 +21,7 @@ New coercion path [h1; f3] : B >-> C' is ambiguous with existing
 File "./output/relaxed_ambiguous_paths.v", line 33, characters 0-28:
 Warning:
 New coercion path [ab; bc] : A >-> C is ambiguous with existing 
-[ac] : A >-> C. [ambiguous-paths,typechecker,default]
+[ac] : A >-> C. [ambiguous-paths,coercions,default]
 [ab] : A >-> B
 [ac] : A >-> C
 [ac; cd] : A >-> D
@@ -31,12 +31,12 @@ New coercion path [ab; bc] : A >-> C is ambiguous with existing
 File "./output/relaxed_ambiguous_paths.v", line 50, characters 0-28:
 Warning:
 New coercion path [ab; bc] : A >-> C is ambiguous with existing 
-[ac] : A >-> C. [ambiguous-paths,typechecker,default]
+[ac] : A >-> C. [ambiguous-paths,coercions,default]
 File "./output/relaxed_ambiguous_paths.v", line 51, characters 0-28:
 Warning:
 New coercion path [ba; ab] : B >-> B is not definitionally an identity function.
 New coercion path [ab; ba] : A >-> A is not definitionally an identity function.
-[ambiguous-paths,typechecker,default]
+[ambiguous-paths,coercions,default]
 [ab] : A >-> B
 [ac] : A >-> C
 [ba] : B >-> A
@@ -58,7 +58,7 @@ New coercion path [ab; ba] : A >-> A is not definitionally an identity function.
 File "./output/relaxed_ambiguous_paths.v", line 147, characters 0-86:
 Warning:
 New coercion path [D_C; C_A'] : D >-> A' is ambiguous with existing 
-[D_B; B_A'] : D >-> A'. [ambiguous-paths,typechecker,default]
+[D_B; B_A'] : D >-> A'. [ambiguous-paths,coercions,default]
 [A'_A] : A' >-> A
 [B_A'; A'_A] : B >-> A
 [B_A'] : B >-> A'
@@ -71,12 +71,12 @@ New coercion path [D_C; C_A'] : D >-> A' is ambiguous with existing
 File "./output/relaxed_ambiguous_paths.v", line 156, characters 0-47:
 Warning:
 New coercion path [unwrap_nat; wrap_nat] : NAT >-> NAT (reversible) is not definitionally an identity function.
-[ambiguous-paths,typechecker,default]
+[ambiguous-paths,coercions,default]
 File "./output/relaxed_ambiguous_paths.v", line 157, characters 0-64:
 Warning:
 New coercion path [unwrap_list; wrap_list] : LIST >-> LIST (reversible) is not definitionally an identity function.
-[ambiguous-paths,typechecker,default]
+[ambiguous-paths,coercions,default]
 File "./output/relaxed_ambiguous_paths.v", line 158, characters 0-51:
 Warning:
 New coercion path [unwrap_Type; wrap_Type] : TYPE >-> TYPE (reversible) is not definitionally an identity function.
-[ambiguous-paths,typechecker,default]
+[ambiguous-paths,coercions,default]
diff --git a/test-suite/output/undeclared_key.out b/test-suite/output/undeclared_key.out
@@ -6,7 +6,7 @@ The command has indeed failed with message:
 There is no qualid-valued table with this name: "Search Blacklist".
 File "./output/undeclared_key.v", line 3, characters 0-22:
 Warning: There is no flag or option with this name: "Search Blacklists".
-[unknown-option,option,default]
+[unknown-option,default]
 File "./output/undeclared_key.v", line 4, characters 0-40:
 The command has indeed failed with message:
 There is no string-valued table with this name: "Search Blacklists".
diff --git a/vernac/classes.ml b/vernac/classes.ml
@@ -184,9 +184,7 @@ let add_instance cl info global impl =
   observe (Event.NewInstance { class_name = cl.cl_impl; instance = impl; info; locality = global })
 
 let warning_not_a_class =
-  let name = "not-a-class" in
-  let category = CWarnings.CoreCategories.typeclasses in
-  CWarnings.create ~name ~category (fun (n, ty) ->
+  CWarnings.create ~name:"not-a-class" (fun (n, ty) ->
       let env = Global.env () in
       let evd = Evd.from_env env in
       Pp.(str "Ignored instance declaration for “"
diff --git a/vernac/comCoercion.ml b/vernac/comCoercion.ml
@@ -296,7 +296,7 @@ lorque source est None alors target est None aussi.
 *)
 
 let warn_uniform_inheritance =
-  CWarnings.create ~name:"uniform-inheritance" ~category:CWarnings.CoreCategories.typechecker
+  CWarnings.create ~name:"uniform-inheritance" ~category:CWarnings.CoreCategories.coercions
          (fun g ->
           Printer.pr_global g ++
             strbrk" does not respect the uniform inheritance condition.")
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
@@ -29,7 +29,7 @@ module RelDecl = Context.Rel.Declaration
 (* 3b| Mutual inductive definitions *)
 
 let warn_auto_template =
-  CWarnings.create ~name:"auto-template" ~category:CWarnings.CoreCategories.vernacular ~default:CWarnings.Disabled
+  CWarnings.create ~name:"auto-template" ~default:CWarnings.Disabled
     (fun id ->
        Pp.(strbrk "Automatically declaring " ++ Id.print id ++
            strbrk " as template polymorphic. Use attributes or " ++
@@ -448,7 +448,7 @@ let split_universe_context subset (univs, csts) =
   (subset, subcst), (rem, remcst)
 
 let warn_no_template_universe =
-  CWarnings.create ~name:"no-template-universe" ~category:CWarnings.CoreCategories.universes
+  CWarnings.create ~name:"no-template-universe"
     (fun () -> Pp.str "This inductive type has no template universes.")
 
 let compute_template_inductive ~user_template ~env_ar_params ~ctx_params ~univ_entry entry concl =
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
diff --git a/vernac/loadpath.ml b/vernac/loadpath.ml
diff --git a/vernac/locality.ml b/vernac/locality.ml
diff --git a/vernac/record.ml b/vernac/record.ml
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
