search

chanind / mathlib-changelog

https://mathlib-changelog.org
MIT License
10 stars 0 forks source link

Update to work with mathlib4 #11

Closed kim-em closed 1 year ago

kim-em commented 1 year ago

We're gradually phasing out mathlib and switching to mathlib4.

I'm going to remove the link to the changelog website from the sidebar of https://leanprover-community.github.io/, but of course it will still stay at https://leanprover-community.github.io/lean3

Please ping me (or just open a PR on the website) if an update to mathlib4 happens, and I'll restore the link in the webpage.

chanind commented 1 year ago

Sounds good, I'll let you know if I get some time to update this to v4 (or make a separate v4 version). Thanks for your work on lean!

faenuccio commented 1 year ago

Are you planning an update of your great tool to mathlib4?

chanind commented 1 year ago

Apologies for the delay - I add support for mathlib v4 at https://mathlib-changelog.org/v4. I didn't change any of the parsing logic, so it's likely that the v4 version may be missing some content due to not parsing the new syntax correctly. If you notice that, please open an issue here!