search

leanprover-community / lean4-mode

Emacs major mode for Lean 4
https://leanprover.github.io/
Apache License 2.0
64 stars 27 forks source link

Failure of toolchain detection when `.elan` is a symlink #66

Open JLimperg opened 2 months ago

JLimperg commented 2 months ago

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 commented 2 months ago

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.