live.lean-lang.org indefinitely waiting

Stream: general

[Shreyas Srinivas]

Lean Live is indefinitely waiting for the server to start at the time of this message.

[Marc Huisinga]

Testing it now, it seems to work for me.

[Shreyas Srinivas]

Works for me now.

[Jon Eugster]

I think I observed that too sometimes, and I think it might be depending on where your cursor position is in the document. Further, I think I occationally have this in VSCode, as well (or used to have?).

Lean mentions it in this troubleshooting doc, so it's likely unrelated to the webeditor. Next time this happens, you could try if "☰ > Restart Server" does anything, or note the exact code and cursor position you had and file an issue at lean4web.

[Sebastian Ullrich]

I was updating the server OS today

[Shreyas Srinivas]

Okay. Thanks :). That would also explain why restarting the server failed for me at that time.