How do I install vscode-lean4?

Stream: lean4

[Huỳnh Trần Khanh]

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

[Huỳnh Trần Khanh]

VS Code says "No extensions found."

[Edward Ayers]

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

[Huỳnh Trần Khanh]

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

[Huỳnh Trần Khanh]

Doesn't work either.

[Huỳnh Trần Khanh]

Can you reproduce this issue on your machine?

[Edward Ayers]

Can you install other extensions?

[Huỳnh Trần Khanh]

Yes, I can.

[Edward Ayers]

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

[Huỳnh Trần Khanh]

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.

[Edward Ayers]

The extension is present for me.

[Edward Ayers]

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

[Edward Ayers]

There is a 'download extension' link on that page

[Edward Ayers]

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

[Edward Ayers]

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

[Edward Ayers]

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

[Huỳnh Trần Khanh]

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