Stream: Miscellaneous

Topic: Proof General really slow?


view this post on Zulip 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)

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Nov 02 2020 at 13:24):

Ah, that reminds me of some github issues: proof general adds some metadata to the buffer

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Nov 02 2020 at 16:06):

There's a thread on discourse, but tldr the xml branch was never finished.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip 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:

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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 ;-)

view this post on Zulip 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.

view this post on Zulip 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 :)

view this post on Zulip Paolo Giarrusso (Nov 03 2020 at 09:36):

I use vscodevim...

view this post on Zulip Paolo Giarrusso (Nov 03 2020 at 09:37):

... and I even added at some point keybindings for coq.

view this post on Zulip 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.

view this post on Zulip Anton Trunov (Nov 03 2020 at 09:38):

Hmm, I tried vscodevim but I couldn't switch to normal mode in a Coq "buffer"

view this post on Zulip 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

view this post on Zulip 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",
          ]
      }
  ],

view this post on Zulip Anton Trunov (Nov 03 2020 at 09:44):

Thanks for sharing Paolo, I'm going to try your settings :)

view this post on Zulip Maxime Dénès (Nov 03 2020 at 15:42):

Yes, I do use vim bindings with VsCoq :)


Last updated: Aug 19 2022 at 19:03 UTC