Imports and jump-to-def in lean4 repo (VS code)

Stream: lean4 dev

[Thomas Murrills]

I noticed that when working on a lean4 PR, if I command-click to jump to a def, it jumps to the source in the toolchain, not the repo I'm working in. Likewise, changing something in an imported file doesn't affect the environment when editing files which import those modified files, as they seem to import from the toolchain, not the local repo.

Is this a known issue? Is there a simple workaround or change I need to make somewhere?

(I'm guessing this is not possible for some files needed for bootstrapping, but I wonder if it's possible for every other lean4 file. Or is every file in core somehow involved in that process? I don't know how exactly bootstrapping works in this context.)

[Scott Morrison]

When working in the Lean4 repo, you should use elan override, per https://lean-lang.org/lean4/doc/dev/index.html

Does that help?