Server crashes when invalidating some sentences

[thery]

I am using 2.2.4 and the parsing phase seems more fragile. While editing I have sometimes the server crashing.
Here is my log file of the Coq Language Server

[top                 , 69531, 1740479886.430753] ==========================================================
[top                 , 69531, 1740479886.430856] cannot find dependents for sentence 923
[top                 , 69531, 1740479886.430859] ==========================================================
[Error - 11:38:06 AM] Server process exited with code 0.
[Info  - 11:38:06 AM] Connection to server got closed. Server will restart.
true
[top                 , 96024, 1740484354.726290] ==========================================================
[top                 , 96024, 1740484354.726321] cannot find dependents for sentence 1371
[top                 , 96024, 1740484354.726322] ==========================================================
[Error - 12:52:34 PM] Server process exited with code 0.
[Info  - 12:52:34 PM] Connection to server got closed. Server will restart.

How I can find what senterce 923 and 1371 refer to?

[rtetley]

This is an issue in the scheduler. Do you have an example where this happens ?
We now schedule parse errors as a specific event to have it show up in the interface (as opposed to running through).

[rtetley]

Okay, I believe the culprit is:
https://github.com/coq/vscoq/blob/b0b7f6933cb3c2b6f16d90891a7884bd75284d05/language-server/dm/executionManager.ml#L846

When a sentence is invalidated we check if we need to invalidate its dependents. In the off chance that we scheduled a block on parse error event that needs to be "invalidated", this will try and look for its dependents (to invalidate them) and crash.

I can push a hotfix / release if this is really blocking or we can wait till next release (in about 3 weeks time).

[thery]

Ok here is a way to reproduce it. I create a syntax error and try to execute it.

now editing anywhere on the line of the error makes the server crash

[rtetley]

Well I've got a fix, so depending on how impactful this is, I can release.

[thery]

Please release 🙏

[rtetley]

I have had reports of similar crashes happening just with some copy pasting through a coq file... See https://coq.zulipchat.com/#narrow/channel/237662-VsCoq-devs-.26-users/topic/VSCoq.20resetting.20a.20lot.20on.202.2E2.2E5

If anyone gets a similar behaviour please could you report ? Trying to pin-point the problem !

[thery]

Got the same error as @TheoWinterhalter

==========================================================
[top                 , 385482, 1741257457.337959] Trying to get range of non-existing sentence 1453
[top                 , 385482, 1741257457.337962] 
==========================================================
[Error - 11:37:37 AM] Server process exited with code 0.
[Info  - 11:37:37 AM] Connection to server got closed. Server will restart.
true

very difficult to reproduce.