Joshua Grosso (Nov 02 2020 at 06:06): Joshua Grosso (Nov 02 2020 at 06:06):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)
Joshua Grosso (Nov 02 2020 at 06:13):(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.)
Paolo Giarrusso (Nov 02 2020 at 09:44):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.
Paolo Giarrusso (Nov 02 2020 at 09:46):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
Fabian Kunze (Nov 02 2020 at 11:02):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.
Fabian Kunze (Nov 02 2020 at 11:02):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.
Paolo Giarrusso (Nov 02 2020 at 13:24):Ah, that reminds me of some github issues: proof general adds some metadata to the buffer
Stefan Monnier (Nov 02 2020 at 13:47):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.
Xuanrui Qi (Nov 02 2020 at 14:53):Slightly derailing the discussion here, but is there a reason why Proof General can't take advantage of async proofs?
Paolo Giarrusso (Nov 02 2020 at 16:06):There's a thread on discourse, but tldr the xml branch was never finished.
Joshua Grosso (Nov 03 2020 at 00:28):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.
Joshua Grosso (Nov 03 2020 at 00:29):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.
Paolo Giarrusso (Nov 03 2020 at 00:37):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.)
Joshua Grosso (Nov 03 2020 at 01:23):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
Shea Levy (Nov 03 2020 at 01:26):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:
Karl Palmskog (Nov 03 2020 at 01:31):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)
Karl Palmskog (Nov 03 2020 at 01:33):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.
Fabian Kunze (Nov 03 2020 at 06:40):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
Paolo Giarrusso (Nov 03 2020 at 07:15):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.
Paolo Giarrusso (Nov 03 2020 at 07:16):@Fabian Kunze I should try that out first, but I think I want to build you a statue
Anton Trunov (Nov 03 2020 at 08:42):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)
Théo Winterhalter (Nov 03 2020 at 08:52):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.
Enrico Tassi (Nov 03 2020 at 08:58):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 ;-)
Anton Trunov (Nov 03 2020 at 09:35):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.
Anton Trunov (Nov 03 2020 at 09:36):@Enrico Tassi Ah, that's good to hear, but I just don't like reaching for the arrow keys :)
Paolo Giarrusso (Nov 03 2020 at 09:36):I use vscodevim...
Paolo Giarrusso (Nov 03 2020 at 09:37):... and I even added at some point keybindings for coq.
Paolo Giarrusso (Nov 03 2020 at 09:38):of course, there was some issue, I forget — probably because I wanted the same bindings as in Spacemacs.
Anton Trunov (Nov 03 2020 at 09:38):Hmm, I tried vscodevim but I couldn't switch to normal mode in a Coq "buffer"
Paolo Giarrusso (Nov 03 2020 at 09:43):I'm afraid I'm going to ask "are you sure did you reboot vscode", because I can't find settings for this
Paolo Giarrusso (Nov 03 2020 at 09:43):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 :)
Maxime Dénès (Nov 03 2020 at 15:42):Yes, I do use vim bindings with VsCoq :)
Last updated: May 31 2023 at 02:31 UTC