Go to definition not working in Lean 4 repository

[semorrison]

To work on the Lean 4 repository in VSCode, we have to run elan override set to point to an appropriate toolchain.

This allows editing .lean files with server support, and go-to-definition (F12) works within a file.

Depending on which toolchain we use, go-to-definition may or may not work for definitions in imported files.
If we use a nightly, then go-to-definition works, but the .lean files that it jumps to are taken from .elan/toolchains, rather than the local build.

If we use a toolchain pointing to the local build, per the instructions

elan toolchain link lean4 build/release/stage1
elan override set lean4

then go-to-definition does not work at all across files.

[semorrison]

Discussed on zulip here and here.

[gebner]

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.

[gebner]

Sebastian fixed this by creating the src symlink in cmake.