Lean 4 released

Stream: general

[Kevin Buzzard]

For those of you not following the rss stream, Lean 4 has just been released!

[Gabriel Ebner]

I believe the -M1 suffix means it's still a milestone (i.e. beta) release. But I'm sure we'll hear more concrete details later today.

[Bryan Gin-ge Chen]

vscode-lean4 is probably of interest as well.

[Bryan Gin-ge Chen]

There's a short "release post" for Lean 4.0.0-m1 here.

edit: link fixed per Marc Huisinga's post below.

[Kenny Lau]

Do we have a Lean 4 Zulip stream? I'll have 100000 questions to ask.

[Bryan Gin-ge Chen]

I think separate topics for each question in the #general stream is fine, but maybe there are other opinions.

[Kenny Lau]

I would rather have centralized stream for every Lean 4 question for easy accessibility

[Adam Topaz]

Is there a lean4-mode emacs package somewhere?

[Bryan Gin-ge Chen]

It looks like it's in the lean4 repository: https://github.com/leanprover/lean4/tree/master/lean4-mode

[Marc Huisinga]

Bryan Gin-ge Chen said:

There's a short "release post" for Lean 4.0.0-M1 here.

the release post can now be found here: https://github.com/leanprover/lean4/releases/tag/v4.0.0-m1 :)

[Bryan Gin-ge Chen]

In case it's helpful for others, here are the steps I took to get a Lean 4 project up and running with vscode-lean4.

First, clone your favorite Lean 4 project, e.g. advent-of-lean-4:

git clone https://github.com/rwbarton/advent-of-lean-4.git

Then install lean4 using elan:

elan install leanprover/lean4:4.0.0-m1

Navigate to your lean4 project directory, set an override for the Lean version, and open VS Code:

cd advent-of-lean-4
elan override set leanprover-lean4-4.0.0-m1
code .

Open the extensions tab in VS Code, search for vscode-lean4 and install it. It seems to override vscode-lean in all Lean projects, so for now I've disabled it globally and enabled it only in this workspace.

The extension should run when you open a .lean file and you can test the features mentioned in the README. For example, you can go through each of the files in advent-of-lean-4 and make the (relatively straightforward) fixes to get it to work with 4.0.0-m1.

[Julian Berman]

Does hover support work (I guess that's a question for anyone who got things set up in emacs)

[Marc Huisinga]

not yet! it's being worked on, though :)

[Julian Berman]

Ah awesome thanks! k, just wanted to make sure I wasn't missing something -- just also saw the list of functionality in https://github.com/mhuisi/vscode-lean4 too

[Julian Berman]

While I'm at it.. is there a decent way to decide whether to run Lean 3 or lean 4? I guess a way is "try to load a leanpkg.toml and read the version out of that, and fallback to lean4 maybe?"?

[Kevin Sullivan]

On OSX just now. I don't know what the problem is.

elan install leanprover/lean4:4.0.0-m1
error: toolchain 'leanprover-lean4-4.0.0-m1' is not installed

[Alex J. Best]

Kevin Sullivan said:

On OSX just now. I don't know what the problem is.

elan install leanprover/lean4:4.0.0-m1
error: toolchain 'leanprover-lean4-4.0.0-m1' is not installed

I tried this on osx big sur and on windows and it worked fine, you could try updating or reinstalling elan (and move your ~/.elan directory elsewhere to clear out all the old stuff)?

[Sebastian Ullrich]

Kenny Lau said:

I would rather have centralized stream for every Lean 4 question for easy accessibility

That's probably a good idea. I don't remember, if we add all current members to the stream during stream creation, do they all get mailed :laughter_tears: ? Or was that only when adding people after the stream has been created?

[Mario Carneiro]

I don't think it's a bad idea to mail everyone in this particular instance

[Sebastian Ullrich]

Alright, I'll go ahead and create #lean4 then... after moving a certain private channel with the same name out of the way

[Sebastian Ullrich]

Created and added to default streams