Lean 3 vs Lean 4

Stream: Zulip meta

[Martin Dvořák]

I think we should reëvaluate which version of Lean is the default outside of the streams lean4 and mathlib4. Possibly we could create a separate stream for Lean 3 since Lean 4 has gained a lot of popularity recently.

[Marcus Rossel]

I think the natural point to switch the default is when Lean 4 is released.

[Kevin Buzzard]

A related question is whether we should split the #mathlib4 stream into a porting stream and another stream

[Martin Dvořák]

Marcus Rossel said:

I think the natural point to switch the default is when Lean 4 is released.

In what sense is Lean 4 "not released" now?

[Johan Commelin]

See the first line of https://github.com/leanprover/lean4/

[Johan Commelin]

See also https://github.com/leanprover/lean4/releases

[Bulhwi Cha]

When will the first stable release of Lean 4 come out?

[Kevin Buzzard]

When it comes out.

[Kevin Buzzard]

We will let the devs decide when they are happy.

[Mario Carneiro]

mathlib4 being (mostly) ported is likely to be a prerequisite for the release

[Martin Dvořák]

If I understand correctly, we shouldn't ask Lean 4 questions in the "Is there code for X?" stream. The only streams for questions about Lean 4 are lean4 and mathlib4.

[Eric Wieser]

I think generally "is there code for X" is usually for "does this exist in mathlib", although occasionally is fishing for links to people's external projects.

[Eric Wieser]

And of course anything that exists in mathlib4 today likely also exists in mathlib3

[Johan Commelin]

I think #lean4 is fine for this sort of questions. Once it becomes high traffic we can think about how to split the stream.

[Martin Dvořák]

Eric Wieser said:

I think generally "is there code for X" is usually for "does this exist in mathlib", although occasionally is fishing for links to people's external projects.

So if I want to know only about stuff that is available when using Lean 4, I shouldn't ask there. Sounds reasonable.

[Martin Dvořák]

Is Lean 4 the default in all channels now?

[Kevin Buzzard]

Depends on who you ask, probably, but if you're asking me then the answer is "yes".

[Scott Morrison]

Yes. I think we can safely include in answers to any Lean 3 specific questions a suggestion that the user migrate!

[Martin Dvořák]

I think we should create a lean3 stream and defer all questions about Lean 3 (such that "switch to Lean 4" is not a desirable answer) to it.

[Scott Morrison]

I'd prefer to see a nontrivial number of examples of such before devoting a stream to it.

[Timo Carlin-Burns]

Now that Lean 4 is released and lean 3 is deprecated, what's the difference between #general and #lean4?

[Scott Morrison]

My take is that #lean4 is about implementation of the Lean 4 language, rather than using it.

[Timo Carlin-Burns]

then what's #lean4 dev?

[Mario Carneiro]

not very active

[Mario Carneiro]

but historically it has been used for questions about how to develop in the lean4 repo itself

[Mario Carneiro]

RFC style questions and suggestions for language changes usually go in #lean4