Lean Live doesn't recover when restarting the server

Stream: general

[Shreyas Srinivas]

Of late, I frequently run into the following issue:

1. I am completing a definition which is therefore an error until comleted.
2. Lean server stops and the restart message pops up
3. I restart
4. Infoview doesn't recover and I still see the error message of the crash.

I am not sure how to reproduce this. Normally I quickly refresh the server and things are fine again. (Thankfully the code isn't lost because it is in the URL).

[Shreyas Srinivas]

I am not sure how to reproduce this error

[Kim Morrison]

Next time it happens please share the URL (with the code), and we can see if just retyping the last definition suffices to repro?

[Shreyas Srinivas]

I tried that once before (not pasting the code here, but retyping it in a new window). It is not a deterministic bug

[Shreyas Srinivas]

If it helps, this has been happening to me since 4.9.0-rc1 was released

[Michael Stoll]

I've noticed this, too, for quite some time (and I think I reported it somewhere on Zulip, but need to search more throroughly to find it). Reloading the page works.

[Michael Stoll]

Here.

[Shreyas Srinivas]

Interesting. I don't remember running into this issue until last month. But that coincides with when I started using firefox regularly instead of a certain chrome based browser

[Shreyas Srinivas]

It happened again and I have copied the error message : Server process for file:///project/mathlib-demo.lean crashed, likely due to a stack overflow or a bug.

[Shreyas Srinivas]

Best guess is that there is some sort of a worker process that is handling each session and its instance of the lean LSP has crashed in this process. Refreshing spawns a fresh process. The corresponding fix would be to restart such a process when a lean server restart is requested

[Shreyas Srinivas]

CC: @Jon Eugster