Does anyone else who uses Proof General (with company-coq) find that it becomes unbearably slow and unresponsive for no discernable reason? I've found some issues on the PG repo that seem kinda relevant, but none of the suggested fixes seem to be working for me....
(for context, by "slow and unresponsive" I mean that the goals window just doesn't update sometimes, or the proof process doesn't stop thinking until I manually call proof-layout-windows
)
(Also: Just to confirm it wasn't the proof file itself, I've compared CoqIDE and Proof General with the same file, line number, specific tactic I'm evaluating, etc., and CoqIDE finishes quickly and as expected.)
Yes. Disabling company-coq seems to help a bit, but it's often enough so slow that I've switched to VsCoq. However, VsCoq and CoqIDE are much faster than Proof General can possibly be, thanks to async proofs.
it sounds like async proofs might not explain what you're observing; do you know what's taking CPU? Is it Emacs or coqtop? Those are very different symptoms
I found that resizing the emacs buffer with the coq file to a smaller size resulted in proportional speed-up of interactive processing.
Then i switched to vscoq.
I think some part of syntax highlighting or a history in the background is the culprit: If i remember right, closing the buffer does result in "reseting" the slow-dow, but simply going to the top does not.
Ah, that reminds me of some github issues: proof general adds some metadata to the buffer
I suggest you file a bug report. From your description, it seems that maybe the problem is not that Emacs is busy but that it is mistakenly waiting for something that won't happen (or that happened already)? In any case, it will require more investigation than is appropriate in this forum, I think.
Slightly derailing the discussion here, but is there a reason why Proof General can't take advantage of async proofs?
There's a thread on discourse, but tldr the xml branch was never finished.
Paolo Giarrusso said:
it sounds like async proofs might not explain what you're observing; do you know what's taking CPU? Is it Emacs or coqtop? Those are very different symptoms
A CPU+mem profile showed nothing unusual, so Emacs itself doesn't seem to be doing much of anything.
Paolo Giarrusso said:
Yes. Disabling company-coq seems to help a bit, but it's often enough so slow that I've switched to VsCoq. However, VsCoq and CoqIDE are much faster than Proof General can possibly be, thanks to async proofs.
I've been playing around with VsCoq, but it's super broken on my machine (I probably messed up my VS Code config at some point) :-(
I'll file a PG bug report, thanks everyone for the help.
VsCoq is still pretty buggy in general, FWIW. I apologise for not saying that upfront; everything I said is true, but I'd usually add huge caveats. (OTOH, coqide is IMHO more unusable on macs, so.)
I've gone back to PG and opened an issue (https://github.com/ProofGeneral/PG/issues/524) for now, only because I can't bear to use CoqIDE for more than a little bit at a time (on macOS) :-P
I'm pretty emacs dependent for everything else (on Linux), is vscoq/coqide recommended even then? I guess I can wait until my code gets complex enough to slow down PG :cold_sweat:
I've almost never had performance problems with PG on Linux, over many years of use. I think it's fair to say PG is still the most featureful and maintained interface (especially with Company-Coq)
a general recommendation is to keep Coq source files to below 1000 lines, preferably below 500. This makes sense both for speeding up compilation (file-level parallelism) and not having IDEs blow up.
Regarding vscoq bugs: i have a few open pullrequests on github that fix all the buggy behaviour that annoys me on a day-to-day basis. I also have a packaged version of the fixes (until they get merged) : https://github.com/fakusb/vscoq/releases/tag/0.3.3-alpha2-custom
Karl is certainly right that most people use PG, especially if you're already an Emacs used. The main "performance problems" with PG are 1) opening two files 2) jumping to a late line of a file, especially for slow proofs.
@Fabian Kunze I should try that out first, but I think I want to build you a statue
The people who switched to vscoq from PG, do you use vim-like keybindings in vscoq? (I use evil-mode all the time with PG)
I don't, but there is probably thousands of packges for vim bindings. There are thousands for emacs bindings. I also don't use them.
Anton Trunov said:
The people who switched to vscoq from PG, do you use vim-like keybindings in vscoq? (I use evil-mode all the time with PG)
I think @Maxime Dénès does. I switched from VIM to vscode myself a few years back, and dropping vim keybings was not really an issue for me, quite a relief actually ;-)
Théo Winterhalter said:
I don't, but there is probably thousands of packges for vim bindings. There are thousands for emacs bindings. I also don't use them.
I tried the two most popular vim-bindings and both didn't work with vscoq. After wasting an hour or so I just gave up.
@Enrico Tassi Ah, that's good to hear, but I just don't like reaching for the arrow keys :)
I use vscodevim
...
... and I even added at some point keybindings for coq.
of course, there was some issue, I forget — probably because I wanted the same bindings as in Spacemacs.
Hmm, I tried vscodevim
but I couldn't switch to normal mode in a Coq "buffer"
I'm afraid I'm going to ask "are you sure did you reboot vscode", because I can't find settings for this
Here are the settings I have:
"vim.useSystemClipboard": true,
"vim.leader" : "<space>",
"vim.normalModeKeyBindingsNonRecursive": [
{
"before": ["<leader>", "."],
"commands": [
"extension.coq.interpretToPoint",
]
}
],
Thanks for sharing Paolo, I'm going to try your settings :)
Yes, I do use vim bindings with VsCoq :)
Last updated: May 31 2023 at 02:31 UTC