search

leanprover / lean4

Lean 4 programming language and theorem prover
https://lean-lang.org
Apache License 2.0
4.47k stars 388 forks source link

Broken hover in mutual def #1417

Open digama0 opened 2 years ago

digama0 commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

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.