olivierverdier / spacemacs-coq Goto Github PK
View Code? Open in Web Editor NEWA very simple coq layer for spacemacs
A very simple coq layer for spacemacs
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!
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.