Unable to update Lean4

Stream: new members

[Aatman Supkar]

Hi guys!
I had installed Lean4 roughly a year ago via VS Code. I returned to it today, and I tried following the instructions from here. Unfortunately, When I try the 'install Lean Version Manager' step, the terminal opens, does something, and before I can read anything, it closes.

In the end, the project that I make does not run. What should I be doing? I'm not even sure about what information I should be informing you guys, at this point, because I don't have an error code from the entire process.

[Eric Wieser]

Are you able to screenrecord it opening and closing?

[Eric Wieser]

It sounds like you might be opening it in a strange way

[Eric Wieser]

And if not, the screen recording would at least let you see what the message was!

[Aatman Supkar]

image.png
The terminal stopped closing at the end, it seems. So here's a screenshot. Does it do any good?

[Richard Copley]

Will you please try the same thing a few more times? Downloads from Github (the plucky little underdog) can sometimes be unreliable.

[Aatman Supkar]

image.png
I genuinely have no idea what has changed (I just did the elan reinstall multiple times, as you insisted). But do I take this as a definitive sign of everything working?

[Richard Copley]

Looks good to me :smile: . The difference is just that a download from Github (which should not have failed) didn't fail.

[Aatman Supkar]

Okay, one last thing. I just want to be really sure I have the current version of Lean and not the one I had from my last year's install. What version of Lean4 should I be expecting? Running lean --version returns

Lean (version 4.13.0-rc3, arm64-apple-darwin23.6.0, commit 01d414ac36dc, Release)

[Aatman Supkar]

(deleted)

[Richard Copley]

Aatman Supkar said:

Okay, one last thing. I just want to be really sure I have the current version of Lean and not the one I had from my last year's install. What version of Lean4 should I be expecting? Running lean --version returns

Lean (version 4.13.0-rc3, arm64-apple-darwin23.6.0, commit 01d414ac36dc, Release)

You'll have several different versions of lean by now. The version of lean which is specified in the lakefile.lean or lakefile.toml of the project you have opened will be automatically installed by elan. If you don't have the version you need, you will know, because the infoview in VS code will not work.

What version lean --version reports depends on where you execute it (the lean binary on your search path is a link to or a copy of the elan binary; elan examines the environment and executes the appropriate version).

Version 4.13.0-rc3 is the latest version.

[Aatman Supkar]

Okay, the final issue seems to be ridiculous. I just have to wait for quite long. There was no indication that it wasn't done 'starting' in any sense.

[Aatman Supkar]

Richard Copley said:

Aatman Supkar said:

Okay, one last thing. I just want to be really sure I have the current version of Lean and not the one I had from my last year's install. What version of Lean4 should I be expecting? Running lean --version returns

Lean (version 4.13.0-rc3, arm64-apple-darwin23.6.0, commit 01d414ac36dc, Release)

You'll have several different versions of lean by now. The version of lean which is specified in the lakefile.lean or lakefile.toml of the project you have opened will be automatically installed by elan. If you don't have the version you need, you will know, because the infoview in VS code will not work.

What version lean --version reports depends on where you execute it (the lean binary on your search path is a link to or a copy of the elan binary; elan examines the environment and executes the appropriate version).

Version 4.13.0-rc3 is the latest version.

Got it, thank you so much!