leanprover-community
Style: Add Deprecation sub-section
Zulip thread here: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Style.20guide.3A.20deprecation
I wonder: would this be a good place to explain mathlib's deprecation policy? (After six months, deprecated declarations may be removed.) Yes, that is scope creep - but that is also not explained yet outside of zulip.
Another idea for scope creep:
- do you think it's useful to say that named instances need not be deprecated? (That question also came up occasionally.)
There was also https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Deprecation.20policy, trying to gather consensus on a mathlib policy. I never followed through on documenting that... and some aspects are outdated now (for the better). The thread highlighted two more details
- for declarations generated by
to_additive, please ensure the generated declaration is also tagged with this attribute. For declarations generated bysimps, this is not strictly required. - "Cyclic renamings", here's a possible snippet:
We allow but discourage contributors to rename declaration X to Y and at the same time renaming W to X. In this case, no deprecation attribute is required for X (but it is for W).
Do you mind adding these as well? Sorry for aiming for really comprehensive docs here - but while we're at it, this is a good opportunity.
I hadn't seen that thread, thanks for the feedback! I tried to integrate all of your changes, with some minor modifications of my own to wording where I thought appropriate. Please give it a look and see if you'd like any further changes.
Thanks; I like your new version. There might always be ways to word-smith, but what's here looks good enough to me. I'll cross-post on zulip to get some more eyes on this; let's get this merged!