Lean Infoview in Gitpod

Stream: maths

[Jeremy Tan]

image.png how do I get the Lean infoview to show up in Gitpod?

[Eric Wieser]

It usually just works; try closing it and opening it again

[Jeremy Tan]

It still doesn't work on my laptop

[Eric Wieser]

Do you have both the lean3 and lean4 extension installed in that vscode?

[Jeremy Tan]

I'm using mathlib3 on online Gitpod, on my new laptop which has vscode and mathlib4 installed

[Jeremy Tan]

What I did was to put the mathlib3 URL into Gitpod and fire up a new workspace

[Eric Wieser]

Right, so ask gitpod what extensions are in that workspace

[Eric Wieser]

Treat it like normal vscode, go into the extension pane and search for lean3 and lean4

[Jeremy Tan]

image.png only Lean 3 is installed in Gitpod

[Jeremy Tan]

I install Lean 4 extension, infoview still ain't working

[Jeremy Tan]

More specifically I'm trying to get Gitpod working because the Lean 3/mathlib3 installation on my other laptop broke upon upgrading the OS to Ubuntu 23.04 and the install script for mathlib3 is broken there

[Huỳnh Trần Khanh]

turn on 3rd party cookies

[Huỳnh Trần Khanh]

trust me, this is the only thing you need to do to make it work

[Jeremy Tan]

but how?

[Huỳnh Trần Khanh]

it's something you do in your browser. search the web for instructions for your browser

[Jeremy Tan]

I disabled Firefox Enhanced Tracking Protection and all add-ons for the site, it still doesn't show the Lean Infoview

[Wojciech Nawrocki]

Jeremy Tan said:

I install Lean 4 extension, infoview still ain't working

Which version of Lean are you trying to use? If you're just using gitpod on leanprover-community/mathlib (that seems to be the case in your screenshot) it certainly doesn't make sense to install the Lean 4 extension.

[Jeremy Tan]

Lean 3

[Huỳnh Trần Khanh]

it's not really a Lean issue. try opening a random readme file then open the markdown preview, you'll see the preview is broken too

[Huỳnh Trần Khanh]

this is 100% a browser issue

[Huỳnh Trần Khanh]

I've experienced a similar issue. i found out the cause by opening devtools and there was a mysterious service worker permission denied thing

[Huỳnh Trần Khanh]

I'm afraid I can't help you diagnose the issue further. turning on 3rd party cookies should be enough, but you tried to turn them on and the issue wasn't fixed, so I have no idea. worst case you can switch browsers

[Eric Wieser]

Jeremy Tan said:

I install Lean 4 extension, infoview still ain't working

This will certainly not help! The two extensions do not play well with each other.

[Huỳnh Trần Khanh]

Congratulations, you found a Visual Studio Code bug early! Now everything relying on webviews is broken on Visual Studio Code and its many forks.

[Huỳnh Trần Khanh]

Now that many folks are affected the bug will be fixed soon.

[Huỳnh Trần Khanh]

disclaimer: not expert, I'm only stating a widespread issue

[Eric Wieser]

Do you have a GitHub issue in mind that describes the bug?

[Huỳnh Trần Khanh]

https://github.com/VSCodium/vscodium/issues/1503

[Scott Morrison]

That issue claims it is a VSCodium specific issue. I'm not sure if anyone is experiencing this issue in VSCode itself?

[Huỳnh Trần Khanh]

https://github.com/coq-community/vscoq/issues/464

[Huỳnh Trần Khanh]

This is a Coq user experiencing this issue on Visual Studio Code itself

[Eric Wieser]

Huỳnh Trần Khanh said:

Now that many folks are affected the bug will be fixed soon.

I don't there's much chance of vscode fixing it if no one reports it to vscode

[Scott Morrison]

In that case the two links you've posted are contradictory: the VSCodium issue has comments saying the issue doesn't occur in VSCode, while the vscoq issue is about something on VSCode.