Comment on my extension request

Stream: lean4

[Huỳnh Trần Khanh]

It turned out that the vscode-lean4 extension is not available on the code-server marketplace so I requested the extension here. A code-server organization member commented on my issue, asking me to reach out to the author of the extension. What they said is Greek to me. I hope that someone understands what they said and maybe does the right thing LOL. Thanks in advance.

[Bryan Gin-ge Chen]

@Marc Huisinga This shouldn't be too hard, hopefully: @Gabriel Ebner did something similar for vscode-lean in this commit.

[Gabriel Ebner]

Yeah, sorry, I'm a bit busy at the moment. Publishing the vscode-lean4 extension on the vscode and openvsx marketplace is very high on my todo list.

[Marc Huisinga]

@Huỳnh Trần Khanh
The current version over at github will probably be published under the leanprover organization, after which I'll take down mhuisi.lean4. Hence I won't publish mhuisi.lean4 anywhere else for now.

@Bryan Gin-ge Chen The current version at github has that release script :)

[Gabriel Ebner]

If the release script is already there, then this is easy to do. :smile:

[Gabriel Ebner]

https://github.com/leanprover-community/vscode-lean4/releases/tag/v0.0.2

[Gabriel Ebner]

https://open-vsx.org/extension/leanprover/lean4

[Gabriel Ebner]

https://marketplace.visualstudio.com/items?itemName=leanprover.lean4

[Marc Huisinga]

:grinning_face_with_smiling_eyes: