VsCoq 2 -- Very slow with 100% CPU usage
Opened this issue · 4 comments
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.
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 ?
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!
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.
Hey @julesjacobs, have the latest releases improved this issue ? Could you give some feedback ?