mathlib4 changelog

Stream: general

[Riccardo Brasca]

Do we have anything like mathlib changelog for mathlib4?

[Scott Morrison]

No

[Oliver Nash]

The author sounds like they might make a mathlib4 version if they received sufficient encouragement: https://github.com/chanind/mathlib-changelog/issues/11

[David Chanin]

Apologies for the delay updating the site, I added mathlib v4 support at https://mathlib-changelog.org/v4. I didn't change any of the parsing logic to extract theorems, defs, lemmas etc from lean commits, so I suspect there's probably some bugs where it's not picking up 100% of the stuff it should be. If you give it a try and find any issues with the v4 version, let me know or open an issue on the Github repo!

[Patrick Massot]

Thanks!

[Scott Morrison]

This is great, thanks. I'd suggest just switching / to point directly to /v4 already: we're not going back. :-)

[Junyan Xu]

Great stuff, thanks!
Two comments: 1. the Github link at the top right corner is broken. 2. I think the #aligns could be used to connect mathlib4 history with mathlib3's. (Should we also index std4/lean4/lean3 together?)

[David Chanin]

Good catch on the Github link! Parsing the #align should be doable, I'll add that to the backlog. For std4, you mean also including the lean4 std lib?

[Junyan Xu]

Yeah, I say this because we frequently upstream lemmas from mathlib4 to std4.

[Alex J. Best]

Do you have an estimate for when you want to move v4 to be the default (I'd say the sooner the better)?

[Alex J. Best]

Though maybe we should wait for the big git history merge

[David Chanin]

I can change the default today if it looks good enough. What's the big git history merge?

[Johan Commelin]

At some point we might merge mathlib3 and mathlib4 git histories. This has been discussed, but there is not yet a concrete plan/date.

[Eric Wieser]

I have a concrete plan but haven't had time to write it up fully

[Eric Wieser]

The mathlib4 wiki already has a short explanation

[Ruben Van de Velde]

If we want to do it, shouldn't we do it asap?

[Eric Wieser]

No, that's explained in the wiki page

[Eric Wieser]

If someone not on mobile could link it, that would be great!

[Ruben Van de Velde]

https://github.com/leanprover-community/mathlib/wiki/Merging-github-repos-and-history

[David Chanin]

It looks like whichever path is chosen, I don't think it will affect the changelog that much. We'll probably just have to clear the crawl cache in the changelog and regenerate the changelog from scratch after the merge, but that's not a big deal

[David Chanin]

I guess a bigger issue might be if the changelog diff parsing changes between v3 and v4, since then we'd have v3 and v4 lean files in the same repo. Even then, I feel like it shouldn't be a huge deal, we'd just need to note which commit is the separator between lean3 and lean4 files

[Eric Wieser]

What's missing from that document currently is that I intend to add some intermediate steps after "mathport output" so that git can understand the history

[Eric Wieser]

Most likely "rename all the files to have their mathlib4 names"

[Eric Wieser]

Otherwise it will see most files as a deletion+creation instead of a move+rewrite.

[Julian Berman]

Are you sure that will help? Git of course doesn't have any notion of renames anyhow, it's all heuristics.

[Eric Wieser]

Yes, I'm certain it will because I am specifically targeting those heuristics

[David Chanin]

The changelog now defaults to v4