Zulip Chat Archive

Stream: new members

Topic: Lean infoview not displaying anything


view this post on Zulip Yakov Pechersky (Nov 12 2020 at 20:15):

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.

view this post on Zulip Yakov Pechersky (Nov 12 2020 at 20:16):

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.

view this post on Zulip Yakov Pechersky (Nov 12 2020 at 20:21):

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

view this post on Zulip Yakov Pechersky (Nov 12 2020 at 20:24):

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

view this post on Zulip Bryan Gin-ge Chen (Nov 12 2020 at 20:25):

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

view this post on Zulip Yakov Pechersky (Nov 12 2020 at 20:33):

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.

view this post on Zulip Yakov Pechersky (Nov 12 2020 at 20:34):

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

view this post on Zulip Yakov Pechersky (Nov 12 2020 at 20:34):

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

view this post on Zulip Wrenna Robson (Nov 12 2020 at 20:34):

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

view this post on Zulip Yakov Pechersky (Nov 12 2020 at 20:36):

Ah, ok, found something

view this post on Zulip Yakov Pechersky (Nov 12 2020 at 20:38):

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

view this post on Zulip Yakov Pechersky (Nov 12 2020 at 20:38):

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.


Last updated: May 08 2021 at 10:12 UTC