Merge vscode-lean4-code-actions?

[DenisGorbachev]

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:

• 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).

Are there any missing pros / cons?

What do you think in general: should we merge?

[kim-em]

Not if it involves parsing Lean code using regexes from another language. That would not be maintainable.