Error loading webview

Stream: mathlib4

[Damiano Testa]

Suddently, every time I open a Lean file in VSCode, the error

Error loading webview: Error: Could not register service worker: InvalidStateError: Failed to register a ServiceWorker: The document is in an invalid state..

appears. When I have seen it in the past, quitting and restarting VSCode fixed it, but now I tried that a few times and nothing changes. Is anyone else seeing this?

[Kevin Buzzard]

Try quitting VSCode, killing all lean processes and then restarting?

[Damiano Testa]

There are no lean processes, but I killall lean anyway and the problem persists.

[Damiano Testa]

(i.e. quit VSCode, killall tells me there is no lean, open VSCode, same error)

[Damiano Testa]

It is "only" the infoview that does not work: hovering over stuff shows what would normally appear in the infoview.

[Kevin Buzzard]

If a reboot doesn't solve it, I'm out of ideas

[Damiano Testa]

Ok, that is what I tried and restarting my computer fixed it! Thanks!

[Marc Huisinga]

The next time you run into this, try killall code before restarting. This is unfortunately one of those long-standing issues related to webviews in VS Code. See also https://stackoverflow.com/questions/67698176/error-loading-webview-error-could-not-register-service-workers-typeerror-fai..

[Kevin Buzzard]

darn it, sorry Damiano! I should have suggested that too!

[Damiano Testa]

Marc, thanks for the advice and the links: I'll try killall code next time.

[Damiano Testa]

I don't know if this is related, but I have also observed that VSCode seems to have some bad interactions with Firefox, more so than with Chrome. These issues though are hard to reproduce. I will see if killing all code processes works there too.