Broken hover in mutual def

[digama0]

trafficstars

Currently if you click on visit on these lines: https://github.com/leanprover/lean4/blob/9e69259f83432371fdcf3af7ba6f504462e7bff1/src/Lean/MetavarContext.lean#L986-L990 go to definition will take you do this entirely unrelated definition: https://github.com/leanprover/lean4/blob/9e69259f83432371fdcf3af7ba6f504462e7bff1/src/Init/Meta.lean#L229-L230

I suspect it has something to do with the fact that this is a link to a mutual def from another def in the same mutual block. I'll add a MWE version of the issue when I can.

[digama0]

It seems to be difficult to reproduce. If you just make a copy of MetavarContext.lean, inside or outside the lean4 repo, then the hovers work fine. It might be some corruption in the .ilean files, or something to do with the compilation process? I reproduced this on master after using make to compile everything.

[leodemoura]

I cannot reproduce this instance of the problem, but I have experienced it from time to time. I don't know what triggers this issue. @Kha is also investigating the problem.