Zulip Chat Archive

Stream: general

Topic: Lean 4 released


Kevin Buzzard (Jan 04 2021 at 14:17):

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

Gabriel Ebner (Jan 04 2021 at 14:19):

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 (Jan 04 2021 at 14:21):

vscode-lean4 is probably of interest as well.

Bryan Gin-ge Chen (Jan 04 2021 at 14:27):

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

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

Kenny Lau (Jan 04 2021 at 14:28):

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

Bryan Gin-ge Chen (Jan 04 2021 at 14:36):

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

Kenny Lau (Jan 04 2021 at 14:46):

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

Adam Topaz (Jan 04 2021 at 14:48):

Is there a lean4-mode emacs package somewhere?

Bryan Gin-ge Chen (Jan 04 2021 at 14:50):

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

Marc Huisinga (Jan 04 2021 at 15:03):

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 (Jan 04 2021 at 15:33):

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 (Jan 04 2021 at 18:01):

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

Marc Huisinga (Jan 04 2021 at 18:02):

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

Julian Berman (Jan 04 2021 at 18:03):

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 (Jan 04 2021 at 18:05):

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 (Jan 05 2021 at 03:39):

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 (Jan 05 2021 at 04:37):

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 (Jan 05 2021 at 10:23):

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 (Jan 05 2021 at 11:00):

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

Sebastian Ullrich (Jan 05 2021 at 11:01):

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 (Jan 05 2021 at 11:50):

Created and added to default streams


Last updated: Dec 20 2023 at 11:08 UTC