Merge pull request #589 from proux01/coq_18248

Adapt to coq/coq#18248

Changelog.md

@@ -1,5 +1,13 @@
 # Changelog
 
+## Unreleased
+
+- New option `@warn! Cats Message`.
+  In order to pass a warn directive one has to do something like
+    `@warn! "cata, catb, catc" "Beware of foo." => coq.add-something`
+  Deprecation is understood by:
+  - `coq.notation.add-abbreviation`
+
 ## [2.0.1] - 24/12/2023
 
 Requires Elpi 1.18.1 and Coq 8.19.

coq-builtin.elpi

@@ -490,6 +490,10 @@ macro @redflags! F :- get-option "coq:redflags" F. % for whd & co
 macro @deprecated! Since Msg :-
   get-option "coq:deprecated" (pr Since Msg).
 
+% both arguments are strings eg "cata, catb, catc" "Beware of foo."
+macro @warn! Cats Msg :-
+  get-option "coq:warn" (pr Cats Msg).
+
 macro @ltacfail! N :- get-option "ltac:fail" N.
 
 % retrocompatibility macro for Coq v8.10
@@ -1346,6 +1350,7 @@ typeabbrev abbreviation (ctype "abbreviation").
 % ignored, eg (fun _ _ x\ fun _ _ y\ app[global "add",x,y]).
 % Supported attributes:
 % - @deprecated! (default: not deprecated)
+% - @warn! (default: no warning)
 % - @global! (default: false)
 external pred coq.notation.add-abbreviation i:id, i:int, i:term, i:bool, 
                                             o:abbreviation.

elpi/coq-HOAS.elpi

@@ -339,6 +339,10 @@ macro @redflags! F :- get-option "coq:redflags" F. % for whd & co
 macro @deprecated! Since Msg :-
   get-option "coq:deprecated" (pr Since Msg).
 
+% both arguments are strings eg "cata, catb, catc" "Beware of foo."
+macro @warn! Cats Msg :-
+  get-option "coq:warn" (pr Cats Msg).
+
 macro @ltacfail! N :- get-option "ltac:fail" N.
 
 % retrocompatibility macro for Coq v8.10

src/coq_elpi_HOAS.ml

@@ -333,7 +333,7 @@ type universe_decl_option =
 type options = {
   hoas_holes : hole_mapping option;
   local : bool option;
-  deprecation : Deprecation.t option;
+  user_warns : UserWarn.t option;
   primitive : bool option;
   failsafe : bool; (* don't fail, e.g. we are trying to print a term *)
   ppwidth : int;
@@ -352,7 +352,7 @@ type options = {
 let default_options () = {
   hoas_holes = Some Verbatim;
   local = None;
-  deprecation = None;
+  user_warns = None;
   primitive = None;
   failsafe = false;
   ppwidth = Option.default 80 (Topfmt.get_margin ());
@@ -1127,6 +1127,12 @@ let get_options ~depth hyps state =
         let since = unspec2opt since |> empty2none in
         let note = unspec2opt note |> empty2none in
         Some { Deprecation.since; note } in
+  let warn = function
+    | None -> []
+    | Some(cats,note) ->
+        let cats = unspec2opt cats |> empty2none in
+        let note = unspec2opt note |> empty2none in
+        Option.cata (fun note -> [UserWarn.make_warn ~note ?cats ()]) [] note in
   let get_universe_decl () =
     match API.Data.StrMap.find_opt "coq:udecl-cumul" map, API.Data.StrMap.find_opt "coq:udecl" map with
     | None, None -> NotUniversePolymorphic
@@ -1154,7 +1160,12 @@ let get_options ~depth hyps state =
       | Some true -> Some Heuristic
       | Some false -> Some Verbatim end;
     local = locality @@ get_string_option "coq:locality";
-    deprecation = deprecation @@ get_pair_option API.BuiltInData.string API.BuiltInData.string "coq:deprecation";
+    user_warns =
+      begin
+        let depr = deprecation @@ get_pair_option API.BuiltInData.string API.BuiltInData.string "coq:deprecated" in
+        let warn = warn @@ get_pair_option API.BuiltInData.string API.BuiltInData.string "coq:warn" in
+        Some UserWarn.{ depr; warn }
+      end;
     primitive = get_bool_option "coq:primitive";
     failsafe = false;
     ppwidth = ppwidth @@ get_int_option "coq:ppwidth";

src/coq_elpi_HOAS.mli

@@ -33,7 +33,7 @@ type universe_decl_option =
 type options = {
   hoas_holes : hole_mapping option;
   local : bool option;
-  deprecation : Deprecation.t option;
+  user_warns : UserWarn.t option;
   primitive : bool option;
   failsafe : bool; (* readback is resilient to illformed terms *)
   ppwidth : int;

src/coq_elpi_builtins.ml

@@ -2994,6 +2994,7 @@ Supported attributes:
 The term must begin with at least Nargs "fun" nodes whose domain is ignored, eg (fun _ _ x\ fun _ _ y\ app[global "add",x,y]).
 Supported attributes:
 - @deprecated! (default: not deprecated)
+- @warn! (default: no warning)
 - @global! (default: false)|})))))),
   (fun name nargs term onlyparsing _ ~depth { env; options } _ -> grab_global_env "coq.notation.add-abbreviation" (fun state ->
        let sigma = get_sigma state in
@@ -3036,7 +3037,7 @@ Supported attributes:
      let vars, nenv, env, body = strip_n_lambas nargs env term in
      let gbody = Coq_elpi_utils.detype env sigma body in
      let pat, _ = Notation_ops.notation_constr_of_glob_constr nenv gbody in
-     Abbreviation.declare_abbreviation ~local ~onlyparsing options.deprecation name (vars,pat);
+     Abbreviation.declare_abbreviation ~local ~onlyparsing options.user_warns name (vars,pat);
      let qname = Libnames.qualid_of_string (Id.to_string name) in
      match Nametab.locate_extended qname with
      | Globnames.TrueGlobal _ -> assert false