How to install Lean 4?

Stream: lean4

[Kenny Lau]

Bryan Gin-ge Chen said:

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

Update elan if you haven’t recently:

elan self update

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. Also, vscode-lean should also be disabled in Lean 4 projects, otherwise unicode shortcuts don't seem to work.

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.

edit: added reminder to update elan.
edit 2: added note about disabling vscode-lean to get unicode translation to work.

[Reid Barton]

I added a leanpkg.toml file to advent-of-lean-4 and fixed the programs that needed fixing, so a couple of the steps above can be skipped now.

[Gihan Marasingha]

Using vscode, how do I evaluate the 'main' function in a Lean file (assuming that question makes sense)? E.g. 1/a.leanin advent-of-lean-4.

[Johan Commelin]

#eval main?

[Gihan Marasingha]

I get an error message failed to synthesize Lean.Eval (List String → IO UInt32) when I try that.

[Reid Barton]

I don't know how to do it in vscode, but from the command line you can run lean --run 1/a.lean

[Gihan Marasingha]

@Reid Barton Thanks. Do I need to build the project first? I'm getting an error message about no such file a.in.

[Reid Barton]

You need an input file such as the one provided by https://adventofcode.com/2020/day/1

[Gihan Marasingha]

Oh, thanks!

[Gihan Marasingha]

Duh, I hadn't actually read the code.

[James Caldwell]

I'm running Ubuntu. I have had a lot of trouble getting to this point. I have elan installed and vs code with the lean extension. When I load a simple file that I have seen running in lean, vs code gets stuck with the perpetual message "Waiting for Lean server to start..."

λ > which lean
/home/jlc/.elan/bin/lean
λ > cd ~/.elan/bin/
λ > ls
elan lake lean leanc leanchecker leanmake leanpkg
λ >

Any ideas what tio try next?

[Adam Topaz]

Just to be sure, are you trying to isntall lean4?

[James Caldwell]

Yes - lean4.

[James Caldwell]

Sorry for the delay ... I took a break.

[Arthur Paulino]

Do you have a Lean 4 toolchain? What does elan toolchain list show?

[James Caldwell]

λ > elan toolchain list
stable (default)
leanprover/lean4:4.0.0-m1
leanprover/lean4:4.0.0-m3
leanprover/lean4:nightly
leanprover/lean4:stable
λ >

[Arthur Paulino]

Do you have a Lean 4 project you want to open? Or do you want to start a project from scratch?

[James Caldwell]

Start a new one.

[James Caldwell]

Here's the director I'm working in.

ls -al
total 32
drwxrwxr-x 3 jlc jlc 4096 Mar 2 14:56 .
drwxrwxr-x 4 jlc jlc 4096 Mar 2 14:51 ..
drwxrwxr-x 7 jlc jlc 4096 Mar 2 14:56 .git
-rw-rw-r-- 1 jlc jlc 54 Mar 2 14:56 .gitignore
-rw-rw-r-- 1 jlc jlc 2522 Feb 23 15:07 GodelGentzen.lean
-rw-rw-r-- 1 jlc jlc 227 Mar 2 14:56 lakefile.lean
-rw-rw-r-- 1 jlc jlc 76 Mar 2 14:56 Main.lean
-rw-rw-r-- 1 jlc jlc 20 Mar 2 14:56 Translations.lean
λ >

[Adam Topaz]

Did you install the lean4 vscode extension?

[Adam Topaz]

In any case, you should open the project folder itself in vscode, not individual files

[Arthur Paulino]

You're missing a lean-toolchain file. Example: https://github.com/leanprover-community/mathlib4/blob/master/lean-toolchain

[James Caldwell]

Yes - when I open the file GodelGentzen.lean .... that's when it fails to start lean.

[James Caldwell]

OK - what do I need to do to get it?

[Adam Topaz]

Will lake init do it? I'm not sure. The usual way to start new projects is lake new, and that will add all the necessary files. I don't know how youb obtained this folder without a toolchain file.

[James Caldwell]

I sucessfully ran "lake int translations" earlier ... when I try to run it again I'm told I already ran it.

[James Caldwell]

I created the folder and copied the file GodelGentzen.lean into it.

[Arthur Paulino]

I think you ran with an old toolchain. Try deleting your current folder, run elan default leanprover/lean4:nightly-2023-02-24 and then run the lake init command again

[Arthur Paulino]

Actually, run lake new instead of lake init

[Arthur Paulino]

lake new SomeProjectName

[James Caldwell]

I just hit CR on the lake init ... should I do lake new?

[Arthur Paulino]

Hmm, if your folder is not a mess at this point you should be fine

[James Caldwell]

Also, should I be in the folder when I run it ... or one level up?

[Arthur Paulino]

lake init turns your current folder into a Lake project. lake new creates a new folder

[Arthur Paulino]

But if you ran lake init then you should be ready to kickoff VS Code with code .

[James Caldwell]

OK - I want it to be a level down so I ran "lake new tranbslations". I'm going down into translations and starting vscode.

[James Caldwell]

It works! Thank you so much.