Stable Release of Lean 4

Stream: lean4

[Evan Greenup]

Is there any release schedule for the first stable release of Lean 4?

[Mario Carneiro]

not with dates on it

[Mario Carneiro]

But there are some general milestones in terms of things that need to happen before we think it is ready, the main one being mathlib4 getting ported (not because it is specifically important to lean4 the language but because it is a large and important test case as well as the source of a lot of lean4-related documentation)

[Mario Carneiro]

But I'm not the one in charge of the release schedule, this is just my read on things

[Mario Carneiro]

I'm not sure whether the new compiler is planned for before or after the stable release

[Mario Carneiro]

cc: @Leonardo de Moura

[Kevin Buzzard]

To give a guess for a time on mathlib4 being ported, it looks like it will all be over bar the shouting in a couple of weeks. There will probably be some debate about what "finished" means (all of /src? all of /src and all of the IMO problems/counterexamples? etc etc) and there will be a lot of triaging of porting notes which will need thinking about, but in all reasonable measures of the problem we are "nearly there" in the sense that the vast majority of the work seems to be done now and the current speed of porting remains high.

[Scott Morrison]

I compared being "finished" with the port as like climbing a mountain. We're very close to the summit, but even we get there, we still need to climb back down the other side. All those porting notes are going to take some time.

[Ruben Van de Velde]

And there's a bunch of files that have in-progress PRs with more or less painful issues, so we may end up slowing down as these become blockers

[Joseph Myers]

And all the documentation on the website needs updating for Lean 4, including e.g. updating 100.yaml and undergrad.yaml for the new names of all the results and definitions referenced, etc.

[Evan Greenup]

In Lean 4, the leanc command will compile a lean source file to a machine code. Is that correct?

[Henrik Böving]

No its a modified C compiler