peek definition sometimes fails in VS code

Stream: new members

[Arthur Paulino]

Greg Leo said:

In VS code, sometimes my ability to peek at definitions just goes away. Is this a known bug?

I think it deserves a thread of its own, but I'm going to say something related:
In Lean 3 I remember being able to ctrl+click on imports and it would take me to the respective modules. But I'm not able to do it in Lean 4 anymore :sad:
(can a mod split this thread in two please? :pray: )

[Julian Berman]

In Lean4, are the cases it doesn't work for you stdlib modules perchance?

[Julian Berman]

Er, core modules I suppose I mean.

[Arthur Paulino]

It doesn't work for any import right now (modules inside the package nor from core (Prelude.lean for instance))

[Stuart Presnell]

Greg Leo said:

In VS code, sometimes my ability to peek at definitions just goes away. Is this a known bug?

Is there any pattern to when this is happening? In particular, is this happening when you have an error in your code? Or when the orange progress bar hasn't made (enough) progress yet?