dev setup for vscode: goto definition finds nightly

Stream: lean4

[Mario Carneiro]

I've been trying to follow the instructions at https://leanprover.github.io/lean4/doc/dev/index.html#dev-setup-using-elan for setting up goto definition to lead back into the src directory of lean4, without luck. After following the instructions, lean --version or lean +lean4 --version shows the master branch as expected, but the vscode seems to be running the nightly version instead of stage1 and go to definition takes me into the nightly sources in elan instead of src. I got it to work by setting the "Lean4: Toolchain Path" to /home/mario/Documents/lean/lean4/build/release/stage1 (the full path seems to be required), but I can't help but think there's something wrong with the setup.

[Mario Carneiro]

Actually I don't think that's right either. Using stage1 causes the definition links to not get updated when I edit the file, and stage0 has updated link locations but strangely the definitions themselves will not update. (For example, if I add a field to a structure then in a downstream file #print Foo.oldField will have the new span of the field but #print Foo.newField will still be an error.)

[Mac]

Mario Carneiro said:

stage0 has updated link locations but strangely the definitions themselves will not update.

Yep, this is the expected behavior afaik. You have to rebuild Lean after making modifications for them to be recognized by the Lean 4 server / VSCode. At least that is my experience.

[Sebastian Ullrich]

If lean uses the correct version but VS Code in the same directory does not, that sounds like a bug in vscode-lean4