coq-lsp
coq-lsp copied to clipboard
ejgallego
0.2.0 crashes frequently
Describe the bug
0.2.0+8.20 crashes very often (every 5 or so edits) for me, with this error.
Error in goals request: Anomaly "File "gramlib/grammar.ml", line 1615, characters 20-26: Assertion failed." Please report at http://coq.inria.fr/bugs/.
This doesn't seem like a Coq bug because until coq-lsp crashes, everything works fine. I have also gone back to Proof General temporarily and it works well on this file.
Previously I was using 0.1.9+8.18, which also crashes with this message, but seemingly less frequently.
Error in goals request: Anomaly "File "gramlib/grammar.ml", line 1607, characters 82-88: Assertion failed." Please report at http://coq.inria.fr/bugs/.
I'm not sure if the different frequency was due to the kind of edit I was making at the time (on proofs inside one lemma at a time, instead of on definitions that are used by many downstream lemmas), or the version. But when I edit definitions as I am doing now, neither version is usable without restarting every few edits.
To Reproduce Steps to reproduce the behavior:
- My development is here
make- Open Staged.v
- Edit definitions near the top, e.g. val or expr, then re-check the file. The crashes don't happen on every edit but should appear after a short while.
Desktop:
- macOS 15.0.1 (Sequoia)
- coq-lsp 0.2.0+8.20
- Coq LSP v0.2.2
- VS Code 1.94.2
Hi @dariusf , this is due to the memprof-limits interruption backend and a patch that wasn't applied to Coq upstream to make it safe w.r.t. this method.
I will push a fix ASAP.
Sorry for this, I was hoping 8.20 would carry the fix, but we did miss the merge window.
While I apply the patch upstream, please pass to coq-lsp arguments: --int_backend=Coq , you can do this in VSCode settings.
This will make interrupting Coq slower, but will remove the crash.
Did you install Coq using OPAM? If so, I will provide you with a command to fix it.
Thank you for responding so quickly! --int_backend=Coq works great. I did install Coq using opam.