Setup lean4

Stream: lean4

[b38b]

I am a bit confused on how to setup lean4. I followed the instructions here: https://leanprover.github.io/lean4/doc/quickstart.html. It seems to work:

Screenshot-2023-08-22-at-15.47.11.png

However on a terminal lake or elan commands do not work, which seem necessary to create a project. What am I missing?

[b38b]

Oh, forgot to mention. I am on macOS (M2 series chip). I am using vscode.

[Alex J. Best]

Did you restart your terminal / open a new terminal?

[b38b]

Yes.

[Kevin Buzzard]

So which lake in a fresh terminal gives you...what? What do you mean by "do not work"?

That's a very old nightly by the way.

[b38b]

➜  ~ which lake
lake not found

[b38b]

That's a very old nightly by the way.

So how do I update it?

[b38b]

Ok so apparently lean4 (which I installed with vscode) put this in my .bash_profile:

export PATH="$HOME/.elan/bin:$PATH"

Problem is I'm using zsh (which is default in macOS). So I just moved that line to .zprofile instead. Now it recognizes the commands elan, lake.

[Kevin Buzzard]

Oh nice.

[Kevin Buzzard]

The version of Lean you use is determined by the version declared in the project you're working in. So maybe just now make a new project (now lake is working) and hopefully it will use a newish Lean.

[b38b]

Thanks

[Sebastian Ullrich]

Elan does modify .zprofile as well if SHELL during installation looks like *zsh*, but apparently that didn't work in this case