https://github.com/cpitclaudel/company-coq.git
git clone 'git://github.com/cpitclaudel/company-coq.git'
Company backend for Proof-General's Coq mode. Setup should be pretty straightforward, although the most advanced features require a patched version of coqtop.
Auto-completion of math symbols (using company-math).
Auto-completion of theorems and tactics defined in the same buffer.
Fuzzy auto-completion of (most of) Coq's tactics and commands, with snippets auto-extracted from the manual.
Fuzzy auto-completion of library module names in Import commands.
Auto-completion of hypotheses in proof contexts, and of section and modules names.
Auto-completion of search results: after running a search, results are available as completions.
Easy access to Proof-General's templates (using yasnippet), with smart templates for sections and modules.
Documentation for (most) auto-completion entries, with excerpts from the manual shown directly in Emacs.
Documentation for many error messages, with automagic matching of the last error message against errors documented in the manual.
Interactive lemma extraction: press C-c C-a C-x to extract the current goal into a separate lemma, keeping the hypotheses of your choice.
Convenient snippets: easily insert new match cases and match goal rules.
Visual word diff of large unification error messages (The term “blah” has type “huge blob” while it is expected to have type “slightly different blob”).
Interactive proof script outline and in-buffer folding.
Basic project search (search for instances of the word at point in neighboring files).
Extended font beautification: keywords are transparently replaced with the corresponding symbols (⊢⊤⊥→⇒λ∀∃∧∨¬≠⧺𝓝ℤℕℚℝ𝔹𝓟), and the goals line (========) actually looks like a line (════════).
Minimal quick help (inline documentation).
Automatic highlighting of deprecated forms (assert (_ := _), SearchAbout, etc.).
Occur in *coq* buffer (company-coq-search-in-coq-buffer).
Limited form of source view for same-buffer definitions, or using company-coq-location-defun (needs .v files).
(These require a patched version of coqtop)
Auto-completion of all known types and theorems with annotations, and of all user-defined tactics and tactic notations.
Source view for auto-completed symbols and user-defined tactics (needs .v files). Works to a limited with an unpatched coqtop.
Currently works for symbols and user-defined tactics (prover must be started)
coqtop, see notes)
(notice the help string in the mini-buffer)
coqtop)
coqtop)
Note: You need a version of Emacs ≥ 24 for this to work properly. You can check which version you are running with M-x emacs-version RET. Note that some features, like beautification of symbols or syntax highlighting in the manual, only work with emacs ≥ 24.4.
sudo apt-get install proof-general(or from source)
company-coq is on MELPA. First add the following to your .emacs and restart emacs.
(require 'package)
(add-to-list 'package-archives '("melpa" . "http://melpa.org/packages/") t)
(package-initialize)Then type 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
(package-initialize)
;; Open .v files with Proof-General's coq-mode
(require 'proof-site)
;; Load company-coq when opening Coq files
(add-hook 'coq-mode-hook #'company-coq-initialize)You can check out the interactive tutorial by pressing M-x company-coq-tutorial.
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:
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>. Some snippets (like Print Instances) include multiple choices.
Loading company-coq also binds the following keys:
match case (| _ => _).match goal rule (| [ H: _ |- _ ] => _).occur).Require Import C.N..Ab.ZPa and press RET to insert Coq.Numbers.Integer.Abstract.ZParity.setrewin and pressing RET is enough to insert setoid_rewrite term in ident. You can (and must) omit spaces: SLD will insert Set Ltac Debug (of course SetLtDeb will also work), and ULD will insert Unset Ltac Debug.match goal saves a lot of time (and finger contortions).xterm-mouse-mode.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-enabled font, or insert the following snippet in your .emacs to disable symbols beautification:
;; Disable keyword replacement
(setq company-coq-prettify-symbols nil)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.
For font beautification to work properly, you'll need a font with proper symbol support. DejaVu Sans Mono, Symbola, FreeMono, STIX, Unifont, Segoe UI Symbol, Arial Unicode and Cambria Math do. If Emacs doesn't fallback properly, you can use the following snippet:
(set-fontset-font t 'unicode (font-spec :name "Symbola") nil 'append)Adjust and use the following snippet to register your own keywords. This needs be called before (company-coq-initialize), 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") nil)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-initialize):
(setq company-coq-dynamic-autocompletion t)This feature won't work unless you build and use a patched coq REPL: see this fork. One of the relevant patches has been merged upstream; the other two are being discussed here and here.
Modules, context, symbols, end of block and search results auto-completion can be turned off using the following lines
(setq company-coq-autocomplete-modules nil)
(setq company-coq-autocomplete-context nil)
(setq company-coq-autocomplete-symbols nil)
(setq company-coq-autocomplete-block-end nil)
(setq company-coq-autocomplete-search-results nil)You can set these variables using `M-x customize-group RET company-coq RET
M-x unload-feature RET company-coq RET should work fine.
mkdir -p ~/.emacs.d/lisp/
git clone https://github.com/cpitclaudel/company-coq.git ~/.emacs.d/lisp/company-coq
cd ~/.emacs.d/lisp/company-coq
make package && make install