Installation: Interesting elan errors

Stream: lean4

[Henrik Böving]

First I bring some positive news, we just installed Lean 4 (among a few other proof assistants) here: https://itp-school-2023.github.io/ in a crowd consisting mainly of mathematicians and so far only one person has had an issue! (that I know of^^)

Now for the interesting issue. The person was running on an M1 and tried to install elan through the brew install elan-init procedure, this procedure did succeed. She then tried to open a Lean file, installed the extension and got the "waiting for language server to start" popup which did not go away anymore. After a bit of debugging I noticed that
her elan kept reporting that it could not find binaries for Lean 4 for this architecture. As it turns out the elan that she was calling was still at version 0.7.5 from 2019 (current is 3.0.0) despite brew reporting an installed version of 3.0.0. So why is this:
Brew installs elan to /usr/local/somewhere while the elan she was running was in ~/.elan/bin/elan so apparently a very old version of an earlier experiment. In addition to that 0.7.5 is so old that it could not elan self update anymore to maneuver out of this situation.

I don't quite know how we can help mathematicians to get out of this error on their own, they would have to notice the presence of two elans on their machine and remove one of them.

That said what I do think we can improve is the behavior of the LSP. I don't know why it believes that it is waiting for a lean server to start and I haven't reproduced the error yet locally due to lack of time. But it would be nice if people that know about this part of the vscode plugin could try to reproduce this and make this error out so the user is at least aware of the fact that things are broken.

[Marc Huisinga]

The "Waiting for language server to start"-issue is similar to vscode-lean4#323, so I'll add it there. Error messages in the VSCode extension could be much better in general.

[Julian Berman]

I don't quite know how we can help mathematicians to get out of this error on their own, they would have to notice the presence of two elans on their machine and remove one of them.

Detecting this itself is not very hard, the question for this bit perhaps is where to put the check so it's seeable but not intrusive? Specifically type -a elan and/or type -a lean will tell someone how many elans and leans they've got on their path, perhaps elan should warn if it sees multiple versions of itself available?

[Julian Berman]

(If that check was in elan I guess it'd happen by walking PATH directly of course rather than via the shell builtin)

[Kevin Buzzard]

People who tried Lean once in 2018 are amongst the hardest to debug. I once had a student for whom nothing worked and it turned out that they had changed the default link to the lean exe in VS Code because at some point you had to do things like this.

[Scott Morrison]

These sort of problems should mostly be solved in the VSCode extension, and happily @Marc Huisinga working hard on making the extension more helpful during installation.

The extension is the obvious place that can run automatic checks that elan, lean, lake are sane, and give suggestions to the user when they are not.