Guidance on breaking changes

[b-mehta]

The motivation here is that:

1. Users bumping their mathlib versions by a small amount (eg less than one month) should not have to deal with errors in their code
2. But if this is necessary, then mathlib should endeavour to make them as easy to fix as possible
3. We already follow these principles with the deprecation policy and deprecation of modules policy
4. Ecosystems of programming languages are often very strict with breaking changes, and the guidance I add here is relatively very mild to the contributor and harsh on the downstream user. I don't like that it's this way round, but hopefully the change here is a step in the right direction and uncontroversially so. (see eg Rust's policy on breaking changes https://rustc-dev-guide.rust-lang.org/bug-fix-procedure.html, or SemVer's rule on backwards-incompatible changes https://semver.org/#spec-item-8)
5. Lean core sets an expectation that breaking changes will be discussed in the release notes: https://github.com/leanprover/lean4/blob/master/RELEASES.md
6. A number of PRs already discuss breaking changes in their description
7. Hopscotch and its existing CI workflows create issues/PRs giving the mathlib commit and PR description which breaks project code, so requiring it to be mentioned in the description is especially useful for users of hopscotch.

The spirit of this policy already exists in mathlib writings in various guises:

• We discourage non-terminal simps because they make it more likely that a new [simp] can produce a breaking change (and more generally the flexible linter)
• We have a deprecation policy for names and modules
• The "Growing Mathlib" paper says

Many large formalisation projects are carried out in a repository depending on Mathlib. If keeping
up with the latest Mathlib changes is too onerous, contributing results back to Mathlib may become impossible.

Previous discussion on related points:

• https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Deprecation.20.26.20recycling.20lemma.20names
• #mathlib4 > notes for adaptations each release cycle @ 💬
• #mathlib maintainers > Deleting #align statements @ 💬 in particular the comment

Imagine that refactor PRs have to pass a check that every unique id is accounted for by mentioning which are added and which are deleted in the PR description. Then as a reviewer you can know if every declaration has been preserved (modulo judgment calls for whether to preserve an id for a transformed statement).
Adding what you just said, it could also check that the id refers to the same statement, and if not, the PR description must mention the breaking change.

• #lean4 > Deprecation without explanations @ 💬
• The general discussion around deprecated modules

[grunweg]

Thanks for proposing this. I think it's good to document this, and start a discussion. I'm not sure, though, if this has been discussed before. Can you point me to a discussion that I missed, or start a brief one on Zulip?

[grunweg]

I'm not sure what exactly this sentence is contrasting. To me, the sentence reads fine without it.

Suggested change

	However, this kind of change is sometimes necessary for the growth of mathlib, but should be carefully considered.
	This kind of change is sometimes necessary for the growth of mathlib, but should be carefully considered.

[b-mehta]

The intended message here is "You should avoid doing this unless you really have to, but sometimes you truly do have to". I'm happy with alternate wording which conveys this!

[grunweg]

To me, it's not 100% clear what this means. Do you have an example in mind? (Do you think we have been following this, or would this also be a proposed new policy?)

[b-mehta]

I think this is followed in general, but not consistently. For example:

• [Merged by Bors] - chore(Topology/MetricSpace/Closeds): rename lemmas about MetricSpace (NonemptyCompacts α) mathlib4#42774
• [Merged by Bors] - feat(Topology/InfiniteSum): applying the sum of functions mathlib4#42829
• [Merged by Bors] - refactor(Order): make CompletePartialOrder extend OrderBot mathlib4#34477
• [Merged by Bors] - chore(Algebra/Order/Monoid/Unbundled/Basic): golfing + formatting mathlib4#38227

[b-mehta]

Thanks for proposing this. I think it's good to document this, and start a discussion. I'm not sure, though, if this has been discussed before. Can you point me to a discussion that I missed, or start a brief one on Zulip?

Apologies, I accidentally made the PR before remembering to add the motivation. I have added motivation and some links to previous discussion in the description.

[grunweg]

Thanks for the explanation; that is very helpful. I find this idea reasonable, but also think it's good to draw wider attention to this. I've started a thread on Zulip: https://leanprover.zulipchat.com/#narrow/channel/345428-mathlib-reviewers/topic/Breaking.20change.20policy/with/622851226