If there is a way to mark some definition deprecated so it will trigger a compilation warning?
Thank!
There’s the deprecated attribute, but it doesn’t work for Lemmas.
Maybe this hack can be useful:
(* To make `foo` deprecated, rename it to `deprecated_foo` and add a notation using the `depricated` attribute. *)
Lemma deprecated_foo : 2 = 1 + 1.
Proof. reflexivity. Qed.
#[deprecated(note="Use bar instead")]
Notation foo := deprecated_foo (only parsing).
Goal 2 = 1 + 1.
Proof.
apply foo.
(* Warning: Notation foo is deprecated. Use lemma bar instead [deprecated-syntactic-definition,deprecated] *)
Qed.
1 Like
Thanks! That it is hack indeed, but should work. Perhaps it may be a feature to add in the future versions of Coq?
On a second thought, I believe it is not really a hack. Notations are sometimes used for providing old lemma names for compatibility, after lemmas have been renamed. (For example, the module ConstructiveEpsilon.v of stdlib provides old lemma names as (only parsing) notations (hidden in the coqdoc)). So if you just want to rename a lemma and keep the old names for compatibility, I believe it is a good idea to make the old names a notation with the deprecated attribute.
But one should also support deprecated on lemmas directly…
This is indeed the proper way to do this when you want to rename a lemma (it’s even documented in the reference manual now). If you want to remove a lemma, it’s true that it does not work as well, and adding support for the deprecated attribute on any definition or lemma would be nice as well (and shouldn’t be so hard).
I’ve added a feature request https://github.com/coq/coq/issues/12266
1 Like