Zulip Chat Archive

Stream: lean4

Topic: How do I install vscode-lean4?


view this post on Zulip Huỳnh Trần Khanh (Jan 24 2021 at 13:40):

Screenshot-from-2021-01-24-20-40-06.png

view this post on Zulip Huỳnh Trần Khanh (Jan 24 2021 at 13:40):

VS Code says "No extensions found."

view this post on Zulip Edward Ayers (Jan 24 2021 at 13:44):

Can you try hitting Ctrl+P and then typing ext install mhuisi.lean4

view this post on Zulip Huỳnh Trần Khanh (Jan 24 2021 at 13:45):

Screenshot-from-2021-01-24-20-45-32.png

view this post on Zulip Huỳnh Trần Khanh (Jan 24 2021 at 13:45):

Doesn't work either.

view this post on Zulip Huỳnh Trần Khanh (Jan 24 2021 at 13:46):

Can you reproduce this issue on your machine?

view this post on Zulip Edward Ayers (Jan 24 2021 at 13:50):

Can you install other extensions?

view this post on Zulip Huỳnh Trần Khanh (Jan 24 2021 at 13:50):

Yes, I can.

view this post on Zulip Edward Ayers (Jan 24 2021 at 13:50):

It looks like you are using a non-official build of vscode from the icon for the welcome screen in your last screenshot

view this post on Zulip Huỳnh Trần Khanh (Jan 24 2021 at 13:52):

Yeah, I am using an unofficial build of VS Code for headless servers. But that shouldn't affect things right? I can install other extensions, including the Lean 3 extension so I don't think this build is the cause of this problem.

view this post on Zulip Edward Ayers (Jan 24 2021 at 13:53):

The extension is present for me.

view this post on Zulip Edward Ayers (Jan 24 2021 at 13:54):

As a last resort you can download the vsix from https://marketplace.visualstudio.com/items?itemName=mhuisi.lean4 and install manually

view this post on Zulip Edward Ayers (Jan 24 2021 at 13:54):

There is a 'download extension' link on that page

view this post on Zulip Edward Ayers (Jan 24 2021 at 13:55):

https://code.visualstudio.com/docs/editor/extension-gallery#_install-from-a-vsix

view this post on Zulip Edward Ayers (Jan 24 2021 at 13:56):

It should just show up in that marketplace explorer though, maybe it's a version thing.

view this post on Zulip Edward Ayers (Jan 24 2021 at 13:57):

https://stackoverflow.com/questions/37143536/no-extensions-found-when-running-visual-studio-code-from-source
It might be that the different build that you are using is pointing at a different extension index

view this post on Zulip Huỳnh Trần Khanh (Jan 24 2021 at 14:02):

Worked like a charm, thank you! Editing the product.json file did the trick!


Last updated: May 07 2021 at 13:21 UTC