Merge PR coq#18248: Generalize the deprecation machinery to other for…

…ms of comments

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

dev/ci/user-overlays/18248-herbelin-master-extend-deprecation.sh

@@ -0,0 +1 @@
+overlay elpi https://github.com/proux01/coq-elpi coq_18248 18248

doc/changelog/08-vernac-commands-and-options/18248-user_warn.rst

@@ -0,0 +1,5 @@
+- **Added:**
+  :attr:`warn` attribute generalizing the deprecation
+  machinery to other forms of comments
+  (`#18248 <https://github.com/coq/coq/pull/18248>`_,
+  by Hugo Herbelin and Pierre Roux).

doc/sphinx/language/core/assumptions.rst

@@ -170,8 +170,8 @@ has type :n:`@type`.
 
    These commands bind one or more :n:`@ident`\(s) to specified :n:`@type`\(s) as their specifications in
    the global environment. The fact asserted by :n:`@type` (or, equivalently, the existence
-   of an object of this type) is accepted as a postulate.  They accept the :attr:`program`
-   and :attr:`deprecated` attributes.
+   of an object of this type) is accepted as a postulate.  They accept the :attr:`program`,
+   :attr:`deprecated` and :attr:`warn` attributes.
 
    :cmd:`Axiom`, :cmd:`Conjecture`, :cmd:`Parameter` and their plural forms
    are equivalent.  They can take the :attr:`local` :term:`attribute`,

doc/sphinx/language/core/basic.rst

@@ -512,7 +512,8 @@ Document-level attributes
    document. When compiled with ``coqc`` (see Section
    :ref:`thecoqcommands`), the attributes are associated with the
    compiled file and may have an effect when the file is loaded with
-   :cmd:`Require`. Supported attributes include :attr:`deprecated`.
+   :cmd:`Require`. Supported attributes include :attr:`deprecated`
+   and :attr:`warn`.
 
 .. _flags-options-tables:
 

doc/sphinx/language/core/definitions.rst

@@ -100,8 +100,8 @@ Section :ref:`typing-rules`.
 
    These commands also support the :attr:`universes(polymorphic)`,
    :attr:`program` (see :ref:`program_definition`), :attr:`canonical`,
-   :attr:`bypass_check(universes)`, :attr:`bypass_check(guard)`, :attr:`deprecated` and
-   :attr:`using` attributes.
+   :attr:`bypass_check(universes)`, :attr:`bypass_check(guard)`, :attr:`deprecated`,
+   :attr:`warn` and :attr:`using` attributes.
 
    If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof mode.
    This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic.
@@ -174,7 +174,7 @@ The basic assertion command is:
    command :cmd:`Guarded`.
 
    This command accepts the :attr:`bypass_check(universes)`,
-   :attr:`bypass_check(guard)`, :attr:`deprecated`, and :attr:`using` attributes.
+   :attr:`bypass_check(guard)`, :attr:`deprecated`, :attr:`warn`, and :attr:`using` attributes.
 
    .. exn:: The term @term has type @type which should be Set, Prop or Type.
       :undocumented:

doc/sphinx/proof-engine/vernacular-commands.rst

@@ -952,6 +952,7 @@ Controlling display
    `ssr`,
    `syntax`,
    `tactics`,
+   `user-warn`,
    `vernacular`.
 
    .. This list is from lib/cWarnings.ml

doc/sphinx/using/libraries/writing.rst

@@ -21,7 +21,7 @@ deprecated compatibility alias using :cmd:`Notation (abbreviation)`
    are present, either one may appear first and they must be separated
    by a comma. If they are present, they will be used in the warning
    message, and :n:`since` will also be used in the warning name and
-   categories.
+   categories. Spaces inside :n:`since` are changed to hyphens.
 
    This attribute is supported by the following commands: :cmd:`Ltac`,
    :cmd:`Tactic Notation`, :cmd:`Notation`, :cmd:`Infix`, :cmd:`Ltac2`,
@@ -67,6 +67,43 @@ deprecated compatibility alias using :cmd:`Notation (abbreviation)`
 
    See :cite:`Zimmermann19`, Section 3.6.3, for more details.
 
+Triggering warning for library objects or library files
+-------------------------------------------------------
+
+You may use the following :term:`attribute` to trigger a warning on a
+notation, definition, axiom, theorem or file.
+
+.. attr:: warn ( note = @string , {? cats = @string } )
+   :name: warn
+
+   The :n:`note` field will be used as the warning message, and
+   :n:`cats` is a comma separated list of categories to be used in the
+   warning name and categories. Leading and trailing spaces in each
+   category are trimmed, whereas internal spaces are changed to
+   hyphens. If both :n:`note` and :n:`cats` are present, either one
+   may appear first and they must be separated by a comma.
+
+   This attribute is supported by the following commands:
+   :cmd:`Notation`, :cmd:`Infix`, :cmd:`Definition`, :cmd:`Theorem`,
+   and similar commands. To attach it to a compiled library file, use
+   :cmd:`Attributes`.
+
+   It can trigger the following warning:
+
+   .. warn:: @string__note
+
+      :n:`@string__note` is the note. It's common practice to start it
+      with a capital and end it with a period.
+
+      Explicitly :cmd:`Require`\ing a file that has a warn message set
+      using the :cmd:`Attributes` command, triggers a
+      ``warn-library-file`` warning. Requiring such a file, even
+      indirectly through a chain of :cmd:`Require`\s, will produce a
+      ``warn-transitive-library-file`` warning if the :opt:`Warnings`
+      option "warn-transitive-library-file" is set (it is
+      "-warn-transitive-library-file" by default, silencing the
+      warning).
+
 .. example:: Deprecating a tactic.
 
    .. coqtop:: all abort warn

interp/abbreviation.ml

@@ -22,7 +22,7 @@ open Notationextern
 type abbreviation =
   { abbrev_pattern : interpretation;
     abbrev_onlyparsing : bool;
-    abbrev_deprecation : Deprecation.t option;
+    abbrev_user_warns : UserWarn.t option;
     abbrev_activated : bool; (* Not really necessary in practice *)
   }
 
@@ -43,7 +43,7 @@ let toggle_abbreviation ~on ~use kn =
       | OnlyParsing | ParsingAndPrinting ->
          if on then
            begin
-             Nametab.push_abbreviation ?deprecated:data.abbrev_deprecation (Nametab.Until 1) sp kn;
+             Nametab.push_abbreviation ?user_warns:data.abbrev_user_warns (Nametab.Until 1) sp kn;
              Nametab.push_abbreviation (Nametab.Exactly 1) sp kn
            end
          else
@@ -60,7 +60,7 @@ let load_abbreviation i ((sp,kn),(_local,abbrev)) =
     user_err
       (Id.print (basename sp) ++ str " already exists.");
   add_abbreviation kn sp abbrev;
-  Nametab.push_abbreviation ?deprecated:abbrev.abbrev_deprecation (Nametab.Until i) sp kn
+  Nametab.push_abbreviation ?user_warns:abbrev.abbrev_user_warns (Nametab.Until i) sp kn
 
 let is_alias_of_already_visible_name sp = function
   | _,NRef (ref,None) ->
@@ -102,11 +102,11 @@ let inAbbreviation : Id.t -> (bool * abbreviation) -> obj =
     subst_function = subst_abbreviation;
     classify_function = classify_abbreviation }
 
-let declare_abbreviation ~local deprecation id ~onlyparsing pat =
+let declare_abbreviation ~local user_warns id ~onlyparsing pat =
   let abbrev =
     { abbrev_pattern = pat;
       abbrev_onlyparsing = onlyparsing;
-      abbrev_deprecation = deprecation;
+      abbrev_user_warns = user_warns;
       abbrev_activated = true;
     }
   in

interp/abbreviation.mli

@@ -15,7 +15,7 @@ open Globnames
 
 (** Abbreviations. *)
 
-val declare_abbreviation : local:bool -> Deprecation.t option -> Id.t ->
+val declare_abbreviation : local:bool -> UserWarn.t option -> Id.t ->
   onlyparsing:bool -> interpretation -> unit
 
 val search_abbreviation : abbreviation -> interpretation

interp/constrintern.ml

@@ -1383,7 +1383,7 @@ let intern_qualid_for_pattern test_global intern_not qid pats =
   match Nametab.locate_extended_nowarn qid with
   | TrueGlobal g as xref ->
     test_global g;
-    Nametab.is_deprecated_xref xref |> Option.iter (fun depr -> Nametab.warn_deprecated_xref ?loc:qid.loc depr (TrueGlobal g));
+    Nametab.is_warned_xref xref |> Option.iter (fun warn -> Nametab.warn_user_warn_xref ?loc:qid.loc warn (TrueGlobal g));
     dump_extended_global qid.loc (TrueGlobal g);
     (g, false, Some [], pats)
   | Abbrev kn as xref ->
@@ -1410,8 +1410,8 @@ let intern_qualid_for_pattern test_global intern_not qid pats =
       | _ -> None in
     match Abbreviation.search_filtered_abbreviation filter kn with
     | Some (g, pats1, pats2) ->
-      Nametab.is_deprecated_xref xref
-      |> Option.iter (fun depr -> Nametab.warn_deprecated_xref ?loc:qid.loc depr (Abbrev kn));
+      Nametab.is_warned_xref xref
+      |> Option.iter (fun warn -> Nametab.warn_user_warn_xref ?loc:qid.loc warn (Abbrev kn));
       dump_extended_global qid.loc (Abbrev kn);
       (g, true, pats1, pats2)
     | None -> raise Not_found

interp/notation.ml

@@ -81,7 +81,7 @@ type notation_location = (DirPath.t * DirPath.t) * string
 type notation_data = {
   not_interp : interpretation;
   not_location : notation_location;
-  not_deprecation : Deprecation.t option;
+  not_user_warns : UserWarn.t option;
 }
 
 type activation = bool
@@ -1413,8 +1413,8 @@ let warn_deprecation_overridden =
 let warn_override_if_needed (scopt,ntn) overridden data old_data =
   if overridden then warn_notation_overridden (scopt,ntn)
   else
-    if data.not_deprecation <> old_data.not_deprecation then
-      warn_deprecation_overridden ((scopt,ntn),old_data.not_deprecation,data.not_deprecation)
+    if data.not_user_warns <> old_data.not_user_warns then
+      warn_deprecation_overridden ((scopt,ntn),old_data.not_user_warns,data.not_user_warns)
 
 let check_parsing_override (scopt,ntn) data = function
   | OnlyParsingData (_,old_data) ->
@@ -1436,8 +1436,8 @@ let check_printing_override (scopt,ntn) data parsingdata printingdata =
     if overridden then NoParsingData else parsingdata in
   let exists = List.exists (fun (on_printing,old_data) ->
     let exists = interpretation_eq data.not_interp old_data.not_interp in
-    if exists && data.not_deprecation <> old_data.not_deprecation then
-      warn_deprecation_overridden ((scopt,ntn),old_data.not_deprecation,data.not_deprecation);
+    if exists && data.not_user_warns <> old_data.not_user_warns then
+      warn_deprecation_overridden ((scopt,ntn),old_data.not_user_warns,data.not_user_warns);
     exists) printingdata in
   parsing_update, exists
 
@@ -1529,7 +1529,7 @@ let interp_notation ?loc ntn local_scopes =
   let scopes = make_current_scopes local_scopes in
   try
     let (n,sc) = find_interpretation ntn (find_notation ntn) scopes in
-    Option.iter (fun d -> warn_deprecated_notation ?loc (ntn,d)) n.not_deprecation;
+    Option.iter (fun d -> Option.iter (fun d -> warn_deprecated_notation ?loc (ntn,d)) d.UserWarn.depr) n.not_user_warns;
     n.not_interp, (n.not_location, sc)
   with Not_found as exn ->
     let _, info = Exninfo.capture exn in
@@ -1720,14 +1720,14 @@ type entry_coercion_kind =
   | IsEntryGlobal of string * int
   | IsEntryIdent of string * int
 
-let declare_notation (scopt,ntn) pat df ~use coe deprecation =
+let declare_notation (scopt,ntn) pat df ~use coe user_warns =
   (* Register the interpretation *)
   let scope = match scopt with NotationInScope s -> s | LastLonelyNotation -> default_scope in
   let sc = find_scope scope in
   let notdata = {
     not_interp = pat;
     not_location = df;
-    not_deprecation = deprecation;
+    not_user_warns = user_warns;
   } in
   let notation_update,printing_update = update_notation_data (scopt,ntn) use notdata sc.notations in
   let sc = { sc with notations = notation_update } in
@@ -2705,7 +2705,7 @@ let toggle_notations ~on ~all ?(verbose=true) prglob ntn_pattern =
             match kind with
             | Inl (l, (sc, (entry, _))) ->
               let sc = match sc with NotationInScope sc -> sc | LastLonelyNotation -> default_scope in
-              let data = { not_interp = i; not_location = l; not_deprecation = None } in
+              let data = { not_interp = i; not_location = l; not_user_warns = None } in
               hov 0 (str "Notation " ++ pr_notation_data prglob (Some true,Some true,data) ++
               (match entry with InCustomEntry s -> str " (in custom " ++ str s ++ str ")" | _ -> mt ()) ++
               (if String.equal sc default_scope then mt () else (brk (1,2) ++ str ": " ++ str sc)))

interp/notation.mli

@@ -251,7 +251,7 @@ type entry_coercion_kind =
 val declare_notation : notation_with_optional_scope * notation ->
   interpretation -> notation_location -> use:notation_use ->
   entry_coercion_kind option ->
-  Deprecation.t option -> unit
+  UserWarn.t option -> unit
 
 
 (** Return the interpretation bound to a notation *)

lib/cWarnings.ml

@@ -432,6 +432,7 @@ module CoreCategories = struct
   let ssr = make "ssr"
   let syntax = make "syntax"
   let tactics = make "tactics"
+  let user_warn = make "user-warn"
   let vernacular = make "vernacular"
 
 end

lib/cWarnings.mli

@@ -121,6 +121,7 @@ module CoreCategories : sig
   val ssr : category
   val syntax : category
   val tactics : category
+  val user_warn : category
   val vernacular : category
 
 end

lib/userWarn.ml

@@ -0,0 +1,58 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** This is about warnings triggered from user .v code ("warn" attibute).
+    See cWarnings.mli for the generic warning interface. *)
+
+type warn = { note : string; cats : string }
+(** note and comma separated list of categories *)
+
+type t = { depr : Deprecation.t option; warn : warn list }
+
+let empty = { depr = None; warn = [] }
+
+let make_warn ~note ?cats () =
+  let l = String.split_on_char ',' (Option.default "" cats) in
+  let l =
+    List.map String.(fun s -> map (function ' ' -> '-' | c -> c) (trim s)) l in
+  let l = List.sort String.compare l in
+  { note; cats = String.concat "," l }
+
+let user_warn_cat = CWarnings.CoreCategories.user_warn
+
+let warn_cats = ref CString.Map.empty
+
+let get_generic_cat cat =
+  match CString.Map.find_opt cat !warn_cats with
+  | Some c -> c
+  | None ->
+    let c = CWarnings.create_category ~from:[user_warn_cat] ~name:cat () in
+    warn_cats := CString.Map.add cat c !warn_cats;
+    c
+
+let create_warning ?default ~warning_name_if_no_cats () =
+  let main_cat, main_w = CWarnings.create_hybrid ?default ~name:warning_name_if_no_cats ~from:[user_warn_cat] () in
+  let main_w = CWarnings.create_in main_w Pp.strbrk in
+  let warnings = ref CString.Map.empty in
+  fun ?loc {note;cats} ->
+    let w =
+      if cats = "" then main_w else
+        match CString.Map.find_opt cats !warnings with
+        | Some w -> w
+        | None ->
+           let l = String.split_on_char ',' cats in
+           let generic_cats = List.map get_generic_cat l in
+           let w = CWarnings.create_warning ?default ~from:(main_cat :: generic_cats)
+               ~name:(String.concat "-" (warning_name_if_no_cats :: l)) () in
+           let w = CWarnings.create_in w Pp.strbrk in
+           warnings := CString.Map.add cats w !warnings;
+           w
+    in
+    w ?loc note

lib/userWarn.mli

@@ -0,0 +1,24 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** This is about warnings triggered from user .v code ("warn" attibute).
+    See cWarnings.mli for the generic warning interface. *)
+
+type warn = private { note : string; cats : string }
+(** note and comma separated list of categories *)
+
+type t = { depr : Deprecation.t option; warn : warn list }
+
+val empty : t
+
+val make_warn : note:string -> ?cats:string -> unit -> warn
+
+val create_warning : ?default:CWarnings.status -> warning_name_if_no_cats:string ->
+  unit -> ?loc:Loc.t -> warn -> unit

library/lib.ml

@@ -132,7 +132,7 @@ let dummy = {
 let synterp_state = ref dummy
 let interp_state = ref ([] : Summary.Interp.frozen library_segment)
 
-let library_info = ref []
+let library_info = ref UserWarn.empty
 
 let contents () = !interp_state
 
@@ -348,7 +348,7 @@ module type LibActions = sig
 
   val drop_objects : frozen -> frozen
 
-  val declare_info : Library_info.t list -> unit
+  val declare_info : Library_info.t -> unit
 
 end
 
@@ -437,7 +437,14 @@ module SynterpActions : LibActions with type summary = Summary.Synterp.frozen =
     let lib_synterp_stk = List.map (fun (node,_) -> drop_node node, []) st.lib_stk in
     { st with lib_stk = lib_synterp_stk }
 
-  let declare_info info = library_info := !library_info @ info
+  let declare_info info =
+    let open UserWarn in
+    let depr = match !library_info.depr, info.depr with
+      | None, depr | depr, None -> depr
+      | Some _, Some _ ->
+         CErrors.user_err Pp.(str "Library file is already deprecated.") in
+    let warn = !library_info.warn @ info.warn in
+    library_info := { depr; warn }
 
 end
 
@@ -572,7 +579,7 @@ module type StagedLibS = sig
 
   val drop_objects : frozen -> frozen
 
-  val declare_info : Library_info.t list -> unit
+  val declare_info : Library_info.t -> unit
 
 end