A collection of extensions for Proof General's Coq mode.
See screenshots below, or jump right to setup instructions and try the tutorial with M-x company-coq-tutorial after setting up!
Download and install Proof General from GitHub:
git clone https://github.com/ProofGeneral/PG ~/.emacs.d/lisp/PG
make -C ~/.emacs.d/lisp/PG
Then add the following to your .emacs
:
;; Open .v files with Proof General's Coq mode
(require 'proof-site "~/.emacs.d/lisp/PG/generic/proof-site")
MELPA is a repository of Emacs packages. Skip this step if you already use MELPA. Otherwise, add the following to your .emacs
and restart Emacs:
(require 'package)
(add-to-list 'package-archives '("melpa" . "http://melpa.org/packages/") t)
(package-initialize)
This should be easier: company-coq
is on MELPA. Just use M-x package-refresh-contents RET followed by M-x package-install RET company-coq RET to install and byte-compile company-coq
and its dependencies. Some of them will produce a few warnings; that's OK.
Add the following to your .emacs
:
;; Load company-coq when opening Coq files
(add-hook 'coq-mode-hook #'company-coq-mode)
You can check out the interactive tutorial by pressing M-x company-coq-tutorial RET. See also the screenshots below!
company-coq
should be pretty transparent. Completion windows will pop up when company-coq
has suggestions to make. By default, this would be when you start writing a tactic name or a command. You can also launch manual completion by using C-RET (or whatever was originally assigned to proof-script-complete
in Coq mode).
Once auto-completion has started, the following key bindings are available:
- RET selects a completion
- C-g interrupts completion.
- C-h and <f1> display documentation for the currently highlighted keyword, identifier, or tactic.
- C-M-v scrolls down in the documentation window.
- C-w opens source view when available (alternatively, pressing M-. browses to the definition of the identifier at point).
Selecting a completion often inserts a snippet with holes at the current point (company-coq
uses yasnippet
as the snippet backend). You can move between holes by using <tab> and S-<tab>.
Loading company-coq
also binds the following keys:
- M-RET inserts a new
match
case (| _ => _
). - M-S-RET inserts a new
match goal
rule (| [ H: _ |- _ ] => _
). - C-c C-a C-x extracts the current goal into a separate lemma.
- C-down-mouse-1 (i.e. C-click) shows an inline quick help box for the identifier under point. The box disappears when the mouse is released. Pressing the <menu> key also works.
- M-. jumps to the source of the identifier at point, when available.
- C-c C-p opens the documentation of the identifier at point (for theorems, and definitions; for tactics, use C-h during completion).
- C-c C-, opens an outline of the code in a separate buffer (using
occur
). - C-c C-/ folds the current code block, or all blocs in the file if repeated.
- C-c C-\ unfolds the current code block, or all blocs in the file if repeated.
- C-c C-& looks up (grep) the current word in files in the current directory subtree.
- C-c C-a C-e tries to match the last output to a documented error message, and displays the relevant section of the manual if it finds one.
- C-c C-a C-d parses the last unification error, and shows a diff of the two types that can't unify.
- Most completion engines support fuzzy matching: you can type
Require Import C.N..Ab.ZPa
and press RET to insertCoq.Numbers.Integer.Abstract.ZParity
, and typingsetrewin
is enough to insertsetoid_rewrite term in ident
. You can (and must) omit spaces:SLD
will insertSet Ltac Debug
(of courseSetLtDeb
will also work), andULD
will insertUnset Ltac Debug
. - Using M-S-RET to insert new cases in a
match goal
saves a lot of time (and finger contortions). - The point-and-click feature (quick help) also works in non-graphic mode, if you enable
xterm-mouse-mode
. company-coq
improves on some of Proof General's features. Try C-c C-a RET nat RET.
company-coq
is implemented as a collection of small modules implementing independent features; check out M-x customize-variable RET company-coq-disabled-features RET
and M-x customize-group RET company-coq RET
for more info!
If you see blank squares appear where there should be math symbols (forall
, exists
, etc.), or if some lines suddenly become very tall, you may be missing a proper math font. See Installing a math font, or insert the following snippet in your .emacs to disable symbols beautification:
;; Disable symbol prettification
(setq company-coq-disabled-features '(prettify-symbols))
On the other hand, if you like that feature so much, you can enable it in the terminal:
(setq company-coq-features/prettify-symbols-in-terminals t)
Technical note: Proof General also offers a Unicode keywords facility. company-coq
's implementation is based on the prettify-symbols-mode
facility found in Emacs 24.4+, yielding a more compact (and faster?) implementation.
Use company-coq-cite
to insert the BibTeX entries for Coq, Proof General, and company-coq
in the current buffer.
@InProceedings{CompanyCoq2016,
Title = {Company-Coq: Taking Proof General one step closer to a real IDE},
Author = {Pit-Claudel, Clément and Courtieu, Pierre},
Booktitle = {CoqPL'16: The Second International Workshop on Coq for PL},
Year = {2016},
Month = jan,
Doi = {10.5281/zenodo.44331},
Url = {http://dx.doi.org/10.5281/zenodo.44331}
}
For font beautification to work properly, you'll need a font with proper symbol support. Symbola, FreeMono, STIX Math, Segoe UI Symbol, Latin Modern, and Cambria Math will all work. If Emacs doesn't fallback properly, you can use the following snippet:
(set-fontset-font t 'unicode (font-spec :name "YOUR-USUAL-FONT"))
(set-fontset-font t 'unicode (font-spec :name "Symbola") nil 'append)
Using a variable-width font for symbols will break indentation. See this other project of mine to download a monospace-friendly symbols font. You'll want to replace the snippet above by following (adjusting Symbola
and DejaVu sans Mono
as appropriate):
(set-fontset-font t 'unicode (font-spec :name "DejaVu Sans Mono"))
(set-fontset-font t 'unicode (font-spec :name "Symbola monospacified for DejaVu Sans Mono") nil 'append)
If possible, company-coq
will use the alert
library to display notifications when long-running proofs complete. alert
is only needed on Windows and OSX; on Linux systems with DBus this should work out of the box. You can try it out by running the snippet below and opening another application while the proof runs; after 10 seconds company-coq will show a notification.
Goal True.
Fail timeout 10 repeat pose 1.
Adjust and use the following snippet to register your own keywords. This needs be called before (company-coq-mode)
, so the code needs to be added after the code listed above.
(add-hook 'coq-mode-hook
(lambda ()
(set (make-local-variable 'prettify-symbols-alist)
'((":=" . ?≜) ("Proof." . ?∵) ("Qed." . ?■)
("Defined." . ?□) ("Time" . ?⏱) ("Admitted." . ?😱)))))
Greek symbols can be obtained using the following mappings:
'(("Alpha" . ?Α) ("Beta" . ?Β) ("Gamma" . ?Γ)
("Delta" . ?Δ) ("Epsilon" . ?Ε) ("Zeta" . ?Ζ)
("Eta" . ?Η) ("Theta" . ?Θ) ("Iota" . ?Ι)
("Kappa" . ?Κ) ("Lambda" . ?Λ) ("Mu" . ?Μ)
("Nu" . ?Ν) ("Xi" . ?Ξ) ("Omicron" . ?Ο)
("Pi" . ?Π) ("Rho" . ?Ρ) ("Sigma" . ?Σ)
("Tau" . ?Τ) ("Upsilon" . ?Υ) ("Phi" . ?Φ)
("Chi" . ?Χ) ("Psi" . ?Ψ) ("Omega" . ?Ω)
("alpha" . ?α) ("beta" . ?β) ("gamma" . ?γ)
("delta" . ?δ) ("epsilon" . ?ε) ("zeta" . ?ζ)
("eta" . ?η) ("theta" . ?θ) ("iota" . ?ι)
("kappa" . ?κ) ("lambda" . ?λ) ("mu" . ?μ)
("nu" . ?ν) ("xi" . ?ξ) ("omicron" . ?ο)
("pi" . ?π) ("rho" . ?ρ) ("sigma" . ?σ)
("tau" . ?τ) ("upsilon" . ?υ) ("phi" . ?φ)
("chi" . ?χ) ("psi" . ?ψ) ("omega" . ?ω))
in which case you may want to use a custom font for Greek characters:
(set-fontset-font t 'greek (font-spec :name "DejaVu Sans Mono"))
The procedure above will give you auto-completion and documentation for tactics, commands, and theorems that you define locally, but not for theorem names and symbols defined in the libraries you load. To get the latter, add the following to your .emacs
, before (company-coq-mode)
:
(setq company-coq-live-on-the-edge t)
This feature won't work unless you build and use a patched coq REPL: see this fork. Two of the relevant patches has been merged upstream (into Coq trunk, not 8.5); the last one is being discussed here.
You can download these changes as patches for 8.4, 8.5 or trunk.
See dependencies in Cask
file.
Many thanks to Pierre Courtieu for his work on Proof General, and to Jonathan Leivent and Jason Gross for their tireless bug reports and suggestions!