Zulip Chat Archive

Stream: lean4

Topic: How to install Lean 4?


view this post on Zulip Kenny Lau (Jan 05 2021 at 11:51):

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.

view this post on Zulip Reid Barton (Jan 05 2021 at 16:39):

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.

view this post on Zulip Gihan Marasingha (Jan 06 2021 at 17:32):

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.

view this post on Zulip Johan Commelin (Jan 06 2021 at 17:39):

#eval main?

view this post on Zulip Gihan Marasingha (Jan 06 2021 at 17:55):

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

view this post on Zulip Reid Barton (Jan 06 2021 at 18:04):

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

view this post on Zulip Gihan Marasingha (Jan 06 2021 at 18:07):

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

view this post on Zulip Reid Barton (Jan 06 2021 at 18:07):

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

view this post on Zulip Gihan Marasingha (Jan 06 2021 at 18:08):

Oh, thanks!

view this post on Zulip Gihan Marasingha (Jan 06 2021 at 18:08):

Duh, I hadn't actually read the code.


Last updated: May 07 2021 at 12:15 UTC