vscoq is constantly crashing and has to be reloaded every minute

[JasonGross]

I don't think the server should crash when it sees

[top                 , 91315, 1737325241.070620] ==========================================================
[top                 , 91315, 1737325241.070650] Trying to get range of non-existing sentence 794
[top                 , 91315, 1737325241.070651] ==========================================================
[Info  - 10:20:41 PM] Connection to server got closed. Server will restart.
true
[Error - 10:20:41 PM] Server process exited with code 0.
[top                 , 91390, 1737325246.720450] ==========================================================
[top                 , 91390, 1737325246.720488] Trying to get range of non-existing sentence 692
[top                 , 91390, 1737325246.720490] ==========================================================
[Error - 10:20:46 PM] Server process exited with code 0.
[Info  - 10:20:46 PM] Connection to server got closed. Server will restart.
true
[top                 , 91429, 1737325291.813120] ==========================================================
[top                 , 91429, 1737325291.813144] Trying to get range of non-existing sentence 1050
[top                 , 91429, 1737325291.813145] ==========================================================
[Error - 10:21:31 PM] Server process exited with code 0.
[Error - 10:21:31 PM] The Coq Language Server server crashed 5 times in the last 3 minutes. The server will not be restarted. See the output for more information.

[rtetley]

Could you provide an example file where this happens ?

[Dashadower]

I'm getting the same error. It's not occurring when I step through but when I'm in the middle of typing something.

[JasonGross]

This was caused by having autocompletions enabled in settings, disabling them fixes the issue

[Dashadower]

This was caused by having autocompletions enabled in settings, disabling them fixes the issue

Did you disable vscoq's Completion: Enable option? I'm still getting the same error after disabling it, even after reinstalling coq and vscoq from a fresh switch.

[rtetley]

I believe this is the same problem as #1009 and was fixed by https://github.com/coq/vscoq/pull/1021. Next release is imminent !

[Dashadower]

That's great. Looking forwards to it.

[Blaisorblade]

This should probably be closed (fixed duplicate), unless the problem reoccurs.

[afdw]

I am getting this on master (Rocq commit https://github.com/rocq-prover/rocq/commit/4015c7e4126a1aca4abef8a72bede16a54a1f0a5, VsRocq commit https://github.com/rocq-prover/vsrocq/commit/395799c142e13d973f66e5cb7b3827e44100adee):

[top                 , 1423197, 1753882094.894078] ==========================================================
[Error - 3:28:15 PM] Server process exited with code 0.
[Info  - 3:28:15 PM] Connection to server got closed. Server will restart.
true
[top                 , 1434937, 1753882235.676034] ==========================================================
[top                 , 1434937, 1753882235.676119] Trying to get range of non-existing sentence 1139
Raised at Exninfo.iraise in file "clib/exninfo.ml", line 79, characters 4-11
Called from Dm__DocumentManager.handle_event in file "dm/documentManager.ml", line 728, characters 16-51
Called from Dune__exe__LspManager.handle_event in file "vsrocqtop/lspManager.ml", line 657, characters 26-133
Called from Dune__exe__Vsrocqtop.loop.loop in file "vsrocqtop/vsrocqtop.ml", line 31, characters 21-50
Called from Dune__exe__Vsrocqtop.loop in file "vsrocqtop/vsrocqtop.ml", line 39, characters 6-15

Happens on any project of file. VsRocq options (continuous proof checking mode):

{
    "vsrocq.proof.mode": 1,
    "vsrocq.goals.messages.full": true,
    "vsrocq.diagnostics.full": true,
    "vsrocq.args": [
        "-d", "backtrace",
    ],
    "vsrocq.goals.maxDepth": 1e+100,
}

It crashes after basically any change to a file. Also, the goals and messages panels are out of sync most of the time, and I have to move the cursor back and forth to make them synchronize.

I had to increase the maxRestartCount, otherwise it stops restarting after 5 times. Still, these crashes every few seconds and the desynchronization issue slow my work down.

Can you reproduce that on master or do you need more information about my setup?

[gares]

Can you share a file where the problem occurs. Thanks

[afdw]

Sure, here is one:

Goal 1 = 1 -> 2 = 2.
  intros.

Inserting H between intros and . (so replacing it with intros H.) crashes the server for me. It happens basically every time I try doing it.

[afdw]

Are there other people who are able to reproduce the issue?