Zulip Chat Archive

Stream: lean4

Topic: Comment on my extension request


view this post on Zulip Huỳnh Trần Khanh (Jan 26 2021 at 00:39):

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.

view this post on Zulip Bryan Gin-ge Chen (Jan 26 2021 at 01:13):

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

view this post on Zulip Gabriel Ebner (Jan 26 2021 at 09:06):

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.

view this post on Zulip Marc Huisinga (Jan 26 2021 at 09:46):

@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 :)

view this post on Zulip Gabriel Ebner (Jan 26 2021 at 09:56):

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

view this post on Zulip Gabriel Ebner (Jan 26 2021 at 09:56):

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

view this post on Zulip Gabriel Ebner (Jan 26 2021 at 09:57):

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

view this post on Zulip Gabriel Ebner (Jan 26 2021 at 09:57):

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

view this post on Zulip Marc Huisinga (Jan 26 2021 at 09:59):

:grinning_face_with_smiling_eyes:


Last updated: May 07 2021 at 13:21 UTC