Stale web editor behavior

Stream: general

[Eric Wieser]

I'm seeing some confusing behavior in the web editor on mathlib stable, where

#eval Lean.versionString == "4.13.0"
#guard Lean.versionString == "4.13.0"

shows the eval as being true, but fails the #guard

[Eric Wieser]

The UI also seems confused:

image.png

[Eric Wieser]

Refreshing and adjusting the dropdown seems to reliably reproduce

[Mario Carneiro]

I just tried opening that on the playground and consistently got a false from eval and a failure of the guard

[Eric Wieser]

Even after switching the playground to "mathlib stable"?

[Mario Carneiro]

oh, I missed that dropdown

[Mario Carneiro]

with it, both seem to say true

[Eric Wieser]

I think the failing sequence is:

• Open the example above with the default version
• Switch the dropdown to "stable"
• Refresh the page

[Mario Carneiro]

indeed, it seems there are now two LSPs running on both versions

[Eric Wieser]

(where step 3 often happens because I forgot about the tab for a while, and the server shutdown in the meantime)

[Kyle Miller]

I've seen this error a few times now. Somehow there's a second LSP that gives additional underlines, but you don't get messages from it. There's no error message on the #guard, right? just the red squiggle?

[Eric Wieser]

Mario Carneiro said:

indeed, it seems there are now two LSPs running on both versions

Ah, you're right; editing the code leads to up-to-date printouts from both versions, not just stale printouts from the old version

[Mario Carneiro]

If I do

#guard Lean.versionString == "4.13.0"
#guard Lean.versionString != "4.13.0"

I get red squiggles from both

[Eric Wieser]

@Kyle Miller: it looks like the editor is connected to both LSPs, but the infoview is connected to only the right one

[Kyle Miller]

@Joachim Breitner was guessing that it has to do with https://github.com/leanprover-community/lean4web/issues/41

[Joachim Breitner]

Indeed, and @Jon Eugster mentioned that he’ll have a bit more time to work on lean-related stuff the coming weeks.