Style guide: deprecation

Stream: mathlib4

[Vlad Tsyrklevich]

I'm new to contributing to mathlib and needed to deprecate a lemma in favor of one with a different name to match style. I looked in the style guide online and didn't find anything about deprecation in the style guide. I found another thread asking for clarification and also this thread which suggested adding more info to @[deprecated] than what the deprecate to command currently adds, but maybe this command is not what people commonly use?

Anyways, it'd be nice to have a subsection in the style guide on deprecation, and though I have no idea what I'm talking about, I figured I'd write a suggestion to get the ball rolling. Please nitpick or re-write:

Deprecation

Deleting, renaming, or changing theorem definitions can cause downstreams projects that rely on these definitions to fail to compile. Any publicly exposed theorem definitions that are being changed should be gracefully transitioned by keeping the old theorem statement with a@[deprecated] attribute, to warn downstream projects to transition away from deprecated definitions before they are deleted. Renamed theorems can use a deprecated alias to the new name, while in cases where the theorem is not being replaced, the deprecated theorem definition can be marked with an attribute, like so:

theorem new_name : ... := ...
@[deprecated new_name (since := "YYYY-MM-DD")] alias old_name := new_name

@[deprecated "This theorem is deprecated in favor of using ... with ..." (since := "YYYY-MM-DD")]
theorem example_thm ...

The deprecate to command can help generate alias definitions. The @[deprecated] attribute should always include the deprecation date, and either the new name for the theorem when it is being renamed or kept substantially the same, or a string to explain how transition away form the old definition when a new version is no longer being provided.

[Yaël Dillies]

Note that there are two code snippets, deprecated and deprecated alias, to help you write deprecations

[Vlad Tsyrklevich]

Good point, I've edited the original text to make it more explicit about what I'm showing.

[Vlad Tsyrklevich]

Going to ask for feedback one more time before PRing it. (I'm trying to figure out what best practices are in proposing this, so please nitpick.)

[Eric Wieser]

I think the nitpicks are more easily made through the github UI, so go ahead and make the PR and link it from here

[Vlad Tsyrklevich]

https://github.com/leanprover-community/leanprover-community.github.io/pull/604