Topic: Lean 4 extension
Gabriel Ebner (Mar 25 2021 at 14:21):
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 (Mar 26 2021 at 12:37):
What are the changes? Would be nice to know what to try out?
Gabriel Ebner (Mar 26 2021 at 12:55):
Mostly just a big bugfix that avoids vscode and lean using 100% cpu if you use ctrl+hover.
Marc Huisinga (Mar 26 2021 at 13:12):
(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 (Mar 26 2021 at 13:13):
The PR description seems to be outdated, yes.
Last updated: May 14 2021 at 13:24 UTC