Coq crashes too frequently

Using Coq
1

Hi,

I have recently been facing this issue of the coq goals window not updating in my text editor while editing the .v file. I am using Coq v8.18.0 on my Mac along with coq-lsp v0.1.8+8.18 (coq-lsp extension as well) on VS Code. I noticed that after coq-lsp finishes analyzing the document, it works fine for a few seconds after which it stops updating as I step through the code. I also noticed in the activity monitor that the coq-lsp process becomes a memory hog eating up loads of memory and using swap memory as well, eventually draining my machine’s battery.

I have tried the following solutions:

  • Uninstalling and reinstalling the coq-lsp VS Code extension.
  • Restarting my machine
  • Uninstalling and reinstalling all coq related packages using Opam.
  • Switching to VSCoq (another extension that runs on a different language server)

Can someone guide me on how to navigate this issue? What steps can I take to fix this problem?

Thank you.

2

Hi @ArshMalik02 , it could be that you are running into some of the known issues for coq-lsp.

Would you mind opening a bug so we can reproduce? Also, I recommend you follow up on coq-lsp Zulip’s channel.

Usually for coq-lsp to describe like that, one of two things happened:

  • a file couldn’t be interrupted properly
  • the printing routine is taking a long time and VSCode gets stuck

Both issues can be workarounded.

Alternatively, you can go back to more traditional interfaces like VSCoq 1 , CoqIDE, or Emacs, but these are way less convenient in some other ways.

3

How do I open a bug?

To add, I am working on a project which has a bunch of modules and a main.v file (~1400 lines of code) that imports the necessary modules. coq-lsp, after the initial compilation, hangs after a few seconds. But, when I create a temp.v in a separate directory, it works fine.

4

Hi @ArshMalik02 , see my comment on Zulip, basically the file you shared has a command that takes 10 seconds to execute, and cannot be interrupted in the current version.

Newer version of coq-lsp should work much better, but still some issues may appear as documented in Zulip.