Random highlighting failure

Stream: lean4

[Patrick Massot]

Does anyone else sometimes see semantic highlighting stopping in the middle of a file, and returns only after reloading the file? If yes, is this a VSCode bug only or is it something that could be fixed on our side? @Marc Huisinga

[Scott Morrison]

I have not seen this.

[Kevin Buzzard]

@Bhavik Mehta did you see this once?

[Bhavik Mehta]

Yeah I've seen this a ton, it usually doesn't get fixed by restarting Lean but does by reloading the window

[Yongyi Chen]

I've had this too.

[Marc Huisinga]

This sounds a lot like the elusive lean4#1219. I haven't investigated this myself yet, but the fact that restarting the server doesn't fix it strongly suggests that it's either a VS Code issue or a VS Code extension issue.

[Sebastian Ullrich]

I've seen highlighting get stuck in weird states without the server hanging but it's so rare that I couldn't even begin to speculate about how to reproduce it

[Marc Huisinga]

When this occurs, does it only affect highlighting or other features as well? (E.g. go-to-definition, diagnostics, the info view, ...)

[Sebastian Ullrich]

Anything on-demand definitely was not affected for me. I don't really use the document structure, problem view (in contrast to info view), or other persistent information enough to tell...

[Patrick Massot]

I am pretty sure that only highlighting is affected but I will check next time it occurs.

[Bhavik Mehta]

For me go-to-definition usually fails with it, and I think the info view too, but I'm less sure on the latter one. This occurs for me about once every day working in Lean 4, but I also have no idea how to reproduce it.

[Patrick Massot]

I confirm that go-to-definition works.