Need to set elan override for Lean toolchain directories

Stream: lean4

[Jannis Limperg]

I'm using plain elan + Emacs for Lean 4 development. When I open a Core file in e.g. ~/.elan/toolchains/leanprover-lean4-nightly-2021-05-04/, LSP hangs indefinitely in the "starting" state. This is fixed if I elan override set leanprover/lean4:nightly-2021-05-04 in the toolchain directory, so it seems like elan/LSP can't figure out which Lean executable to use here. Is this an issue in VSCode as well? Should elan automatically set an override for these toolchain directories?

[Sebastian Ullrich]

Did you open it as a workspace? I usually select [n]o when lsp-mode asks me for an installed stdlib, which should prevent the LSP from being started. It's a bit more explicit in VS Code, you need to open src/ as a folder (and there's a known issue with multiple workspaces).

[Sebastian Ullrich]

I'm open to a PR for defaulting elan in those directories. I wonder why it wasn't done in rustup.

[Jannis Limperg]

That's the next issue (which I just discovered): I'd like to have the stdlib as a workspace so that go-to-definition works. But each time I open a different stdlib file, it asks me for the workspace root again. I'll experiment a bit, see if that can be fixed.

[Sebastian Ullrich]

Maybe it's opening the wrong folder as a namespace? As I said, it should be src/. Not sure if we can give lsp-mode any hints there.

[Jannis Limperg]

The workspace issue is now fixed for me. I think this was because I had my .elan behind a symlink, so LSP may have thought that the files I opened weren't in a subdirectory of the workspace dir. Don't know how much work it would be to have LSP auto-configure the workspace, but if I need to do it only once, it's not much of a hassle. Thanks for helping with the debugging by the way!