Mention Lean 4 somewhere in the Lean Community pages

Stream: new members

[Giovanni Mascellani]

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]

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

[Giovanni Mascellani]

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]

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

[Eric Wieser]

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]

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