When writing a proof in proof mode, I frequently encounter this message 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. I would then need to restart VS Code to continue using the language server.
I would assume this mechanism is designed to prevent infinite restart loops from happening. However, sometimes I won't mind the language server restarting once every 10 seconds. Is it possible to have some additional configuration to adjust this behavior? For example, vscoq would not restart the language server after it crashed 50 (instead of 5) times in the last 3 minutes. The number of retries would be an adjustable parameter.
As for language server crashes, I found that it can be reproduced by repeatedly inserting and deleting a character in proof mode in quick succession. In particular, if I repeatedly hit d and Backspace in proof mode, the language server would reach 5 crashes only after a few seconds. However, if I wait for a few seconds between each keystroke, no crash would occur. I would assume this error occurred because I set proof.mode to Continuous: if I make a change to the document when the language server is reevaluating the document, the language server would somehow crash.
Here's some more info in case they are needed:
vscoq version: v2.2.1
language server version: v2.2.1
coq version: v8.20.0
OS: Fedora 40
Frequent language server crashes also occur on a macbook, but I did not run detailed experiments on it.
Language server output:
[Error - 6:29:48 PM] Server process exited with code 0.
[Info - 6:29:48 PM] Connection to server got closed. Server will restart.
true
[Error - 6:29:49 PM] Server process exited with code 0.
[Info - 6:29:49 PM] Connection to server got closed. Server will restart.
true
[Error - 6:29:50 PM] Server process exited with code 0.
[Info - 6:29:50 PM] Connection to server got closed. Server will restart.
true
[Error - 6:29:51 PM] Server process exited with code 0.
[Info - 6:29:51 PM] Connection to server got closed. Server will restart.
true
[Error - 6:29:51 PM] Server process exited with code 0.
[Error - 6:29:51 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.
When writing a proof in proof mode, I frequently encounter this message
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.I would then need to restart VS Code to continue using the language server.I would assume this mechanism is designed to prevent infinite restart loops from happening. However, sometimes I won't mind the language server restarting once every 10 seconds. Is it possible to have some additional configuration to adjust this behavior? For example,
vscoqwould not restart the language server after it crashed50(instead of 5) times in the last 3 minutes. The number of retries would be an adjustable parameter.As for language server crashes, I found that it can be reproduced by repeatedly inserting and deleting a character in proof mode in quick succession. In particular, if I repeatedly hit
dandBackspacein proof mode, the language server would reach 5 crashes only after a few seconds. However, if I wait for a few seconds between each keystroke, no crash would occur. I would assume this error occurred because I setproof.modetoContinuous: if I make a change to the document when the language server is reevaluating the document, the language server would somehow crash.Here's some more info in case they are needed:
vscoq version:
v2.2.1language server version:v2.2.1coq version:v8.20.0OS: Fedora 40 Frequent language server crashes also occur on a macbook, but I did not run detailed experiments on it.
Language server output: