Lean 4 extension

Stream: general

[Gabriel Ebner]

A new version of the Lean 4 vscode extension was just released. Please complain if it breaks anything, like for example the Lean 3 extension.

[Daniel Fabian]

What are the changes? Would be nice to know what to try out?

[Gabriel Ebner]

Mostly just a big bugfix that avoids vscode and lean using 100% cpu if you use ctrl+hover.

[Marc Huisinga]

(This one: https://github.com/leanprover/lean4/issues/367, where the associated PR is this one: https://github.com/leanprover-community/vscode-lean4/pull/17)
I don't see how the above commit could break the compatibility layer with vscode-lean. In an earlier version of the PR there was a change to the language id provided by the package.json, but that change is also gone now, so it should be fine, I think?

[Gabriel Ebner]

The PR description seems to be outdated, yes.