Zulip Chat Archive

Stream: general

Topic: Lean Infoview going blank

Arthur Paulino (Oct 20 2021 at 17:33):

I'm playing around with Lean on VS Code but my Lean Infoview goes blank anytime I change the content of a lean file. Has anyone experienced anything similar? I'm running VS Code on a Linux machine

Gabriel Ebner (Oct 20 2021 at 17:34):

By "blank" do you mean the diagnostics are gone?

Arthur Paulino (Oct 20 2021 at 17:34):

yeah, completely clean image.png

Marc Huisinga (Oct 20 2021 at 17:37):

Judging from your other thread in #lean4, you're using the m2 release version of Lean 4. Is this the version that this issue occuring with?
If so, you may want to use the nightly version of Lean 4 instead. The VSCode extension maintains compatibility with that, and the release version is very old.

Arthur Paulino (Oct 20 2021 at 17:37):

it does appear under the "Problems" tab though. But it's a bit bothersome

Chris B (Oct 20 2021 at 17:39):

I'm also having (new) issues; the infoview only shows:

All Messages (0)
No messages.

I'm using the pinned mathlib 4 version: Lean (version 4.0.0-nightly-2021-10-12, commit d6ba8e597a3d, Release)

Arthur Paulino (Oct 20 2021 at 17:41):

@Marc Huisinga that worked thanks!

Gabriel Ebner (Oct 20 2021 at 17:43):

Mmmh, the infoview is still supposed to work with M2.

Gabriel Ebner (Oct 20 2021 at 18:01):

Should work with 0.0.39. The reason it didn't work is because 4.0.0-M2 didn't include the fullRange field in diagnostics yet. I've now added a ? to the type and fixed the type errors.

Last updated: Dec 20 2023 at 11:08 UTC