olivierverdier / spacemacs-coq Goto Github PK

There's a performance problem with triggering any prover interaction (most obviously next/previous/go to) from within insert mode. It manifests itself with these operations being much slower in insert mode than in normal mode. This is arguably a performance bug in evil (see issue #696 for the details), where the cursor color is changed too frequently when Proof General makes a bunch of set-window calls to check window properties and re-layout.

I run into this particularly often since I use F2/F3/F4 in insert mode to navigate the proof (see the customized branch of my fork), though anybody using Proof General's C-c C-n/C-c C-u/C-c C-RET bindings in insert mode will run into the same issue. I have a workaround there where I just make the insert and normal mode colors the same.

The default colors used by the combination of Proof General + Spacemacs and the default scheme of the latter clashes awfully in the "response" buffer. To wit, a screenshot of a (to my eyes) unusable turquoise-on-orange:

Can we do something sensible about the default colors? Perhaps the orange background of the error message is overkill?

Using this layer, Proof General works perfectly, but company-coq seems not to work. M-x company-coq-initialize gives the error symbol's value as variable is void: -, as do the other company-coq commands, and none of the prettification seems to be in effect. Any suggestions for troubleshooting?

CC: @cpitclaudel

I've trying to add this coq layer for my spacemacs on MacOS. But i'm stuck with the error as is show in the title. How can I solve this?

Additional Info: My emacs is installed via emacs-plus from homebrew.

First of all I would like to thank you for creating this layer. It makes using Proof General in spacemacs an absolutely pleasant experience.

Since a package upgrade last week I am experiencing a weird little bug that is also described here:
syl20bnr/spacemacs#8853

Basically pressing the escape button triggers auto-completion, which is more annoying than it sounds as it makes it really hard to edit anything when any kind of variable name gets completed to tactics or similar...

I don't know how to fix the problem myself.

How to replicate:
Install the spacemacs-coq layer by cloning into .emacs.d/private (also works with a fresh spacemacs installation), add coq to the enabled layers. Open a file test.v enter o and press escape, the o gets replaced by "omega".

I'm using this layer, and I'd like to edit the Proof General variable coq-load-path. What's the best way to go about this?

The installation is mentioned in a gist, but it would be nice to have real instructions!

When I press C-r in major mode "coq-mode" (evil mode "normal"), redo does not work and the following message is displayed:

command-execute: Symbol's function definition is void: redo

I do not have this issue buffers in "fundamental" major mode.

File error: Cannot open load file, No such file or directory, /usr/local/share/emacs/site-lisp/proof-general/generic/proof-site

Any plans to integrate into spacemacs?

Thanks for the layer!

Hi, thank you for sharing your coq config. It is really nice. However, I encounter some problems with the completion, i.e. company-coq-mode. I thought it is something with the company-coq-mode and I find a similar issue at cpitclaudel/company-coq#79. Do you encounter similar problems? Is it something about our Spacemacs configuration or about company-coq-mode? Thank you again!