Deprecation & recycling lemma names

Stream: mathlib4

[Yury G. Kudryashov]

In #14434, @Floris van Doorn suggests that we rename docs#mem_posTangentConeAt_of_segment_subset to sub_mem_posTangentConeAt_of_segment_subset and docs#mem_posTangentConeAt_of_segment_subset' to mem_posTangentConeAt_of_segment_subset. What should I do about @[deprecated] aliases in this case?

[Kim Morrison]

My suggestion would be:

• aspire to leave deprecations in place for 6 months
• but if they've made it into at least one "stable release" (i.e. a version bump) then they are fair game if there is a positive reason to drop them

[Yury G. Kudryashov]

What do you suggest in this specific situation? I want to rename A to B and A' to A.

[Jireh Loreaux]

I don't think we have deprecation capabilities for this situation. In that case, I would just proceed with the rename with no deprecation. This is in a relatively niche portion of Mathlib (in terms of downstream dependencies), so it's not ideal, but acceptable in my mind.

[Yury G. Kudryashov]

I'll deprecate the primed version and add mention the rename in the lemma with recycled name.

[Eric Wieser]

I think in the medium term we expect to have a special commit message format for describing this type of swap

[Eric Wieser]

In the very short term, #align tracks the identity despite the swap

[Winston Yin (尹維晨)]

I'd like to revive this thread in light of the fun_mul changes and other planned changes of mine. What is to be done when lemmas are renamed but the original names are immediately used in a different way? Situations like

1. (A, B) -> (A', A)
2. (A, _) -> (A', A) where _ -> A is a introduction of a new feature
3. (A, B) -> (B, A) or longer cycles

I'm fine if the answer is "known issue; not fixing".

[Eric Wieser]

I think the answer is currently "fill out the template in the PR to describe what happened"

[Ruben Van de Velde]

If you're not in a hurry, you can do

1. Move the old lemma to the new name, leave deprecated alias
2. Wait a cycle
3. Drop the the deprecated alias, add the new lemma in its place

but I'm not pushing for that as a general policy

[Ruben Van de Velde]

We sometimes also add a note to the docstring

[Kim Morrison]

The ideal would be to be able to write little composable instructions (maybe even metaprograms) that should be run in any downstream repository as it lake updates a dependency, i.e. to rename all A to A'.

Mario thought some about how to set this up a while back, but there would be a lot of implementation work. If someone is interested in exploring a project like this, please go ahead! We might have resources to do this in future, otherwise.

[Kim Morrison]

It's clearly going to become necessary as the ecosystem grows.