Go to definition jumps to incorrect file

[ammkrn]

If there are two different files that contain declarations with the same name, the go to definition feature will sometimes jump to the declaration in the wrong file. This seems to happen consistently if the offending files are all open in a particular editor group (in tabs).

Example: If I make a file x.lean

structure User where
  name : String

Then another file y.lean

structure User where
  name : Unit

example : User -> User := id

Right clicking on the User in the example declaration and selecting go to definition will take me to the declaration in x.lean.

I'm using vscode 1.67, v0.0.75 of the extension, and lean 4 nightly-2022-05-19.