Lean web server frequent crashes

Stream: lean4

[Shreyas Srinivas]

Hi all,
Lately lean's web server seems to crash at the slightest syntactic error that could be fixed in a minute. This results in the server frequently crashing. Further, at least on firefox, Ctrl + shift + X doesn't restart the server. Not sure why. At least this is the case on Ubuntu + firefox

CC : @Jon Eugster

[Damiano Testa]

I have not noticed the frequent crashes, but I usually refresh the tab as a substitute for restarting.

[Damiano Testa]

Also, I think that this is new (I had certainly never noticed it earlier), but now "Go to definition" in the online server takes you to the documentation pages: this is awesome!

[Shreyas Srinivas]

It crashes for me as soon as I do that

[Damiano Testa]

I don't really know what could be causing it: I'm also using Firefox, on Linux.

[Joachim Breitner]

The last maybe two weeks I observe often heavy load on the machine that wasn’t there before. This may be partly due to a known bug lean4web where a session may spawn duplicate lean processes, but that doesn't fully explain it.

[Jon Eugster]

Ctrl+Shift+X is not supposed to work, or at least thats never been implemented. You should be able to click the "Restart File" button in the infoview or the "Restart Server" button from the menu.

For the crashes, could you give me some concrete operations you do to get the server to crash? I'll try to take some time tomorrow to look at it and the process duplication, too

[Jon Eugster]

@Damiano Testa indeed, I implemented a hacky go-to-def. it's quite rough around the edges, but it works in a good amount of cases:grinning_face_with_smiling_eyes:

[Shreyas Srinivas]

Well, the doc page thing is just one example. It is hard to pin down exactly when the editor crashes. Usually when I am midway through a long def or editing an old def which temporarily introduces a downstream error. To be fair it could just be the LSP that is at fault, since I had crashes at calls for inferInstance both locally and on lean web

[Jon Eugster]

ok, so there are certainly errors thrown to the browser console when shift-howering over things just before go-to-def.

Could you open the browser debug tools and see if you a) see these errors pop up when shift-hovering and b) if they cause problems for you?

[Shreyas Srinivas]

I will try this today. Hopefully the crashes prove deterministic enough to reproduce them