Merge PR #13774: Allow to register deprecation status in Ltac2 term and notation declarations

Reviewed-by: JasonGross
Reviewed-by: Zimmi48
Ack-by: jfehrle

11 files changed, 162 insertions, 35 deletions

diff --git a/doc/changelog/05-tactic-language/13774-ltac2-deprecated-attribute-term.rst b/doc/changelog/05-tactic-language/13774-ltac2-deprecated-attribute-term.rst
new file mode 100644
index 0000000000..5fdfbd9796
--- /dev/null
+++ b/doc/changelog/05-tactic-language/13774-ltac2-deprecated-attribute-term.rst
@@ -0,0 +1,6 @@
+- **Added:**
+  Ltac2 commands defining terms now accept the :attr:`deprecated`
+  attribute
+  (`#13774 <https://github.com/coq/coq/pull/13774>`_,
+  fixes `#12317 <https://github.com/coq/coq/issues/12317>`_,
+  by Pierre-Marie Pédrot).
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index 146da8bb37..294c56ef06 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -66,7 +66,6 @@ Current limitations include:
   - An easy way to get the number of constructors of an inductive type.
     Currently only way to do this is to destruct a variable of the inductive type
     and count the number of goals that result.
-- The :attr:`deprecated` attribute is not supported for Ltac2 definitions.
 
 - Error messages may be cryptic.
 
@@ -229,6 +228,8 @@ One can define new types with the following commands.
    defined in Coq and give their type information.  They can also declare
    data structures from OCaml.  This command has no use for the end user.
 
+   This command supports the :attr:`deprecated` attribute.
+
 APIs
 ~~~~
 
@@ -319,6 +320,8 @@ Ltac2 Definitions
 
    If ``mutable`` is set, the definition can be redefined at a later stage (see below).
 
+   This command supports the :attr:`deprecated` attribute.
+
 .. cmd:: Ltac2 Set @qualid {? as @ident } := @ltac2_expr
 
    This command redefines a previous ``mutable`` definition.
@@ -1246,6 +1249,8 @@ Notations
       so that you may have to resort to thunking to ensure that side-effects are
       performed at the right time.
 
+   This command supports the :attr:`deprecated` attribute.
+
 Abbreviations
 ~~~~~~~~~~~~~
 
@@ -1276,6 +1281,8 @@ Abbreviations
    Note that abbreviations are not type checked at all, and may result in typing
    errors after expansion.
 
+   This command supports the :attr:`deprecated` attribute.
+
 .. _defining_tactics:
 
 Defining tactics
diff --git a/doc/sphinx/using/libraries/writing.rst b/doc/sphinx/using/libraries/writing.rst
index 917edf0774..7461bfe443 100644
--- a/doc/sphinx/using/libraries/writing.rst
+++ b/doc/sphinx/using/libraries/writing.rst
@@ -22,13 +22,17 @@ deprecated compatibility alias using :cmd:`Notation (abbreviation)`
    by a comma.
 
    This attribute is supported by the following commands: :cmd:`Ltac`,
-   :cmd:`Tactic Notation`, :cmd:`Notation`, :cmd:`Infix`.
+   :cmd:`Tactic Notation`, :cmd:`Notation`, :cmd:`Infix`, :cmd:`Ltac2`,
+   :cmd:`Ltac2 Notation`, :cmd:`Ltac2 external`.
 
    It can trigger the following warnings:
 
    .. warn:: Tactic @qualid is deprecated since @string__since. @string__note.
              Tactic Notation @qualid is deprecated since @string__since. @string__note.
              Notation @string is deprecated since @string__since. @string__note.
+             Ltac2 definition @qualid is deprecated since @string__since. @string__note.
+             Ltac2 alias @qualid is deprecated since @string__since. @string__note.
+             Ltac2 notation {+ @ltac2_scope } is deprecated since @string__since. @string__note.
 
       :n:`@qualid` or :n:`@string` is the notation,
       :n:`@string__since` is the version number, :n:`@string__note` is
diff --git a/test-suite/output/ltac2_deprecated.out b/test-suite/output/ltac2_deprecated.out
new file mode 100644
index 0000000000..d17b719bcd
--- /dev/null
+++ b/test-suite/output/ltac2_deprecated.out
@@ -0,0 +1,12 @@
+File "stdin", line 13, characters 11-14:
+Warning: Ltac2 definition foo is deprecated. test_definition
+[deprecated-ltac2-definition,deprecated]
+- : unit = ()
+File "stdin", line 14, characters 11-14:
+Warning: Ltac2 alias bar is deprecated. test_notation
+[deprecated-ltac2-alias,deprecated]
+- : unit = ()
+File "stdin", line 15, characters 11-14:
+Warning: Ltac2 definition qux is deprecated. test_external
+[deprecated-ltac2-definition,deprecated]
+- : 'a array -> int = <fun>
diff --git a/test-suite/output/ltac2_deprecated.v b/test-suite/output/ltac2_deprecated.v
new file mode 100644
index 0000000000..9598a5979c
--- /dev/null
+++ b/test-suite/output/ltac2_deprecated.v
@@ -0,0 +1,15 @@
+Require Import Ltac2.Ltac2.
+
+#[deprecated(note="test_definition")]
+Ltac2 foo := ().
+
+#[deprecated(note="test_notation")]
+Ltac2 Notation bar := ().
+
+#[deprecated(note="test_external")]
+Ltac2 @ external qux : 'a array -> int := "ltac2" "array_length".
+(* Randomly picked external function *)
+
+Ltac2 Eval foo.
+Ltac2 Eval bar.
+Ltac2 Eval qux.
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index 5297409cdf..4ef5c1a918 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -915,8 +915,8 @@ let classify_ltac2 = function
 }
 
 VERNAC COMMAND EXTEND VernacDeclareTactic2Definition
-| #[ local = locality ] [ "Ltac2" ltac2_entry(e) ] => { classify_ltac2 e } -> {
-  Tac2entries.register_struct ?local e
+| #[ deprecation = deprecation; local = locality ] [ "Ltac2" ltac2_entry(e) ] => { classify_ltac2 e } -> {
+  Tac2entries.register_struct ?deprecation ?local e
   }
 | ![proof_opt_query] [ "Ltac2" "Eval" ltac2_expr(e) ] => { Vernacextend.classify_as_sideeff } -> {
   fun ~pstate -> Tac2entries.perform_eval ~pstate e
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index faa1e74728..0aa05934bf 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -57,6 +57,7 @@ type tacdef = {
   tacdef_mutable : bool;
   tacdef_expr : glb_tacexpr;
   tacdef_type : type_scheme;
+  tacdef_deprecation : Deprecation.t option;
 }
 
 let perform_tacdef visibility ((sp, kn), def) =
@@ -65,6 +66,7 @@ let perform_tacdef visibility ((sp, kn), def) =
     Tac2env.gdata_expr = def.tacdef_expr;
     gdata_type = def.tacdef_type;
     gdata_mutable = def.tacdef_mutable;
+    gdata_deprecation = def.tacdef_deprecation;
   } in
   Tac2env.define_global kn data
 
@@ -77,6 +79,7 @@ let cache_tacdef ((sp, kn), def) =
     Tac2env.gdata_expr = def.tacdef_expr;
     gdata_type = def.tacdef_type;
     gdata_mutable = def.tacdef_mutable;
+    gdata_deprecation = def.tacdef_deprecation;
   } in
   Tac2env.define_global kn data
 
@@ -322,7 +325,7 @@ let check_lowercase {loc;v=id} =
   if Tac2env.is_constructor (Libnames.qualid_of_ident id) then
     user_err ?loc (str "The identifier " ++ Id.print id ++ str " must be lowercase")
 
-let register_ltac ?(local = false) ?(mut = false) isrec tactics =
+let register_ltac ?deprecation ?(local = false) ?(mut = false) isrec tactics =
   let map ({loc;v=na}, e) =
     let id = match na with
     | Anonymous ->
@@ -359,6 +362,7 @@ let register_ltac ?(local = false) ?(mut = false) isrec tactics =
       tacdef_mutable = mut;
       tacdef_expr = e;
       tacdef_type = t;
+      tacdef_deprecation = deprecation;
     } in
     ignore (Lib.add_leaf id (inTacDef def))
   in
@@ -453,7 +457,7 @@ let register_typedef ?(local = false) isrec types =
   let iter (id, def) = ignore (Lib.add_leaf id (inTypDef def)) in
   List.iter iter types
 
-let register_primitive ?(local = false) {loc;v=id} t ml =
+let register_primitive ?deprecation ?(local = false) {loc;v=id} t ml =
   let t = intern_open_type t in
   let rec count_arrow = function
   | GTypArrow (_, t) -> 1 + count_arrow t
@@ -477,6 +481,7 @@ let register_primitive ?(local = false) {loc;v=id} t ml =
     tacdef_mutable = false;
     tacdef_expr = e;
     tacdef_type = t;
+    tacdef_deprecation = deprecation;
   } in
   ignore (Lib.add_leaf id (inTacDef def))
 
@@ -599,6 +604,18 @@ let parse_token = function
   let loc = loc_of_token tok in
   CErrors.user_err ?loc (str "Invalid parsing token")
 
+let rec print_scope = function
+| SexprStr s -> str s.CAst.v
+| SexprInt i -> int i.CAst.v
+| SexprRec (_, {v=na}, []) -> Option.cata Id.print (str "_") na
+| SexprRec (_, {v=na}, e) ->
+  Option.cata Id.print (str "_") na ++ str "(" ++ pr_sequence print_scope e ++ str ")"
+
+let print_token = function
+| SexprStr {v=s} -> quote (str s)
+| SexprRec (_, {v=na}, [tok]) -> print_scope tok
+| _ -> assert false
+
 end
 
 let parse_scope = ParseToken.parse_scope
@@ -608,6 +625,7 @@ type synext = {
   synext_exp : raw_tacexpr;
   synext_lev : int option;
   synext_loc : bool;
+  synext_depr : Deprecation.t option;
 }
 
 type krule =
@@ -628,10 +646,20 @@ let rec get_rule (tok : scope_rule token list) : krule = match tok with
   let act k _ = act k in
   KRule (rule, act)
 
+let deprecated_ltac2_notation =
+  Deprecation.create_warning
+    ~object_name:"Ltac2 notation"
+    ~warning_name:"deprecated-ltac2-notation"
+    (fun (toks : sexpr list) -> pr_sequence ParseToken.print_token toks)
+
 let perform_notation syn st =
   let tok = List.rev_map ParseToken.parse_token syn.synext_tok in
   let KRule (rule, act) = get_rule tok in
   let mk loc args =
+    let () = match syn.synext_depr with
+    | None -> ()
+    | Some depr -> deprecated_ltac2_notation ~loc (syn.synext_tok, depr)
+    in
     let map (na, e) =
       ((CAst.make ?loc:e.loc @@ CPatVar na), e)
     in
@@ -671,23 +699,24 @@ let inTac2Notation : synext -> obj =
 
 type abbreviation = {
   abbr_body : raw_tacexpr;
+  abbr_depr : Deprecation.t option;
 }
 
 let perform_abbreviation visibility ((sp, kn), abbr) =
   let () = Tac2env.push_ltac visibility sp (TacAlias kn) in
-  Tac2env.define_alias kn abbr.abbr_body
+  Tac2env.define_alias ?deprecation:abbr.abbr_depr kn abbr.abbr_body
 
 let load_abbreviation i obj = perform_abbreviation (Until i) obj
 let open_abbreviation i obj = perform_abbreviation (Exactly i) obj
 
 let cache_abbreviation ((sp, kn), abbr) =
   let () = Tac2env.push_ltac (Until 1) sp (TacAlias kn) in
-  Tac2env.define_alias kn abbr.abbr_body
+  Tac2env.define_alias ?deprecation:abbr.abbr_depr kn abbr.abbr_body
 
 let subst_abbreviation (subst, abbr) =
   let body' = subst_rawexpr subst abbr.abbr_body in
   if body' == abbr.abbr_body then abbr
-  else { abbr_body = body' }
+  else { abbr_body = body'; abbr_depr = abbr.abbr_depr }
 
 let classify_abbreviation o = Substitute o
 
@@ -699,12 +728,12 @@ let inTac2Abbreviation : abbreviation -> obj =
      subst_function = subst_abbreviation;
      classify_function = classify_abbreviation}
 
-let register_notation ?(local = false) tkn lev body = match tkn, lev with
+let register_notation ?deprecation ?(local = false) tkn lev body = match tkn, lev with
 | [SexprRec (_, {loc;v=Some id}, [])], None ->
   (* Tactic abbreviation *)
   let () = check_lowercase CAst.(make ?loc id) in
   let body = Tac2intern.globalize Id.Set.empty body in
-  let abbr = { abbr_body = body } in
+  let abbr = { abbr_body = body; abbr_depr = deprecation } in
   ignore (Lib.add_leaf id (inTac2Abbreviation abbr))
 | _ ->
   (* Check that the tokens make sense *)
@@ -723,6 +752,7 @@ let register_notation ?(local = false) tkn lev body = match tkn, lev with
     synext_exp = body;
     synext_lev = lev;
     synext_loc = local;
+    synext_depr = deprecation;
   } in
   Lib.add_anonymous_leaf (inTac2Notation ext)
 
@@ -838,12 +868,21 @@ let perform_eval ~pstate e =
 
 (** Toplevel entries *)
 
-let register_struct ?local str = match str with
-| StrVal (mut, isrec, e) -> register_ltac ?local ~mut isrec e
-| StrTyp (isrec, t) -> register_type ?local isrec t
-| StrPrm (id, t, ml) -> register_primitive ?local id t ml
-| StrSyn (tok, lev, e) -> register_notation ?local tok lev e
-| StrMut (qid, old, e) -> register_redefinition ?local qid old e
+let unsupported_deprecation = function
+| None -> ()
+| Some _ ->
+  Attributes.unsupported_attributes ["deprecated", Attributes.VernacFlagEmpty]
+
+let register_struct ?deprecation ?local str = match str with
+| StrVal (mut, isrec, e) -> register_ltac ?deprecation ?local ~mut isrec e
+| StrTyp (isrec, t) ->
+  let () = unsupported_deprecation deprecation in (* TODO *)
+  register_type ?local isrec t
+| StrPrm (id, t, ml) -> register_primitive ?deprecation ?local id t ml
+| StrSyn (tok, lev, e) -> register_notation ?deprecation ?local tok lev e
+| StrMut (qid, old, e) ->
+  let () = unsupported_deprecation deprecation in (* TODO: what does that mean? *)
+  register_redefinition ?local qid old e
 
 (** Toplevel exception *)
 
diff --git a/user-contrib/Ltac2/tac2entries.mli b/user-contrib/Ltac2/tac2entries.mli
index 782968c6e1..a1e13b60fe 100644
--- a/user-contrib/Ltac2/tac2entries.mli
+++ b/user-contrib/Ltac2/tac2entries.mli
@@ -14,22 +14,19 @@ open Tac2expr
 
 (** {5 Toplevel definitions} *)
 
-val register_ltac : ?local:bool -> ?mut:bool -> rec_flag ->
+val register_ltac : ?deprecation:Deprecation.t -> ?local:bool -> ?mut:bool -> rec_flag ->
   (Names.lname * raw_tacexpr) list -> unit
 
 val register_type : ?local:bool -> rec_flag ->
   (qualid * redef_flag * raw_quant_typedef) list -> unit
 
-val register_primitive : ?local:bool ->
+val register_primitive : ?deprecation:Deprecation.t -> ?local:bool ->
   Names.lident -> raw_typexpr -> ml_tactic_name -> unit
 
-val register_struct
-  :  ?local:bool
-  -> strexpr
-  -> unit
+val register_struct : ?deprecation:Deprecation.t -> ?local:bool -> strexpr -> unit
 
-val register_notation : ?local:bool -> sexpr list -> int option ->
-  raw_tacexpr -> unit
+val register_notation : ?deprecation:Deprecation.t -> ?local:bool -> sexpr list ->
+  int option -> raw_tacexpr -> unit
 
 val perform_eval : pstate:Declare.Proof.t option -> raw_tacexpr -> unit
 
diff --git a/user-contrib/Ltac2/tac2env.ml b/user-contrib/Ltac2/tac2env.ml
index 5479ba0d54..5eb57c8f9b 100644
--- a/user-contrib/Ltac2/tac2env.ml
+++ b/user-contrib/Ltac2/tac2env.ml
@@ -18,6 +18,7 @@ type global_data = {
   gdata_expr : glb_tacexpr;
   gdata_type : type_scheme;
   gdata_mutable : bool;
+  gdata_deprecation : Deprecation.t option;
 }
 
 type constructor_data = {
@@ -35,12 +36,17 @@ type projection_data = {
   pdata_indx : int;
 }
 
+type alias_data = {
+  alias_body : raw_tacexpr;
+  alias_depr : Deprecation.t option;
+}
+
 type ltac_state = {
   ltac_tactics : global_data KNmap.t;
   ltac_constructors : constructor_data KNmap.t;
   ltac_projections : projection_data KNmap.t;
   ltac_types : glb_quant_typedef KNmap.t;
-  ltac_aliases : raw_tacexpr KNmap.t;
+  ltac_aliases : alias_data KNmap.t;
 }
 
 let empty_state = {
@@ -79,9 +85,10 @@ let define_type kn e =
 
 let interp_type kn = KNmap.find kn ltac_state.contents.ltac_types
 
-let define_alias kn tac =
+let define_alias ?deprecation kn tac =
   let state = !ltac_state in
-  ltac_state := { state with ltac_aliases = KNmap.add kn tac state.ltac_aliases }
+  let data = { alias_body = tac; alias_depr = deprecation } in
+  ltac_state := { state with ltac_aliases = KNmap.add kn data state.ltac_aliases }
 
 let interp_alias kn = KNmap.find kn ltac_state.contents.ltac_aliases
 
diff --git a/user-contrib/Ltac2/tac2env.mli b/user-contrib/Ltac2/tac2env.mli
index 95dcdd7e1b..3800ad0198 100644
--- a/user-contrib/Ltac2/tac2env.mli
+++ b/user-contrib/Ltac2/tac2env.mli
@@ -23,6 +23,7 @@ type global_data = {
   gdata_expr : glb_tacexpr;
   gdata_type : type_scheme;
   gdata_mutable : bool;
+  gdata_deprecation : Deprecation.t option;
 }
 
 val define_global : ltac_constant -> global_data -> unit
@@ -72,8 +73,13 @@ val interp_projection : ltac_projection -> projection_data
 
 (** {5 Toplevel definition of aliases} *)
 
-val define_alias : ltac_constant -> raw_tacexpr -> unit
-val interp_alias : ltac_constant -> raw_tacexpr
+type alias_data = {
+  alias_body : raw_tacexpr;
+  alias_depr : Deprecation.t option;
+}
+
+val define_alias : ?deprecation:Deprecation.t -> ltac_constant -> raw_tacexpr -> unit
+val interp_alias : ltac_constant -> alias_data
 
 (** {5 Name management} *)
 
diff --git a/user-contrib/Ltac2/tac2intern.ml b/user-contrib/Ltac2/tac2intern.ml
index ddf70a5a65..90c8528203 100644
--- a/user-contrib/Ltac2/tac2intern.ml
+++ b/user-contrib/Ltac2/tac2intern.ml
@@ -655,6 +655,35 @@ let is_alias env qid = match get_variable env qid with
 | ArgArg (TacAlias _) -> true
 | ArgVar _ | (ArgArg (TacConstant _)) -> false
 
+let is_user_name qid = match qid with
+| AbsKn _ -> false
+| RelId _ -> true
+
+let deprecated_ltac2_alias =
+  Deprecation.create_warning
+    ~object_name:"Ltac2 alias"
+    ~warning_name:"deprecated-ltac2-alias"
+    (fun kn -> pr_qualid (Tac2env.shortest_qualid_of_ltac (TacAlias kn)))
+
+let deprecated_ltac2_def =
+  Deprecation.create_warning
+    ~object_name:"Ltac2 definition"
+    ~warning_name:"deprecated-ltac2-definition"
+    (fun kn -> pr_qualid (Tac2env.shortest_qualid_of_ltac (TacConstant kn)))
+
+let check_deprecated_ltac2 ?loc qid def =
+  if is_user_name qid then match def with
+  | TacAlias kn ->
+    begin match (Tac2env.interp_alias kn).alias_depr with
+    | None -> ()
+    | Some depr -> deprecated_ltac2_alias ?loc (kn, depr)
+    end
+  | TacConstant kn ->
+    begin match (Tac2env.interp_global kn).gdata_deprecation with
+    | None -> ()
+    | Some depr -> deprecated_ltac2_def ?loc (kn, depr)
+    end
+
 let rec intern_rec env {loc;v=e} = match e with
 | CTacAtm atm -> intern_atm env atm
 | CTacRef qid ->
@@ -663,11 +692,12 @@ let rec intern_rec env {loc;v=e} = match e with
     let sch = Id.Map.find id env.env_var in
     (GTacVar id, fresh_mix_type_scheme env sch)
   | ArgArg (TacConstant kn) ->
-    let { Tac2env.gdata_type = sch } =
+    let { Tac2env.gdata_type = sch; gdata_deprecation = depr } =
       try Tac2env.interp_global kn
       with Not_found ->
         CErrors.anomaly (str "Missing hardwired primitive " ++ KerName.print kn)
     in
+    let () = check_deprecated_ltac2 ?loc qid (TacConstant kn) in
     (GTacRef kn, fresh_type_scheme env sch)
   | ArgArg (TacAlias kn) ->
     let e =
@@ -675,7 +705,8 @@ let rec intern_rec env {loc;v=e} = match e with
       with Not_found ->
         CErrors.anomaly (str "Missing hardwired alias " ++ KerName.print kn)
     in
-    intern_rec env e
+    let () = check_deprecated_ltac2 ?loc qid (TacAlias kn) in
+    intern_rec env e.alias_body
   end
 | CTacCst qid ->
   let kn = get_constructor env qid in
@@ -695,12 +726,13 @@ let rec intern_rec env {loc;v=e} = match e with
 | CTacApp ({loc;v=CTacCst qid}, args) ->
   let kn = get_constructor env qid in
   intern_constructor env loc kn args
-| CTacApp ({v=CTacRef qid}, args) when is_alias env qid ->
+| CTacApp ({v=CTacRef qid; loc=aloc}, args) when is_alias env qid ->
   let kn = match get_variable env qid with
   | ArgArg (TacAlias kn) -> kn
   | ArgVar _ | (ArgArg (TacConstant _)) -> assert false
   in
   let e = Tac2env.interp_alias kn in
+  let () = check_deprecated_ltac2 ?loc:aloc qid (TacAlias kn) in
   let map arg =
     (* Thunk alias arguments *)
     let loc = arg.loc in
@@ -709,7 +741,7 @@ let rec intern_rec env {loc;v=e} = match e with
     CAst.make ?loc @@ CTacFun ([var], arg)
   in
   let args = List.map map args in
-  intern_rec env (CAst.make ?loc @@ CTacApp (e, args))
+  intern_rec env (CAst.make ?loc @@ CTacApp (e.alias_body, args))
 | CTacApp (f, args) ->
   let loc = f.loc in
   let (f, ft) = intern_rec env f in
@@ -1243,7 +1275,9 @@ let rec globalize ids ({loc;v=er} as e) = match er with
   let mem id = Id.Set.mem id ids in
   begin match get_variable0 mem ref with
   | ArgVar _ -> e
-  | ArgArg kn -> CAst.make ?loc @@ CTacRef (AbsKn kn)
+  | ArgArg kn ->
+    let () = check_deprecated_ltac2 ?loc ref kn in
+    CAst.make ?loc @@ CTacRef (AbsKn kn)
   end
 | CTacCst qid ->
   let knc = get_constructor () qid in