Zulip Chat Archive

Stream: general

Topic: Lean 4 extension


view this post on Zulip 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.

view this post on Zulip Daniel Fabian (Mar 26 2021 at 12:37):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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