Strange Go to Declaration behavior

Stream: lean4

[Julian Berman]

Create a file containing just:

import Mathlib.RingTheory.PowerSeries.Inverse
import Mathlib.RingTheory.PowerSeries.WellKnown

and try to go to definition on the two import lines. Here (both in neovim and VSCode), if I go to definition on Inverse it will jump to the file, but if I do it on the next line on WellKnown, I get "no definition found" from the language server. I can reproduce the same in GitPod + VSCode. Is this a known issue / does anyone see what's happening?

[Julian Berman]

Ah fun, maybe this is Sebastian's https://github.com/leanprover/lean4/issues/4958

[Julian Berman]

Yeah it is, reordering the imports indeed switches which one is stuck. OK, next time should search first. Never mind the noise.

[Damiano Testa]

I did not know about the issue, but had observed the behaviour, so I'm happy that you mentioned it here, so that I could upvote it!