Jump to definition across files, in lean4 repo

Stream: lean4

[Scott Morrison]

When I have the lean4 repository open in VSCode (where I've use elan override to tell the extension to use Lean 4), jump-to-definition (F12) works great with in a single file, but I just get No definition found for any definitions coming from imports.

Does this work for others? Is it a known problem?

[Mac]

@Scott Morrison nope, that has been my experience as well

[Mac]

I mentioned this in an older thread (see here), but @Mario Carneiro said it worked fined for him, so we were never able to hash out the problem.

[Scott Morrison]

I made an issue at https://github.com/leanprover/vscode-lean4/issues/77

[Mario Carneiro]

just pulled the latest lean, and it still seems to be working, although I forget if I have any relevant elan override settings

[Mario Carneiro]

$ elan override list
/home/mario/Documents/lean/lean4                leanprover/lean4:nightly
...

[Mac]

@Mario Carneiro, well that is probably why it is working -- it is not actually pointing to the custom Lean build as describing in dev setup for elan section of the manual

[Mario Carneiro]

ah right, I have not actually built lean

[Scott Morrison]

Yes, I'm seeing the same thing now. It works with the nightly, but not with a local toolchain.

[Mac]

if you look at to where its jumping to, you will probably notice it is going to the sources for the toolchain not those for the repo

[Mario Carneiro]

yes, that's right

[Mac]

that is not the goal XD

[Mario Carneiro]

I treat lean4 repo as read only anyway so it's not a big deal for me, but if the dev build version is broken then I guess that should be fixed

[Scott Morrison]

I've updated the desciption in the issue to reflect all this.

[Tomas Skrivan]

Yes I have the same problem. As a partial solution, I have set CMAKE_INSTALL_PREFIX to point to ~/.elan/toolchain and when rebuilding I run make install. Now jumping to definition works but jumps to the installed files in elan directory instead of the file in repo.

[Gabriel Ebner]

As posted on the vscode-lean4 issue, this is a known problem:

Local builds don't know where the sources are. There are several "solutions" for this:

• Set the LEAN_SRC_PATH environment variable.
• ln -s ~/lean4/src/ ~/lean4/build/release/stage1/lib/lean/

Ideally, they'd be able to figure out the source path automatically, but that's a lean4 issue not a vscode-lean4 one.

[Sebastian Ullrich]

Yes, the first bullet is documented at https://github.com/kha/lean4/blob/781a28b8f4badddbc01d1a8a6822128d5173c65a/doc/dev/index.md?plain=1#L30-L33. We could automate the second bullet in cmake on Unix platforms.

[Gabriel Ebner]

The symlink is not ideal either, because go-to-definition now goes to a different path than the actual source files. But it's definitely a less confusing out-of-the-box experience.

[Sebastian Ullrich]

Ahh... we could realPath it