how to deprecate

Stream: mathlib4

[Edward van de Meent]

i'm looking into picking up this renaming issue, and realised that i will have to deprecate the old lemma names. There is no clear deprecation guide on the community website, so i'd like to ask here, how do i deprecate old lemma names? (and should there be a guide for this somewhere?)

[Yaël Dillies]

Oh sorry, can you please not touch this issue? I am preparing a huge PR for it

[Edward van de Meent]

please do claim the issue on github then :upside_down:

[Edward van de Meent]

still, the question for a deprecation guide stands

[Damiano Testa]

If you have branch whose only difference with master is the renaming of declarations, then running the script ./scripts/add_deprecations.sh should automatically add the deprecations for those statements. The script is text-based, so it is prone to mistakes, but empirically it tends to work. The script is also a bit more lenient than "no modifications other than renames", but it will get progressively more confused, as you diverge more from this assumption.

[Damiano Testa]

Once you have the deprecations in place, then the old names will be flagged by the deprecated linter. I just got a PR delegated that contains a script that will try to automatically use the non-deprecated names where the deprecated ones are used, but I would like to test it some more before merging.

[Yaël Dillies]

Edward van de Meent said:

please do claim the issue on github then :upside_down:

I had no idea this issue existed, sorry!