jump to definition weirdness

Stream: lean4

[Kevin Buzzard]

Can anyone else reproduce this? I've had this problem for ages with this repo. It's kind of a magic trick.

Step 1: surf your way to https://github.com/kbuzzard/MweSkeletons and install the repo. It has mathlib as a dependency (for convenience when minimising, the purpose of this repo) but if you click around the files in the repo you'll convince yourself that no mathlib file is ever imported.

Step 2: fire up the repo and open the file MweSkeletons.broken_jump_to_def

Step 3: Verify that the only import in that file is MweSkeletons.CommRing which itself has no imports at all (it builds up a chunk of the alegbra heirarchy up to about CommRing).

Step 4: In the #check CommRing in that file, observe that hovering over CommRing tells you that it's coming from file MweSkeletons.CommRing, as expected. Now, make sure that the file MweSkeletons.CommRing isn't open in VS Code.

Step 5: Now jump to definition :tada: Thank you very much, I've been Kevin Buzzard and you are now in mathlib.

[Kevin Buzzard]

Oh -- much easier repro: fire up a local copy of mathlib, make two new files Mathlib/foo.lean containing def CommRing := Nat and Mathlib/bar.lean containing two lines import Mathlib.foo and then #check CommRing, make sure foo isn't open in VS Code and then go to step 4 above. Lean jumps to the wrong CommRing. Here I'm a bit more confused about things because you shouldn't have two definitions of CommRing in one repo I guess...

[Kevin Buzzard]

(this all stems from trying to minimise this BTW, this "feature" is a real pain when manually minimising).

[Adam Topaz]

trying it now... should I really click "Yes, I trust the authors"? ;)

[Kevin Buzzard]

ha ha, there is nothing up my sleeve! You can just try it with mathlib if you like :-)

[Adam Topaz]

for me it jumps to the definition in the repo

[Kevin Buzzard]

?! Are you sure you had the correct target file closed in VS Code when you jumped? It works for me iff the correct file is open.

[Adam Topaz]

... now it just jumped to mathlib.

[Adam Topaz]

WTF

[Kevin Buzzard]

Wooah -- for me it's just started jumping to the repo CommRing?!

[Adam Topaz]

wait, now I restarted vscode and it jumped to the correct place again

[Adam Topaz]

something really strange is happening!

[Kevin Buzzard]

Looks like it's not the most reliable of magic tricks but still...

[Adam Topaz]

I can't get it to jump to mathlib anymore

[Kevin Buzzard]

Maybe it never happened

[Kevin Buzzard]

Yeah, I can't get it to happen either. Maybe it depends on how many minutes past the hour you are or something.

[Adam Topaz]

Peek-2024-02-02-16-30.gif

[Adam Topaz]

now it's backwards

[Kevin Buzzard]

wooah I've never got the import statement on hover to be mathlib.

[Adam Topaz]

I switched the import!

[Kevin Buzzard]

So the hover always indicates the correct import, but the CommRing which you land on is random.

[Adam Topaz]

I don't think it's random. But I don't see a pattern yet.

[Kevin Buzzard]

Is this just explained by the fact that there are two definitions of CommRing in the repo (one of them only in a dependency)

[Kevin Buzzard]

Oh lol what happens if you jump to definition on the actual mathlib definition of CommRing??

[Adam Topaz]

it seems to jump to your repo again.

[Kevin Buzzard]

Yeah, me too. But I can't jump back for some reason.

[Adam Topaz]

Peek-2024-02-02-16-37.gif

[Adam Topaz]

clearly a bug... the question is where?

[Kevin Buzzard]

So that is a reliable repro for me -- this CommRing file has no imports and gives new definitions of CommRing, CommSemiring etc, and then when you're in the definition of CommSemiring in the dependency you can still jump to definition (which should be a no op) and then you jump to the local one.

[Kevin Buzzard]

So here's a video of the weirdness from first principles in mathlib:

jump_to_def_weirdness.gif

You define Group again, in a file which isn't imported by anything, and then jump to definition on mathlib's actual Group jumps to the not-imported file.

[Kevin Buzzard]

Thanks Adam for confirming that it wasn't just me!

[Mario Carneiro]

This is somewhat expected, or at least the mechanisms for the bug all exist. Have you ever noticed that you can run go-to-definition on an identifier before the yellow bar reaches the line in question?

[Marc Huisinga]

(Also: lean4#1170)

[Mario Carneiro]

The reason is because the lean server uses .ilean files to resolve identifiers, which may be out of date and/or not match up with the import structure

[Yury G. Kudryashov]

How do I update them? Sometimes emacs jumps to the location of the definition on master branch while I'm working on a branch where I edited that file and the definition went up or down.

[Sebastian Ullrich]

With lake build. The server should auto-reload the files, though Emacs sometimes asks you whether you want to deactivate that, for big directories