Zulip Chat Archive

Stream: lean4

Topic: Go-to-definition in the standard library


view this post on Zulip Gabriel Ebner (Mar 11 2021 at 12:42):

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?

view this post on Zulip Gabriel Ebner (Mar 11 2021 at 12:45):

(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.)

view this post on Zulip Sebastian Ullrich (Mar 11 2021 at 12:52):

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 :) ...

view this post on Zulip Sebastian Ullrich (Mar 11 2021 at 12:53):

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

view this post on Zulip Gabriel Ebner (Mar 11 2021 at 12:57):

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

view this post on Zulip Gabriel Ebner (Mar 11 2021 at 12:58):

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.

view this post on Zulip Sebastian Ullrich (Mar 11 2021 at 13:02):

Gabriel Ebner said:

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

Then let's change that instead


Last updated: May 07 2021 at 12:15 UTC