Mario suggested merging this extension into vscode-lean4 in the Zulip thread.
Pros:
Users won't need to install two extensions.
Cons:
Lower release speed: the PRs would need to go through the review process.
Lower dev speed: I'll have to adjust to the code style, packages, testing framework, etc (or we could have lengthy discussions, but that would result in even lower speed).
Hi @Vtec234 @gebner !
I've published a new VSCode extension for code actions.
Mario suggested merging this extension into
vscode-lean4
in the Zulip thread.Pros:
Cons:
Are there any missing pros / cons?
What do you think in general: should we merge?