You are viewing the documentation for the develop branch. The documentation for the release version is here .

Table of Contents

Coq layer

Table of ContentsClose


1. Description

This layer adds support for the Coq proof assistant (adapted from spacemacs-coq) to Spacemacs.

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

2. Install

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

2.2. Coq

Official installers for macOS and Windows are available from:

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

(with-eval-after-load 'company-coq
  (add-to-list 'company-coq-disabled-features 'prettify-symbols))

4. Key bindings

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

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

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

4.7. Options

Key binding Description
SPC m T e Toggle electric terminator.

Author: root

Created: 2021-09-29 Wed 20:45