Go-to-definition in the standard library

Stream: lean4

[Gabriel Ebner]

With development builds of Lean 4, go-to-definition only works with elaborate hacks (i.e., you need to set an environment variable depending on the build you're using). I was about to automatically set this environment variable in the vscode extension. But then I noticed that there is a much cleaner solution, which is already explicitly supported by the server:

ln -sr src build/release/stage1/lib/lean/src

Is there a reason the cmake build doesn't create this symlink by default?

[Gabriel Ebner]

(Admittedly, one downside is that vscode doesn't resolve the symlink after go-to-definition. So you end up editing files in build/release/stage1/lib/lean/src.)

[Sebastian Ullrich]

Gabriel Ebner said:

Is there a reason the cmake build doesn't create this symlink by default?

Part of the reason might be that I don't use the cmake build system anymore, so I wouldn't notice :) ...

[Sebastian Ullrich]

Gabriel Ebner said:

(Admittedly, one downside is that vscode doesn't resolve the symlink after go-to-definition. So you end up editing files in build/release/stage1/lib/lean/src.)

So should we do it only when LEAN_SRC_PATH is unset? Assuming that if it is set at cmake invocation, it is probably set in the editor as well

[Gabriel Ebner]

Surprisingly LEAN_SRC_PATH is used as a fallback and not as an override.

[Gabriel Ebner]

Sebastian Ullrich said:

So should we do it only when LEAN_SRC_PATH is unset? Assuming that if it is set at cmake invocation, it is probably set in the editor as well

That seems like a reasonable (though slightly surprising) compromise.

[Sebastian Ullrich]

Gabriel Ebner said:

Surprisingly LEAN_SRC_PATH is used as a fallback and not as an override.

Then let's change that instead