aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitlab-ci.yml38
-rw-r--r--.travis.yml32
-rw-r--r--CHANGES2
-rw-r--r--Makefile.build2
-rw-r--r--configure.ml5
-rw-r--r--doc/sphinx/language/gallina-specification-language.rst8
-rw-r--r--grammar/tacextend.mlp6
-rw-r--r--plugins/ltac/g_ltac.ml412
-rw-r--r--plugins/ltac/tacentries.ml32
-rw-r--r--plugins/ltac/tacentries.mli13
-rw-r--r--plugins/ltac/tacenv.ml47
-rw-r--r--plugins/ltac/tacenv.mli18
-rw-r--r--plugins/ltac/tacexpr.ml4
-rw-r--r--plugins/ltac/tacexpr.mli4
-rw-r--r--plugins/ltac/tacintern.ml27
-rw-r--r--plugins/ltac/tacinterp.ml8
-rw-r--r--test-suite/output/Deprecation.out3
-rw-r--r--test-suite/output/Deprecation.v6
-rw-r--r--test-suite/success/LtacDeprecation.v32
19 files changed, 173 insertions, 126 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 0ad68b508..be19a93a3 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -71,7 +71,7 @@ after_script:
- echo 'end:coq.clean'
- echo 'start:coq.config'
- - ./configure -prefix "$(pwd)/_install_ci" ${COQ_EXTRA_CONF}"$COQ_EXTRA_CONF_QUOTE"
+ - ./configure -warn-error yes -prefix "$(pwd)/_install_ci" ${COQ_EXTRA_CONF}"$COQ_EXTRA_CONF_QUOTE"
- echo 'end:coq.config'
- echo 'start:coq.build'
@@ -88,28 +88,6 @@ after_script:
- set +e
-.warnings-template: &warnings-template
- # keep warnings in test stage so we can test things even when warnings occur
- stage: test
- script:
- - set -e
-
- - echo 'start:coq.clean'
- - make clean # ensure that `make clean` works on a fresh clone
- - echo 'end:coq.clean'
-
- - echo 'start:coq.config'
- - ./configure -local ${COQ_EXTRA_CONF}
- - echo 'end:coq.config'
-
- - echo 'start:coq.build'
- - make -j "$NJOBS" coqocaml
- - echo 'end:coq:build'
-
- - set +e
- variables: &warnings-variables
- COQ_EXTRA_CONF: "-native-compiler yes -coqide byte -byte-only -warn-error yes"
-
# every non build job must set dependencies otherwise all build
# artifacts are used together and we may get some random Coq. To that
# purpose, we add a spurious dependency `not-a-real-job` that must be
@@ -264,20 +242,6 @@ pkg:nix:
paths:
- nix-build-coq.drv-0/*/test-suite/logs
-warnings:base:
- <<: *warnings-template
-
-# warnings:32bit:
-# <<: *warnings-template
-# variables:
-# <<: *warnings-variables
-
-warnings:edge:
- <<: *warnings-template
- variables:
- <<: *warnings-variables
- OPAM_SWITCH: edge
-
documentation:
<<: *doc-template
dependencies:
diff --git a/.travis.yml b/.travis.yml
index 3301d97ce..53fbe5821 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -164,36 +164,6 @@ matrix:
- avsm
packages: *extra-packages
- # Ocaml warnings with two compilers
- - if: NOT (type = pull_request)
- env:
- - MAIN_TARGET="coqocaml"
- - EXTRA_CONF="-byte-only -coqide byte -warn-error yes"
- - EXTRA_OPAM="${LABLGTK}"
- addons:
- apt:
- sources:
- - avsm
- packages: &coqide-packages
- - opam
- - aspcud
- - libgtk2.0-dev
- - libgtksourceview2.0-dev
-
- - if: NOT (type = pull_request)
- env:
- - MAIN_TARGET="coqocaml"
- - COMPILER="${COMPILER_BE}"
- - FINDLIB_VER="${FINDLIB_VER_BE}"
- - CAMLP5_VER="${CAMLP5_VER_BE}"
- - EXTRA_CONF="-byte-only -coqide byte -warn-error yes"
- - EXTRA_OPAM="${LABLGTK_BE}"
- addons:
- apt:
- sources:
- - avsm
- packages: *coqide-packages
-
- os: osx
env:
- TEST_TARGET="test-suite"
@@ -260,7 +230,7 @@ script:
- echo -en 'travis_fold:end:coq.clean\\r'
- echo 'Configuring Coq...' && echo -en 'travis_fold:start:coq.config\\r'
-- ./configure ${COQ_DEST} -native-compiler ${NATIVE_COMP} ${EXTRA_CONF}
+- ./configure ${COQ_DEST} -warn-error yes -native-compiler ${NATIVE_COMP} ${EXTRA_CONF}
- echo -en 'travis_fold:end:coq.config\\r'
- echo 'Building Coq...' && echo -en 'travis_fold:start:coq.build\\r'
diff --git a/CHANGES b/CHANGES
index 6dce7b0db..fdd4feb59 100644
--- a/CHANGES
+++ b/CHANGES
@@ -38,6 +38,8 @@ Tactics
without adding new ones. Preexisting tactic `constr_eq_nounivs` can
still be used if you really want to ignore universe constraints.
+- Tactics and tactic notations now understand the `deprecated` attribute.
+
Tools
- Coq_makefile lets one override or extend the following variables from
diff --git a/Makefile.build b/Makefile.build
index 84f86c99a..c100eda40 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -195,7 +195,7 @@ TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
# the output format of the unix command time. For instance:
# TIME="%C (%U user, %S sys, %e total, %M maxres)"
-COQOPTS=$(NATIVECOMPUTE)
+COQOPTS=$(NATIVECOMPUTE) $(COQWARNERROR)
BOOTCOQC=$(TIMER) $(COQTOPBEST) -boot $(COQOPTS) -compile
LOCALINCLUDES=$(addprefix -I ,$(SRCDIRS))
diff --git a/configure.ml b/configure.ml
index 194f47c49..c08e8dfcc 100644
--- a/configure.ml
+++ b/configure.ml
@@ -647,8 +647,10 @@ let camltag = match caml_version_list with
48: implicit elimination of optional arguments: too common
50: unexpected documentation comment: too common and annoying to avoid
56: unreachable match case: the [_ -> .] syntax doesn't exist in 4.02.3
+ 58: "no cmx file was found in path": See https://github.com/ocaml/num/issues/9
+ 59: "potential assignment to a non-mutable value": See Coq's issue #8043
*)
-let coq_warnings = "-w +a-4-9-27-41-42-44-45-48-50"
+let coq_warnings = "-w +a-4-9-27-41-42-44-45-48-50-58-59"
let coq_warn_error =
if !prefs.warn_error
then "-warn-error +a"
@@ -1337,6 +1339,7 @@ let write_makefile f =
pr "WITHDOC=%s\n\n" (if !prefs.withdoc then "all" else "no");
pr "# Option to produce precompiled files for native_compute\n";
pr "NATIVECOMPUTE=%s\n" (if !prefs.nativecompiler then "-native-compiler" else "");
+ pr "COQWARNERROR=%s\n" (if !prefs.warn_error then "-w +default" else "");
close_out o;
Unix.chmod f 0o444
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index ac6a20198..8250b4b3d 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -1430,6 +1430,12 @@ the following attributes names are recognized:
Takes as value the optional attributes ``since`` and ``note``;
both have a string value.
+ This attribute can trigger the following warnings:
+
+ .. warn:: Tactic @qualid is deprecated since @string. @string.
+
+ .. warn:: Tactic Notation @qualid is deprecated since @string. @string.
+
Here are a few examples:
.. coqtop:: all reset
@@ -1440,7 +1446,7 @@ Here are a few examples:
exact O.
Defined.
- #[deprecated(since="8.9.0", note="use idtac instead")]
+ #[deprecated(since="8.9.0", note="Use idtac instead.")]
Ltac foo := idtac.
Goal True.
diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp
index cea0bed59..02da61ef7 100644
--- a/grammar/tacextend.mlp
+++ b/grammar/tacextend.mlp
@@ -49,13 +49,17 @@ EXTEND
GLOBAL: str_item;
str_item:
[ [ "TACTIC"; "EXTEND"; s = tac_name;
+ depr = OPT [ "DEPRECATED"; depr = LIDENT -> depr ];
level = OPT [ "AT"; UIDENT "LEVEL"; level = INT -> level ];
OPT "|"; l = LIST1 tacrule SEP "|";
"END" ->
let level = match level with Some i -> int_of_string i | None -> 0 in
let level = mlexpr_of_int level in
+ let depr = mlexpr_of_option (fun l -> <:expr< $lid:l$ >>) depr in
let l = <:expr< Tacentries.($mlexpr_of_list (fun x -> x) l$) >> in
- declare_str_items loc [ <:str_item< Tacentries.tactic_extend $plugin_name$ $str:s$ ~{ level = $level$ } $l$ >> ] ] ]
+ declare_str_items loc [ <:str_item< Tacentries.tactic_extend
+ $plugin_name$ $str:s$ ~{ level = $level$ } ?{ deprecation =
+ $depr$ } $l$ >> ] ] ]
;
tacrule:
[ [ "["; l = LIST1 tacargs; "]";
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 9d86f21d4..c13bd69da 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -287,12 +287,14 @@ GEXTEND Gram
(* Definitions for tactics *)
tacdef_body:
- [ [ name = Constr.global; it=LIST1 input_fun; redef = ltac_def_kind; body = tactic_expr ->
+ [ [ name = Constr.global; it=LIST1 input_fun;
+ redef = ltac_def_kind; body = tactic_expr ->
if redef then Tacexpr.TacticRedefinition (name, TacFun (it, body))
else
let id = reference_to_id name in
Tacexpr.TacticDefinition (id, TacFun (it, body))
- | name = Constr.global; redef = ltac_def_kind; body = tactic_expr ->
+ | name = Constr.global; redef = ltac_def_kind;
+ body = tactic_expr ->
if redef then Tacexpr.TacticRedefinition (name, body)
else
let id = reference_to_id name in
@@ -468,7 +470,8 @@ VERNAC COMMAND FUNCTIONAL EXTEND VernacTacticNotation
[ VtSideff [], VtNow ] ->
[ fun ~atts ~st -> let open Vernacinterp in
let n = Option.default 0 n in
- Tacentries.add_tactic_notation (Locality.make_module_locality atts.locality) n r e;
+ let deprecation = atts.deprecated in
+ Tacentries.add_tactic_notation (Locality.make_module_locality atts.locality) n ?deprecation r e;
st
]
END
@@ -512,7 +515,8 @@ VERNAC COMMAND FUNCTIONAL EXTEND VernacDeclareTacticDefinition
| TacticDefinition ({CAst.v=r},_) -> r
| TacticRedefinition (qid,_) -> qualid_basename qid) l), VtLater
] -> [ fun ~atts ~st -> let open Vernacinterp in
- Tacentries.register_ltac (Locality.make_module_locality atts.locality) l;
+ let deprecation = atts.deprecated in
+ Tacentries.register_ltac (Locality.make_module_locality atts.locality) ?deprecation l;
st
]
END
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index fac464a62..4b834d66d 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -252,7 +252,7 @@ type tactic_grammar_obj = {
tacobj_key : KerName.t;
tacobj_local : locality_flag;
tacobj_tacgram : tactic_grammar;
- tacobj_body : Id.t list * Tacexpr.glob_tactic_expr;
+ tacobj_body : Tacenv.alias_tactic;
tacobj_forml : bool;
}
@@ -288,10 +288,11 @@ let load_tactic_notation i (_, tobj) =
extend_tactic_grammar key tobj.tacobj_forml tobj.tacobj_tacgram
let subst_tactic_notation (subst, tobj) =
- let (ids, body) = tobj.tacobj_body in
+ let open Tacenv in
+ let alias = tobj.tacobj_body in
{ tobj with
tacobj_key = Mod_subst.subst_kn subst tobj.tacobj_key;
- tacobj_body = (ids, Tacsubst.subst_tactic subst body);
+ tacobj_body = { alias with alias_body = Tacsubst.subst_tactic subst alias.alias_body };
}
let classify_tactic_notation tacobj = Substitute tacobj
@@ -308,25 +309,26 @@ let cons_production_parameter = function
| TacTerm _ -> None
| TacNonTerm (_, (_, ido)) -> ido
-let add_glob_tactic_notation local ~level prods forml ids tac =
+let add_glob_tactic_notation local ~level ?deprecation prods forml ids tac =
let parule = {
tacgram_level = level;
tacgram_prods = prods;
} in
+ let open Tacenv in
let tacobj = {
tacobj_key = make_fresh_key prods;
tacobj_local = local;
tacobj_tacgram = parule;
- tacobj_body = (ids, tac);
+ tacobj_body = { alias_args = ids; alias_body = tac; alias_deprecation = deprecation };
tacobj_forml = forml;
} in
Lib.add_anonymous_leaf (inTacticGrammar tacobj)
-let add_tactic_notation local n prods e =
+let add_tactic_notation local n ?deprecation prods e =
let ids = List.map_filter cons_production_parameter prods in
let prods = List.map interp_prod_item prods in
let tac = Tacintern.glob_tactic_env ids (Global.env()) e in
- add_glob_tactic_notation local ~level:n prods false ids tac
+ add_glob_tactic_notation local ~level:n ?deprecation prods false ids tac
(**********************************************************************)
(* ML Tactic entries *)
@@ -366,7 +368,7 @@ let extend_atomic_tactic name entries =
in
List.iteri add_atomic entries
-let add_ml_tactic_notation name ~level prods =
+let add_ml_tactic_notation name ~level ?deprecation prods =
let len = List.length prods in
let iter i prods =
let open Tacexpr in
@@ -378,7 +380,7 @@ let add_ml_tactic_notation name ~level prods =
let entry = { mltac_name = name; mltac_index = len - i - 1 } in
let map id = Reference (Locus.ArgVar (CAst.make id)) in
let tac = TacML (Loc.tag (entry, List.map map ids)) in
- add_glob_tactic_notation false ~level prods true ids tac
+ add_glob_tactic_notation false ~level ?deprecation prods true ids tac
in
List.iteri iter (List.rev prods);
(** We call [extend_atomic_tactic] only for "basic tactics" (the ones at
@@ -430,7 +432,7 @@ let warn_unusable_identifier =
(fun id -> strbrk "The Ltac name" ++ spc () ++ Id.print id ++ spc () ++
strbrk "may be unusable because of a conflict with a notation.")
-let register_ltac local tacl =
+let register_ltac local ?deprecation tacl =
let map tactic_body =
match tactic_body with
| Tacexpr.TacticDefinition ({CAst.loc;v=id}, body) ->
@@ -483,10 +485,10 @@ let register_ltac local tacl =
let defs = States.with_state_protection defs () in
let iter (def, tac) = match def with
| NewTac id ->
- Tacenv.register_ltac false local id tac;
+ Tacenv.register_ltac false local id tac ?deprecation;
Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is defined")
| UpdateTac kn ->
- Tacenv.redefine_ltac local kn tac;
+ Tacenv.redefine_ltac local kn tac ?deprecation;
let name = Tacenv.shortest_qualid_of_tactic kn in
Flags.if_verbose Feedback.msg_info (Libnames.pr_qualid name ++ str " is redefined")
in
@@ -658,7 +660,7 @@ let lift_constr_tac_to_ml_tac vars tac =
end in
tac
-let tactic_extend plugin_name tacname ~level sign =
+let tactic_extend plugin_name tacname ~level ?deprecation sign =
let open Tacexpr in
let ml_tactic_name =
{ mltac_tactic = tacname;
@@ -687,10 +689,10 @@ let tactic_extend plugin_name tacname ~level sign =
This is the rôle of the [lift_constr_tac_to_ml_tac] function. *)
let body = Tacexpr.TacFun (vars, Tacexpr.TacML (Loc.tag (ml, [])))in
let id = Names.Id.of_string name in
- let obj () = Tacenv.register_ltac true false id body in
+ let obj () = Tacenv.register_ltac true false id body ?deprecation in
let () = Tacenv.register_ml_tactic ml_tactic_name [|tac|] in
Mltop.declare_cache_obj obj plugin_name
| _ ->
- let obj () = add_ml_tactic_notation ml_tactic_name ~level (List.map clause_of_ty_ml sign) in
+ let obj () = add_ml_tactic_notation ml_tactic_name ~level ?deprecation (List.map clause_of_ty_ml sign) in
Tacenv.register_ml_tactic ml_tactic_name @@ Array.of_list (List.map eval sign);
Mltop.declare_cache_obj obj plugin_name
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index f873631ff..138a584e0 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -12,10 +12,12 @@
open Vernacexpr
open Tacexpr
+open Vernacinterp
(** {5 Tactic Definitions} *)
-val register_ltac : locality_flag -> Tacexpr.tacdef_body list -> unit
+val register_ltac : locality_flag -> ?deprecation:deprecation ->
+ Tacexpr.tacdef_body list -> unit
(** Adds new Ltac definitions to the environment. *)
(** {5 Tactic Notations} *)
@@ -34,8 +36,8 @@ type argument = Genarg.ArgT.any Extend.user_symbol
leaves. *)
val add_tactic_notation :
- locality_flag -> int -> raw_argument grammar_tactic_prod_item_expr list ->
- raw_tactic_expr -> unit
+ locality_flag -> int -> ?deprecation:deprecation -> raw_argument
+ grammar_tactic_prod_item_expr list -> raw_tactic_expr -> unit
(** [add_tactic_notation local level prods expr] adds a tactic notation in the
environment at level [level] with locality [local] made of the grammar
productions [prods] and returning the body [expr] *)
@@ -47,7 +49,7 @@ val register_tactic_notation_entry : string -> ('a, 'b, 'c) Genarg.genarg_type -
to finding an argument by name (as in {!Genarg}) if there is none
matching. *)
-val add_ml_tactic_notation : ml_tactic_name -> level:int ->
+val add_ml_tactic_notation : ml_tactic_name -> level:int -> ?deprecation:deprecation ->
argument grammar_tactic_prod_item_expr list list -> unit
(** A low-level variant of {!add_tactic_notation} used by the TACTIC EXTEND
ML-side macro. *)
@@ -78,4 +80,5 @@ type _ ty_sig =
type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml
-val tactic_extend : string -> string -> level:Int.t -> ty_ml list -> unit
+val tactic_extend : string -> string -> level:Int.t ->
+ ?deprecation:deprecation -> ty_ml list -> unit
diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml
index d5ab2d690..0bb9ccb1d 100644
--- a/plugins/ltac/tacenv.ml
+++ b/plugins/ltac/tacenv.ml
@@ -52,7 +52,11 @@ let shortest_qualid_of_tactic kn =
(** Tactic notations (TacAlias) *)
type alias = KerName.t
-type alias_tactic = Id.t list * glob_tactic_expr
+type alias_tactic =
+ { alias_args: Id.t list;
+ alias_body: glob_tactic_expr;
+ alias_deprecation: Vernacinterp.deprecation option;
+ }
let alias_map = Summary.ref ~name:"tactic-alias"
(KNmap.empty : alias_tactic KNmap.t)
@@ -118,6 +122,7 @@ type ltac_entry = {
tac_for_ml : bool;
tac_body : glob_tactic_expr;
tac_redef : ModPath.t list;
+ tac_deprecation : Vernacinterp.deprecation option
}
let mactab =
@@ -130,8 +135,12 @@ let interp_ltac r = (KNmap.find r !mactab).tac_body
let is_ltac_for_ml_tactic r = (KNmap.find r !mactab).tac_for_ml
-let add kn b t =
- let entry = { tac_for_ml = b; tac_body = t; tac_redef = [] } in
+let add ~deprecation kn b t =
+ let entry = { tac_for_ml = b;
+ tac_body = t;
+ tac_redef = [];
+ tac_deprecation = deprecation;
+ } in
mactab := KNmap.add kn entry !mactab
let replace kn path t =
@@ -139,34 +148,38 @@ let replace kn path t =
let entry _ e = { e with tac_body = t; tac_redef = path :: e.tac_redef } in
mactab := KNmap.modify kn entry !mactab
-let load_md i ((sp, kn), (local, id, b, t)) = match id with
+let tac_deprecation kn =
+ try (KNmap.find kn !mactab).tac_deprecation with Not_found -> None
+
+let load_md i ((sp, kn), (local, id, b, t, deprecation)) = match id with
| None ->
let () = if not local then push_tactic (Until i) sp kn in
- add kn b t
+ add ~deprecation kn b t
| Some kn0 -> replace kn0 kn t
-let open_md i ((sp, kn), (local, id, b, t)) = match id with
+let open_md i ((sp, kn), (local, id, b, t, deprecation)) = match id with
| None ->
let () = if not local then push_tactic (Exactly i) sp kn in
- add kn b t
+ add ~deprecation kn b t
| Some kn0 -> replace kn0 kn t
-let cache_md ((sp, kn), (local, id ,b, t)) = match id with
+let cache_md ((sp, kn), (local, id ,b, t, deprecation)) = match id with
| None ->
let () = push_tactic (Until 1) sp kn in
- add kn b t
+ add ~deprecation kn b t
| Some kn0 -> replace kn0 kn t
let subst_kind subst id = match id with
| None -> None
| Some kn -> Some (Mod_subst.subst_kn subst kn)
-let subst_md (subst, (local, id, b, t)) =
- (local, subst_kind subst id, b, Tacsubst.subst_tactic subst t)
+let subst_md (subst, (local, id, b, t, deprecation)) =
+ (local, subst_kind subst id, b, Tacsubst.subst_tactic subst t, deprecation)
-let classify_md (local, _, _, _ as o) = Substitute o
+let classify_md (local, _, _, _, _ as o) = Substitute o
-let inMD : bool * ltac_constant option * bool * glob_tactic_expr -> obj =
+let inMD : bool * ltac_constant option * bool * glob_tactic_expr *
+ Vernacinterp.deprecation option -> obj =
declare_object {(default_object "TAC-DEFINITION") with
cache_function = cache_md;
load_function = load_md;
@@ -174,8 +187,8 @@ let inMD : bool * ltac_constant option * bool * glob_tactic_expr -> obj =
subst_function = subst_md;
classify_function = classify_md}
-let register_ltac for_ml local id tac =
- ignore (Lib.add_leaf id (inMD (local, None, for_ml, tac)))
+let register_ltac for_ml local ?deprecation id tac =
+ ignore (Lib.add_leaf id (inMD (local, None, for_ml, tac, deprecation)))
-let redefine_ltac local kn tac =
- Lib.add_anonymous_leaf (inMD (local, Some kn, false, tac))
+let redefine_ltac local ?deprecation kn tac =
+ Lib.add_anonymous_leaf (inMD (local, Some kn, false, tac, deprecation))
diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli
index 3af2f2a46..7143f5185 100644
--- a/plugins/ltac/tacenv.mli
+++ b/plugins/ltac/tacenv.mli
@@ -12,6 +12,7 @@ open Names
open Libnames
open Tacexpr
open Geninterp
+open Vernacinterp
(** This module centralizes the various ways of registering tactics. *)
@@ -29,7 +30,11 @@ val shortest_qualid_of_tactic : ltac_constant -> qualid
type alias = KerName.t
(** Type of tactic alias, used in the [TacAlias] node. *)
-type alias_tactic = Id.t list * glob_tactic_expr
+type alias_tactic =
+ { alias_args: Id.t list;
+ alias_body: glob_tactic_expr;
+ alias_deprecation: Vernacinterp.deprecation option;
+ }
(** Contents of a tactic notation *)
val register_alias : alias -> alias_tactic -> unit
@@ -43,7 +48,8 @@ val check_alias : alias -> bool
(** {5 Coq tactic definitions} *)
-val register_ltac : bool -> bool -> Id.t -> glob_tactic_expr -> unit
+val register_ltac : bool -> bool -> ?deprecation:deprecation -> Id.t ->
+ glob_tactic_expr -> unit
(** Register a new Ltac with the given name and body.
The first boolean indicates whether this is done from ML side, rather than
@@ -51,7 +57,8 @@ val register_ltac : bool -> bool -> Id.t -> glob_tactic_expr -> unit
definition. It also puts the Ltac name in the nametab, so that it can be
used unqualified. *)
-val redefine_ltac : bool -> KerName.t -> glob_tactic_expr -> unit
+val redefine_ltac : bool -> ?deprecation:deprecation -> KerName.t ->
+ glob_tactic_expr -> unit
(** Replace a Ltac with the given name and body. If the boolean flag is set
to true, then this is a local redefinition. *)
@@ -61,6 +68,9 @@ val interp_ltac : KerName.t -> glob_tactic_expr
val is_ltac_for_ml_tactic : KerName.t -> bool
(** Whether the tactic is defined from ML-side *)
+val tac_deprecation : KerName.t -> deprecation option
+(** The tactic deprecation notice, if any *)
+
type ltac_entry = {
tac_for_ml : bool;
(** Whether the tactic is defined from ML-side *)
@@ -68,6 +78,8 @@ type ltac_entry = {
(** The current body of the tactic *)
tac_redef : ModPath.t list;
(** List of modules redefining the tactic in reverse chronological order *)
+ tac_deprecation : deprecation option;
+ (** Deprecation notice to be printed when the tactic is used *)
}
val ltac_entries : unit -> ltac_entry KNmap.t
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index 06d2711ad..59b748e25 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -398,5 +398,5 @@ type ltac_call_kind =
type ltac_trace = ltac_call_kind Loc.located list
type tacdef_body =
- | TacticDefinition of lident * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *)
- | TacticRedefinition of qualid * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *)
+ | TacticDefinition of lident * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *)
+ | TacticRedefinition of qualid * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *)
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 71e1edfd7..3a0badb28 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -398,5 +398,5 @@ type ltac_call_kind =
type ltac_trace = ltac_call_kind Loc.located list
type tacdef_body =
- | TacticDefinition of lident * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *)
- | TacticRedefinition of qualid * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *)
+ | TacticDefinition of lident * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *)
+ | TacticRedefinition of qualid * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *)
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 481fc30df..144480062 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -117,9 +117,26 @@ let intern_constr_reference strict ist qid =
(* Internalize an isolated reference in position of tactic *)
+let warn_deprecated_tactic =
+ CWarnings.create ~name:"deprecated-tactic" ~category:"deprecated"
+ (fun (qid,depr) -> str "Tactic " ++ pr_qualid qid ++
+ strbrk " is deprecated" ++
+ pr_opt (fun since -> str "since " ++ str since) depr.Vernacinterp.since ++
+ str "." ++ pr_opt (fun note -> str note) depr.Vernacinterp.note)
+
+let warn_deprecated_alias =
+ CWarnings.create ~name:"deprecated-tactic-notation" ~category:"deprecated"
+ (fun (kn,depr) -> str "Tactic Notation " ++ Pptactic.pr_alias_key kn ++
+ strbrk " is deprecated since" ++
+ pr_opt (fun since -> str "since " ++ str since) depr.Vernacinterp.since ++
+ str "." ++ pr_opt (fun note -> str note) depr.Vernacinterp.note)
+
let intern_isolated_global_tactic_reference qid =
let loc = qid.CAst.loc in
- TacCall (Loc.tag ?loc (ArgArg (loc,Tacenv.locate_tactic qid),[]))
+ let kn = Tacenv.locate_tactic qid in
+ Option.iter (fun depr -> warn_deprecated_tactic ?loc (qid,depr)) @@
+ Tacenv.tac_deprecation kn;
+ TacCall (Loc.tag ?loc (ArgArg (loc,kn),[]))
let intern_isolated_tactic_reference strict ist qid =
(* An ltac reference *)
@@ -137,7 +154,11 @@ let intern_isolated_tactic_reference strict ist qid =
(* Internalize an applied tactic reference *)
let intern_applied_global_tactic_reference qid =
- ArgArg (qid.CAst.loc,Tacenv.locate_tactic qid)
+ let loc = qid.CAst.loc in
+ let kn = Tacenv.locate_tactic qid in
+ Option.iter (fun depr -> warn_deprecated_tactic ?loc (qid,depr)) @@
+ Tacenv.tac_deprecation kn;
+ ArgArg (loc,kn)
let intern_applied_tactic_reference ist qid =
(* An ltac reference *)
@@ -643,6 +664,8 @@ and intern_tactic_seq onlytac ist = function
(* For extensions *)
| TacAlias (loc,(s,l)) ->
+ let alias = Tacenv.interp_alias s in
+ Option.iter (fun o -> warn_deprecated_alias ?loc (s,o)) @@ alias.Tacenv.alias_deprecation;
let l = List.map (intern_tacarg !strict_check false ist) l in
ist.ltacvars, TacAlias (Loc.tag ?loc (s,l))
| TacML (loc,(opn,l)) ->
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index d9ac96d89..77b5b06d4 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1125,17 +1125,17 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
| TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac)
(* For extensions *)
| TacAlias (loc,(s,l)) ->
- let (ids, body) = Tacenv.interp_alias s in
+ let alias = Tacenv.interp_alias s in
let (>>=) = Ftactic.bind in
let interp_vars = Ftactic.List.map (fun v -> interp_tacarg ist v) l in
let tac l =
let addvar x v accu = Id.Map.add x v accu in
- let lfun = List.fold_right2 addvar ids l ist.lfun in
+ let lfun = List.fold_right2 addvar alias.Tacenv.alias_args l ist.lfun in
Ftactic.lift (push_trace (loc,LtacNotationCall s) ist) >>= fun trace ->
let ist = {
lfun = lfun;
extra = TacStore.set ist.extra f_trace trace; } in
- val_interp ist body >>= fun v ->
+ val_interp ist alias.Tacenv.alias_body >>= fun v ->
Ftactic.lift (tactic_of_value ist v)
in
let tac =
@@ -1147,7 +1147,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
some more elaborate solution will have to be used. *)
in
let tac =
- let len1 = List.length ids in
+ let len1 = List.length alias.Tacenv.alias_args in
let len2 = List.length l in
if len1 = len2 then tac
else Tacticals.New.tclZEROMSG (str "Arguments length mismatch: \
diff --git a/test-suite/output/Deprecation.out b/test-suite/output/Deprecation.out
new file mode 100644
index 000000000..7e290847c
--- /dev/null
+++ b/test-suite/output/Deprecation.out
@@ -0,0 +1,3 @@
+File "stdin", line 5, characters 0-3:
+Warning: Tactic foo is deprecated since X.Y. Use idtac instead.
+[deprecated-tactic,deprecated]
diff --git a/test-suite/output/Deprecation.v b/test-suite/output/Deprecation.v
new file mode 100644
index 000000000..04d5eb3d4
--- /dev/null
+++ b/test-suite/output/Deprecation.v
@@ -0,0 +1,6 @@
+#[deprecated(since = "X.Y", note = "Use idtac instead.")]
+ Ltac foo := idtac.
+
+Goal True.
+foo.
+Abort.
diff --git a/test-suite/success/LtacDeprecation.v b/test-suite/success/LtacDeprecation.v
new file mode 100644
index 000000000..633a5e474
--- /dev/null
+++ b/test-suite/success/LtacDeprecation.v
@@ -0,0 +1,32 @@
+Set Warnings "+deprecated".
+
+#[deprecated(since = "8.8", note = "Use idtac instead")]
+Ltac foo x := idtac.
+
+Goal True.
+Fail (foo true).
+Abort.
+
+Fail Ltac bar := foo.
+Fail Tactic Notation "bar" := foo.
+
+#[deprecated(since = "8.8", note = "Use idtac instead")]
+Tactic Notation "bar" := idtac.
+
+Goal True.
+Fail bar.
+Abort.
+
+Fail Ltac zar := bar.
+
+Set Warnings "-deprecated".
+
+Ltac zar := foo.
+Ltac zarzar := bar.
+
+Set Warnings "+deprecated".
+
+Goal True.
+zar x.
+zarzar.
+Abort.
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 13:20:47 +0000