Coq layer
Table of ContentsClose
1. Description
This layer adds support for the Coq proof assistant (adapted from spacemacscoq) to Spacemacs.
1.1. Features:
 Syntax highlighting
 Syntaxchecking
 Autocompletion (requires the autocompletion layer to be installed)
 Debugging of mathematical proofs from within Emacs using a special proof layout
 Replacement of certain constants with the correct mathematical signs
 Inserting of certain preconfigured proof elements
2. Install
2.1. Layer
To use this configuration layer, add it to your ~/.spacemacs
. You will need to
add coq
to the existing dotspacemacsconfigurationlayers
list in this file.
2.2. Coq
Official installers for macOS and Windows are available from: https://coq.inria.fr/download.
Linux users can build from source or consult with their own package managers.
3. Troubleshooting
3.1. There are empty square boxes in place of math operators
Math symbols present in your buffer (e.g. forall exists) will attempt to be
prettified, if you are seeing empty square boxes this means an appropriate math
symbol cannot be found in your font. You can either install a appropriate math
font, or disable the feature by adding the following snippet to the your
dotspacemacs/userconfig
.
(withevalafterload 'companycoq (addtolist 'companycoqdisabledfeatures 'prettifysymbols))
4. Key bindings
4.1. Laying out windows
Key binding  Description 

SPC m l c 
Clear response buffer 
SPC m l l 
Relayout windows 
SPC m l p 
Show current proof 
4.2. Managing prover process
Key binding  Description 

SPC m p i 
Interrupt prover 
SPC m p p 
Process buffer  processes and moves point to end of buffer 
SPC m p q 
Quit prover 
SPC m p r 
Retract buffer  rewinds and moves point to beginning of buffer 
4.3. Getting documentation
Key binding  Description 

SPC m h h 
Show documentation for whatever is below the cursor 
SPC m h e 
Show documentation for the error in the `*response*` buffer 
SPC m h E 
Browse all available documentation for errors 
4.4. Prover queries
The mnemonic for a
is "ask".
Key binding  Description 

SPC m a a 

SPC m a A 
Print (showing all) 
SPC m a b 
About 
SPC m a B 
About (showing all) 
SPC m a c 
Check 
SPC m a C 
Check (showing all) 
SPC m a f 
Search (mnemonic: "find theorems") 
SPC m a i b 
About (showing implicits) 
SPC m a i c 
Check (showing implicits) 
SPC m a i i 
Print (showing implicits) 
SPC m a o 
Show an outline of the current proof script 
4.5. Moving the point
Key binding  Description 

SPC m g e 
Go to end of command at point 
SPC m g g 
Go to definition at point 
SPC m g l 
Go to last processed command 
SPC m g s 
Go to start of command at point 
4.6. Inserting
Key binding  Description 

SPC m MRET 
Insert regular match branch 
SPC m MSRET 
Insert match goal with branch 
SPC m i c 
Insert a vernacular command 
SPC m i e 
Insert End <sectionname> 
SPC m i i 
Insert intros with default variable names 
SPC m i l 
Extract lemma from current goal  exit with CRET (not Cj ) 
SPC m i m 
Insert match on a type 
SPC m i r 
Insert a Require statement 
SPC m i s 
Insert a Section or Module 
SPC m i t 
Insert a tactic 
SPC m i T 
Insert a tactical 
Note the last two are regular companycoq
bindings, left alone since they are
most useful in insert mode. The full companycoq
tutorial showcasing all
available companycoq
key bindings can be accessed at any time using SPC SPC
companycoqtutorial
.
4.7. Options
Key binding  Description 

SPC m T e 
Toggle electric terminator. 