#+TITLE: Coq layer

[[file:img/coq.png]]

* Table of Contents                                        :TOC_4_gh:noexport:
 - [[#description][Description]]
 - [[#install][Install]]
   - [[#layer][Layer]]
   - [[#coq][Coq]]
 - [[#key-bindings][Key bindings]]
   - [[#laying-out-windows][Laying out windows]]
   - [[#managing-prover-process][Managing prover process]]
   - [[#prover-queries][Prover queries]]
   - [[#moving-the-point][Moving the point]]
   - [[#inserting][Inserting]]
 - [[#faq][FAQ]]
   - [[#there-are-empty-square-boxes-in-place-of-math-operators][There are empty square boxes in place of math operators]]

* Description
This layer adds support for the [[https://coq.inria.fr/][Coq]] proof assistant (adapted from
[[https://github.com/tchajed/spacemacs-coq]]).

* Install
** Layer
To use this configuration layer, add it to your =~/.spacemacs=. You will need to
add =coq= to the existing =dotspacemacs-configuration-layers= list in this file.

** 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.

* Key bindings
All Coq specific bindings are prefixed with the major-mode leader ~SPC m~.

** Laying out windows

| Key Binding | Description           |
|-------------+-----------------------|
| ~ll~        | Re-layout windows     |
| ~lc~        | Clear response buffer |
| ~lp~        | Show current proof    |

** Managing prover process

| Key Binding | Description                                                     |
|-------------+-----------------------------------------------------------------|
| ~pc~        | Interrupt prover                                                |
| ~px~        | Quit prover                                                     |
| ~pr~        | Retract buffer - rewinds and moves point to beginning of buffer |
| ~pb~        | Process buffer - processes and moves point to end of buffer     |

** Prover queries
The mnemonic for =a= is "ask".

| Key Binding | Description                                 |
|-------------+---------------------------------------------|
| ~af~        | Search (mnemonic: "find theorems")          |
| ~ao~        | Show an outline of the current proof script |
| ~ap~        | Print                                       |
| ~ac~        | Check                                       |
| ~ab~        | About                                       |
| ~aip~       | Print (showing implicits)                   |
| ~aic~       | Check (showing implicits)                   |
| ~aib~       | About (showing implicits)                   |
| ~anp~       | Print (showing all)                         |
| ~anc~       | Check (showing all)                         |
| ~anb~       | About (showing all)                         |

** Moving the point

| Key Binding | Description                     |
|-------------+---------------------------------|
| ~g.~        | Go to last processed command    |
| ~ga~        | Go to start of command at point |
| ~ge~        | Go to end of command at point   |
| ~gd~        | Go to definition at point       |

** Inserting

| Key Binding | Description                                                     |
|-------------+-----------------------------------------------------------------|
| ~il~        | Extract lemma from current goal - exit with ~C-RET~ (not ~C-j~) |
| ~im~        | Insert =match= on a type                                        |
| ~ie~        | Insert =End <section-name>=                                     |
| ~M-RET~     | Insert regular match branch                                     |
| ~M-S-RET~   | Insert =match goal with= branch                                 |

Note the last two are regular =company-coq= bindings, left alone since they are
most useful in insert mode. The full =company-coq= tutorial showcasing all
available =company-coq= keybindings can be accessed at any time using =SPC SPC
company-coq-tutorial=.

* FAQ
** 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/user-config=.

#+BEGIN_SRC emacs-lisp
(with-eval-after-load 'company-coq
  (add-to-list 'company-coq-disabled-features 'prettify-symbols))
#+END_SRC