Lean Infoview going blank

Stream: general

[Arthur Paulino]

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]

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

[Arthur Paulino]

yeah, completely clean image.png

[Marc Huisinga]

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]

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

[Chris B]

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]

@Marc Huisinga that worked thanks!

[Gabriel Ebner]

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

[Gabriel Ebner]

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.