Lean infoview not displaying anything

Stream: new members

[Yakov Pechersky]

I just restarted my computer, opened VSCode to a mathlib repo, and I'm not getting anything displaying in the Lean Infoview. I've tried restaring Lean in VSCode, exiting and reopening VSCode, trying a different repo. Nothing worked.

[Yakov Pechersky]

My vscode-lean extension is on 0.16.16. I am using Remote-WSL onto my local Ubuntu. This all worked before. This is the October 2020 version of VSCode.

[Yakov Pechersky]

Files compile fine, I see blue bars appear then disappear.

[Yakov Pechersky]

In the Problems section, I'm able to see output of #check or similar commands, or errors where goals haven't been solved.

[Bryan Gin-ge Chen]

If you open "Help > Toggle developer tools" do you see anything suspicious in the console?

[Yakov Pechersky]

I don't see anything different that a VSCode I have open pointing to the same directory, but without Remote-WSL on. Without Remote-WSL, there is a Lean Infoview with the expected buttons and a "loading" message -- it's taking a long time because of slow Windows <-> WSL VM, and the Windows Lean doesn't have the oleans.

[Yakov Pechersky]

Inspecting the elements of the webview where the Lean Infoview is (or should be), they're no different. They both share a shadow-root, which when expanded, is just some empty iframe

[Yakov Pechersky]

The debug console has no messages in it in either case.

[Wrenna Robson]

I think I had this and I fixed it by reinstalling VSCode.

[Yakov Pechersky]

Ah, ok, found something

[Yakov Pechersky]

I'm not sure how, but running leanproject build fixed it.

[Yakov Pechersky]

And maybe removing *.olean.lock files. There were some errors that appeared in the Console of the Developer Tools, but now I can't get them to return.