spacemacs/layers/+lang/coq

Coq layer

• Description
  • Features:
• Install
  • Layer
  • Coq
• Troubleshooting
  • There are empty square boxes in place of math operators
• Key bindings
  • Laying out windows
  • Managing prover process
  • Getting documentation
  • Prover queries
  • Moving the point
  • Inserting
  • Options

Description

This layer adds support for the Coq proof assistant (adapted from 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.

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

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.

Options

Key binding	Description
SPC m T e	Toggle electric terminator.