Failure of toolchain detection when .elan is a symlink

[JLimperg]

Recently, when opening files in a Lean toolchain under .elan/, lean4-mode has reliably failed to start the server, with an error message from elan complaining that no default toolchain was configured. This is true and when I configured a default toolchain, the error went away, but then this toolchain would be started instead of the one to which the file belongs.

At that point, my .elan was a symlink to ~/somedir/.elan. When I removed the symlink and renamed the latter directory to .elan, the error went away. So I suspect that the toolchain detection logic checks whether a directory is under .elan/toolchains and gets confused when this is a symlink.

VSCode doesn't seem to have this issue, so maybe their detection logic can be reused.

[mekeor]

It'd be interesting which command lean4-mode uses to launch the language server. You could open the problematic file, then type M-: (lean4--server-cmd) RET (default binding for eval-expression) and copy the list of strings from the *Messages* buffer (which you can open with C-h e (default binding for view-echo-area-messages)) to share it with us.

[mekeor]

I was not able to reproduce the error: I made ~/.elan a symlink to ~/.elan.backup. I opened a file in ~/.elan/toolchains/leanprover--lean4---.../src/....lean and it works just fine.

Can you provide a minimal reproducing example?