Merge PR #17747: Warn when trying to enable an unknown warning

Reviewed-by: gares
Ack-by: Matafou
Co-authored-by: gares <[email protected]>

Author: coqbot-app[bot]

doc/changelog/08-vernac-commands-and-options/17747-warn-unknown-warn.rst

@@ -0,0 +1,8 @@
+- **Changed:**
+  :opt:`Warnings` and :attr:`warnings` now emit a warning when trying
+  to enable an unknown warning (there is still no warning when
+  disabling an unknown warning as this behavior is useful for
+  compatibility, or when enabling an unknown warning through the
+  command line `-w` as the warning may be in a yet to be loaded
+  plugin) (`#17747 <https://github.com/coq/coq/pull/17747>`_, by
+  Gaëtan Gilbert).

lib/cWarnings.ml

@@ -382,6 +382,28 @@ let create ~name ?category ?default pp =
   let w = create_warning ?from ?default ~name () in
   create_in w pp
 
+let warn_unknown_warnings = create ~name:"unknown-warning" Pp.(fun flags ->
+    str "Could not enable unknown " ++
+    str (CString.plural (List.length flags) "warning") ++ spc() ++
+    prlist_with_sep spc str flags)
+
+let override_unknown_warning = ref false
+
+let warn_unknown_warnings ?loc flags =
+  if not !override_unknown_warning then warn_unknown_warnings ?loc flags
+
+let check_unknown_warnings flags =
+  let flags = flags_of_string flags in
+  let flags = List.filter_map (function
+      | Disabled, _ | _, All -> None
+      | (Enabled|AsError), Other name ->
+        if String.Map.mem name !graph then None
+        else Some name)
+      flags
+  in
+  if not (List.is_empty flags) then
+    warn_unknown_warnings flags
+
 module CoreCategories = struct
 
   let make name = create_category ~name ()

lib/cWarnings.mli

@@ -89,6 +89,15 @@ val with_warn: string -> ('b -> 'a) -> 'b -> 'a
    raises an exception. If both f and restoring the warnings raise
    exceptions, the latter is raised. *)
 
+val check_unknown_warnings : string -> unit
+(** Warn with "unknown-warning" if any unknown warnings are in the
+    string with non-disabled status. *)
+
+val override_unknown_warning : bool ref
+[@@ocaml.deprecated "Do not use, internal."]
+(** For command line -w, this avoids using the warning system to avoid breaking
+    "-w -unknown-warning". *)
+
 module CoreCategories : sig
   (** Categories used in coq-core. Might not be exhaustive. *)
 

plugins/funind/g_indfun.mlg

@@ -209,7 +209,7 @@ VERNAC COMMAND EXTEND Function STATE CUSTOM
 | ["Function" ne_function_fix_definition_list_sep(recsl,"with")]
     => { classify_funind recsl }
     -> {
-    let warn = "-unused-pattern-matching-variable,-matching-variable,-non-recursive" in
+    let warn = "-unused-pattern-matching-variable,-non-recursive" in
     if is_interactive recsl then
       Vernacextend.vtopenproof (fun () ->
           CWarnings.with_warn warn

sysinit/coqinit.ml

@@ -195,4 +195,6 @@ let handle_injection = let open Coqargs in function
 
 let start_library ~top injections =
   Flags.verbosely Declaremods.start_library top;
-  List.iter handle_injection injections
+  CWarnings.override_unknown_warning[@ocaml.warning "-3"] := true;
+  List.iter handle_injection injections;
+  CWarnings.override_unknown_warning[@ocaml.warning "-3"] := false

test-suite/output/Function.out

@@ -0,0 +1,3 @@
+File "./output/Function.v", line 28, characters 4-5:
+Warning: Unused variable n might be a misspelled constructor. Use _ or _n to
+silence this warning. [unused-pattern-matching-variable,default]

test-suite/output/Function.v

@@ -21,11 +21,17 @@ Fixpoint f (l:list nat) : nat :=
    test would then need to be updated. *)
 
 (* Ensuring the warning is a warning. *)
-Set Warnings "matching-variable".
-(* But no warning generated here. *)
-Function f (l:list nat) : nat :=
+Fixpoint f (l:list nat) : nat :=
   match l with
   | nil => O
   | S n :: nil  => 1
   | n :: l'  => f l'
   end.
+
+(* But no warning generated here. *)
+Function g (l:list nat) : nat :=
+  match l with
+  | nil => O
+  | S n :: nil  => 1
+  | n :: l'  => g l'
+  end.

test-suite/success/unknown_warning.v

@@ -0,0 +1,17 @@
+Set Warnings "+unknown-warning".
+
+Set Warnings "-foo".
+Fail Set Warnings "foo".
+Fail Set Warnings "+foo".
+
+#[warnings="-foo"] Check True.
+Fail #[warnings="foo"] Check True.
+
+(* debatable: even though "all" overrides "+foo" we still warn *)
+Fail Set Warnings "+foo,-all".
+
+(* debatable: changing unknown-warning has no effect for the current check *)
+Fail Set Warnings "-unknown-warning,foo".
+Fail #[warnings="-unknown-warning,foo"] Check True.
+Set Warnings "-unknown-warning".
+#[warnings="+unknown-warning,foo"] Check True.

vernac/vernacentries.ml

@@ -1763,7 +1763,11 @@ let () =
       optwrite = (fun b ->  Constrintern.parsing_explicit := b) }
 
 let () =
-  declare_string_option ~preprocess:CWarnings.normalize_flags_string
+  let preprocess flags =
+    CWarnings.check_unknown_warnings flags;
+    CWarnings.normalize_flags_string flags
+  in
+  declare_string_option ~preprocess
     { optstage = Summary.Stage.Interp;
       optdepr  = None;
       optkey   = ["Warnings"];

vernac/vernacinterp.ml

@@ -126,7 +126,9 @@ let with_generic_atts atts f =
       Some (match warnings with Some w -> w ^ "," ^ ui | None -> ui) in
   match warnings with
   | None -> f ~atts
-  | Some warnings -> CWarnings.with_warn warnings (fun () -> f ~atts) ()
+  | Some warnings ->
+    CWarnings.check_unknown_warnings warnings;
+    CWarnings.with_warn warnings (fun () -> f ~atts) ()
 
 (* "locality" is the prefix "Local" attribute, while the "local" component
  * is the outdated/deprecated "Local" attribute of some vernacular commands