quickstart fails

Stream: lean4

[Bjørn Remseth]

Hi. I'm trying to install lean4 using the instructions in https://leanprover.github.io/lean4/doc/quickstart.html, but it fails. First the "install Lean using Elan" dialogue failed to pop up. I then tried to install lean by copying a binary from the dristibution and pointing som e variables at it, but got image.png ... so I don't understand what's going on. Does anyone have any hints?

[Andrés Goens]

it looks like there's a lean server running there, it just doesn't know that identifier. Did you install the "lean4" extension or the "lean" extension?

[Bjørn Remseth]

the lean4 extension

[Bjørn Remseth]

I also deleted an old .elan directory, and a full installation of a new lean was triggered mroe or less as described in the quickstart.html file
("more or less" since the dialogue didn't look identical, but I was prompted to use elan to install)

[Andrés Goens]

I actually get the same message, I think that Lake.leanVersionString just doesn't exist (anymore?)

[Andrés Goens]

but your installation is probably fine

[Bjørn Remseth]

Yay ;-) I suppose that is good news

[Bjørn Remseth]

Ok, then I will assume that things are working, try a few more examples and report back to this chat. Thank you for your help so far :-)

[Bjørn Remseth]

Yup. Seems to be working. Documentation was wrong :-) Thanks^2

[Martin Dvořák]

Should we remove the step (4) from the documentation? Is it outdated?

[Horațiu Cheval]

For me the linked quickstart page shows

import Lean
#eval Lean.versionString

as a test program, not Lake.leanVersionStrong