InfoView failing

Stream: lean4

[Jakob von Raumer]

Can someone help me, I have the current VSCode, with vscode-lean4 0.0.72 and the current master of lean4 and I get some

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

Any reasons this can happen? Any caches I should clear? I already checked that elan chooses the correct lean4 binary...

[Gabriel Ebner]

What vscode version are you on? This might be an issue with the last update (1.67)...

[František Silváši]

Works fine on '1.67.1' with '0.0.72' extension and lean 'version 4.0.0-nightly-2022-03-27'. Also works with the 'today's' nightly. Also works on both Win and Ubuntu if that could somehow matter :).

[Jakob von Raumer]

I'm on 1.67.1

[Jakob von Raumer]

Lean is 4.0.0, commit d03f0b38517d9ca28a5adc8d2c269f8c0f266d30

[Siddhartha Gadgil]

I had this happen when VS code updated and multiple windows were open. When I shut down all VS code windows and opened then it was fixed.

[Jakob von Raumer]

Doesn't fix it for me, but I noticed that it has nothing to do with Lean 4, the Lean 3 Infoview doesn't work either, so it might just be somethings broken in my VSCode in general

[Siddhartha Gadgil]

@Jakob von Raumer In case you did not come across this, my problem was solved by https://stackoverflow.com/questions/67698176/error-loading-webview-error-could-not-register-service-workers-typeerror-fai

[Jakob von Raumer]

Oh, thank you so much! Didn't know windows could hide from the docks on ubuntu!

[Chris Lovett]

I opened a bug on this here: https://github.com/leanprover/vscode-lean4/issues/206 but it might be a vscode issue, see https://github.com/microsoft/vscode/issues/125993. I found it happens more in quick repetition of "close vscode", type "code ." again quickly in another folder, repeat. Eventually I will see this same error. The workaround for me has been "wait a few seconds" before running "code ." again.