fe168f07b3
README: - add `SPC m` prefixes to follow the style of the other READMEs - Sort key bindings alphabetically Key bindings changes made to be more mnemocnic and/or to better fit the other key bindings of other layers: - SPC m p b --> SPC m p p (show prover process buffer) - SPC m p c --> SPC m p i (interrupt prover process) - SPC m p x --> SPC m p q (quit prover process, maybe SPC m p k for kill would be better ?) - SPC m a p --> SPC m a a to print query - SPC m a n p --> SPC m a A to print query showing all - SPC m a i p --> SPC m a i i to print query showing implicits - Ask showing all bindings use the same keys as regular Ask but the last key is capitalized, example: SPC m a b (ask about) and SPC m a B (ask about showing all) - Ask showing implicits are still on SPC m a i (we could also use Control key, for instance SPC m a b (ask about) and SPC m a C-b (ask about show implicit), it depends on how frequent showing implicits are used). - SPC m g . --> SPC m g l (go to end of Locked command) - SPC m g d --> SPC m g g (using the jump handlers facility of Spacemacs) - SPC m g a --> SPC m g s (to go to start of command)
104 lines
4.4 KiB
Org Mode
104 lines
4.4 KiB
Org Mode
#+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
|
|
** Laying out windows
|
|
|
|
| Key Binding | Description |
|
|
|-------------+-----------------------|
|
|
| ~SPC m l c~ | Clear response buffer |
|
|
| ~SPC m l l~ | Re-layout windows |
|
|
| ~SPC m l p~ | Show current proof |
|
|
|
|
** 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 |
|
|
|
|
** Prover queries
|
|
The mnemonic for =a= is "ask".
|
|
|
|
| Key Binding | Description |
|
|
|---------------+---------------------------------------------|
|
|
| ~SPC m a a~ | Print |
|
|
| ~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 |
|
|
|
|
** 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 |
|
|
|
|
** Inserting
|
|
|
|
| Key Binding | Description |
|
|
|-----------------+-----------------------------------------------------------------|
|
|
| ~SPC m M-RET~ | Insert regular match branch |
|
|
| ~SPC m M-S-RET~ | Insert =match goal with= branch |
|
|
| ~SPC m i e~ | Insert =End <section-name>= |
|
|
| ~SPC m i l~ | Extract lemma from current goal - exit with ~C-RET~ (not ~C-j~) |
|
|
| ~SPC m i m~ | Insert =match= on a type |
|
|
|
|
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
|