Error: no position context set

Stream: general

[Michael Stoll]

In a project (depending on Mathlib), after updating Mathlib (via the drop-down Lean menu in VSCode), I now only see the message "Error: no position context set" when I hover over something in the infoview.
Do other people see this, too? (Restarting the Lean server and also quitting and restarting VSCode did not help.)

[Michael Stoll]

(Hover works as usual in a file.)

[Kim Morrison]

Yes, I am seeing this too!

[Kim Morrison]

@Marc Huisinga?

[llllvvuu]

Current workaround: go to VSCode extension sidebar -> click gear -> Install Another Version ... -> 0.0.155

https://github.com/leanprover/vscode-lean4/issues/461
https://github.com/leanprover/vscode-lean4/pull/462

[Marc Huisinga]

I've reverted the commit that caused this issue (cc @Wojciech Nawrocki). To fix the issue, make sure to update to 0.0.157.

Thanks for the suggested fix @llllvvuu, I'll leave whether to use it to @Wojciech Nawrocki.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Oops! Should be fixed in new PR.