VsCoq 2 -- Very slow with 100% CPU usage

[julesjacobs]

In the first few seconds of use it is fast, but then it slows down to a crawl. coqtop shows 100% cpu usage. Updating the proof state when moving the cursor takes several seconds to even minutes. I'm on OS X with vscoq language server 2.1.2, coq 8.18.0, and vscode Version: 1.87.1.

[rtetley]

Hi, thanks for reporting !
Could you give me more context ? Like what file (if you have an example file it would be perfect) you are using and what settings ? I assume continuous mode but are you using proof delegation ?

[julesjacobs]

Yes I am using continuous mode. The slowdown does not happen in the mode where you manually advance the proof state.

I am not certain whether I'm using proof delegation. How do I determine that?
It happens on all large files I've tried. You may be able to replicate it on files from the Iris project https://gitlab.mpi-sws.org/iris/iris/

Let me know if you need more information!

[rtetley]

Ah okay ! To be honest I am not sure using continuous mode will ever be viable on a very large file. Each time you make an edit it will trigger a re-computation of most everything that comes after. Maybe in the future we will figure out a heuristic, or a strategy to make it work but I doubt it. At the moment I would recommend using manual mode on larger files !

For the delegation you can look for the VsCoq > Proof: Delegation setting.