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 theorem names defined in the same buffer, with type annotations.

• Easy access to Proof-General's templates (using yasnippet), with smart templates for sections and modules.

• Auto-completion of (most of) Coq's tactics and commands, with snippets auto-extracted from the manual.

• Fuzzy auto-completion of module names in Import commands.

• Auto-completion of identifiers in proof contexts, and of section and modules names.

• Documentation for (most) auto-completion entries, with excerpts from the manual shown directly in Emacs.

• Interactive proof script outline and in-buffer folding

Advanced features (requires a patched version of coqtop):

• Auto-completion of all known theorem and symbol names, with type annotations.

(notice the help string in the mini-buffer)

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

sudo apt-get install coq

sudo apt-get install proof-general

(or from source)

M-x package-install RET company-coq RET

(require 'package)
(add-to-list 'package-archives '("melpa" . "http:https://melpa.org/packages/") t)
(package-initialize)

Compiling the dependencies of company-coq 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)

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 or identifier.
• C-M-v scrolls down in the documentation window.
• C-w opens the relevant section of the documentation, scrolling to the part about the currently highlighted keyword or identifier. Using C-w allows you scroll up (C-M-S-v) in the documentation window to see more context.

You can customize these keybindings by editing company-active-map.

Selecting a completion generally often 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:

• 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-, opens an outline of the code in a separate buffer (using occur).

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-autocomplete-symbols-dynamic t)

This feature won't work well unless you build and use a patched coq REPL. This patch should work well for 8.4pl2 and pl3; this one should work on 8.5 and trunk.

Modules, context and symbols 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)

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

M-x package-refresh-contents RET
M-x package-install RET company RET
M-x package-install RET company-math RET
M-x package-install RET yasnippet RET

(add-to-list 'load-path "~/.emacs.d/lisp/ProofGeneral/generic/")
(add-to-list 'load-path "~/.emacs.d/lisp/company-coq/")
(require 'company-coq)