Changelog of non-BC changes?

Stream: mathlib4

[Yury G. Kudryashov]

After the port-induced refactor ban will be lifted, I expect quite a few refactors. I suggest that every non-bc commit must include a ###API Changes section in the description that (a) explains what changed; (b) if needed, gives hints about forward-porting for external projects that depend on mathlib. E.g., "generalized lemma A to lemma B".

Then we can have an autogenerated webpage that lists only these secitons (with "API Changes" replaced with the PR title & date).
What do you think about it?

[James Gallicchio]

I'd somewhat rather do the software engineering thing and have @[deprecated "Use blah.blah.blah instead"] annotations. But that requires having a deprecation cycle, which is admittedly a bit of a headache.

[James Gallicchio]

(and prevents using the same name in a refactor, though that might be a good thing)

[Jireh Loreaux]

I really don't want to do this via deprecation. Mathlib just changes too fast for that. An API Changes section in each PR description (for which it is relevant) seems reasonable, but why not just use mathlib-changelog? Isn't that what it's for essentially?

[Kyle Miller]

Mathlib's not afraid to make backwards-incompatible changes (we even have tools like #changelog to help for mathlib3). It's nice that we're able to converge on the "right" design for the math library. Most refactors are not a matter of deprecating an old definition or lemma, so I don't think @[deprecated] suffices.

I like the idea of doing this as messages in PR descriptions, though it'd be nice to have some tooling to help make sure this message actually covers the changes to the API (and helps write the section).

[James Gallicchio]

What about a different annotation that specifies what changed from version X? Something like @[changes_since <commit> "blah blah blah"]. Annotations are just so much easier to build tooling for...

[Kyle Miller]

(@James Gallicchio You mentioned yesterday that you're a non-mathlib user. Mathlib is different from most software engineering projects I think, so beware that wisdom you might have about software engineering may or may not apply here.)

[James Gallicchio]

I've unfortunately become a mathlib user because so many useful tactics are still locked in mathlib land :rofl: but you're right that I'm almost definitely concerned about a different subset of mathlib than most its users.

[Kyle Miller]

One big difference is that mathlib is meant to be a mono-repo, and while downstream projects are tolerated, it's preferred that they become part of mathlib.

[Kyle Miller]

Having a changelog is to help users get their projects onto the newest mathlib, to help get things into a state that they can contribute.

[Kyle Miller]

(I worry about too much math finding its way into Std, because this will make it harder for us to do big refactors. We spent time moving things out of Lean 3 core into mathlib3 for this reason.)

[James Gallicchio]

how was the mathlib3 changelog info for #changelog stored?

[Mario Carneiro]

Kyle Miller said:

(I worry about too much math finding its way into Std, because this will make it harder for us to do big refactors. We spent time moving things out of Lean 3 core into mathlib3 for this reason.)

I think we should try to restrict the things that are migrated to "refactor-resistant" mathematics. It should be something we are pretty okay sticking with long term, because I want Std to have an actual stability policy eventually (maybe not now, but once lean gets a stable release).

[Mario Carneiro]

This is also part of the reason I am avoiding the whole mathlib typeclass hierarchy, because this is refactored every tuesday

[Scott Morrison]

James Gallicchio said:

how was the mathlib3 changelog info for #changelog stored?

My understanding is that this is entirely automated: it parses the git diffs!

[Yury G. Kudryashov]

As for parsing git diffs, I can do git log -S lemma_name, find a commit, then try to understand what happened there.

[James Gallicchio]

It would be nice to have any changelog information right in the editor, though I'm not super sure how you might accomplish that

[Mario Carneiro]

git blame?

[Yury G. Kudryashov]

When you port something on top of a new mathlib, a common situation is "lemma no longer exists".

[Yury G. Kudryashov]

A less common situation is "your notation no longer works" (see norm notation).