552fd5953c
Apple renamed "Mac OS X" to "OS X" in 2012 and then to "macOS" in 2016. Update references to use the current name.
129 lines
5.7 KiB
Org Mode
129 lines
5.7 KiB
Org Mode
#+TITLE: Coq layer
|
|
|
|
#+TAGS: dsl|layer|programming
|
|
|
|
[[file:img/coq.png]]
|
|
|
|
* Table of Contents :TOC_5_gh:noexport:
|
|
- [[#description][Description]]
|
|
- [[#features][Features:]]
|
|
- [[#install][Install]]
|
|
- [[#layer][Layer]]
|
|
- [[#coq][Coq]]
|
|
- [[#troubleshooting][Troubleshooting]]
|
|
- [[#there-are-empty-square-boxes-in-place-of-math-operators][There are empty square boxes in place of math operators]]
|
|
- [[#key-bindings][Key bindings]]
|
|
- [[#laying-out-windows][Laying out windows]]
|
|
- [[#managing-prover-process][Managing prover process]]
|
|
- [[#getting-documentation][Getting documentation]]
|
|
- [[#prover-queries][Prover queries]]
|
|
- [[#moving-the-point][Moving the point]]
|
|
- [[#inserting][Inserting]]
|
|
|
|
* Description
|
|
This layer adds support for the [[https://coq.inria.fr/][Coq]] proof assistant (adapted from [[https://github.com/tchajed/spacemacs-coq][spacemacs-coq]]) to Spacemacs.
|
|
|
|
** Features:
|
|
- Syntax highlighting
|
|
- Syntax-checking
|
|
- Auto-completion
|
|
- 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
|
|
|
|
* 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.
|
|
|
|
* Troubleshooting
|
|
** 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
|
|
|
|
* 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 |
|
|
|
|
** 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 |
|
|
|
|
** 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 c~ | Insert a vernacular command |
|
|
| ~SPC m i e~ | Insert =End <section-name>= |
|
|
| ~SPC m i i~ | Insert =intros= with default variable names |
|
|
| ~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 |
|
|
| ~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 =company-coq= bindings, left alone since they are
|
|
most useful in insert mode. The full =company-coq= tutorial showcasing all
|
|
available =company-coq= key bindings can be accessed at any time using =SPC SPC
|
|
company-coq-tutorial=.
|