Zulip Chat Archive

Stream: new members

Topic: Mention Lean 4 somewhere in the Lean Community pages

Giovanni Mascellani (May 02 2023 at 20:20):

The pages in https://leanprover-community.github.io/ (especially https://leanprover-community.github.io/get_started.html) bear no mention of Lean 4 and mathlib4. I don't know if the eventual fate of mathlib (for Lean 3) is to be deprecated and abandoned, or if the idea is to keep mathlib and mathlib4 around together for at least some time, but it would perhaps be less confusing for newcomers be informed about what's going on and to have a few links about learning Lean 4, or pivoting from Lean 3 to Lean 4.

Patrick Massot (May 02 2023 at 20:21):

Yes, we are sorry about that. We've been talking about this issue, but the current state is still what you describe.

Giovanni Mascellani (May 02 2023 at 20:24):

Thanks! And BTW I didn't mean to complain, rather to give a feedback. About my question, is the idea to keep mathlib around after mathlib4 is in sync, or will it be dropped?

Johan Commelin (May 02 2023 at 20:25):

It will archived: available for projects that still depend on it, but no longer actively developed.

Eric Wieser (May 02 2023 at 20:33):

Morally archived but perhaps not github-archived; archiving it makes it impossible to comment on any old PRs, which can be helpful for pinging old authors

Notification Bot (May 02 2023 at 23:32):

9 messages were moved from this topic to #mathlib4 > putting mathlib3 in the git history by Eric Wieser.

Last updated: Dec 20 2023 at 11:08 UTC