User interfaces

Editor-support packages

Coq projects can be developed with a variety of editors thanks to great support provided through user-contributed extensions. Here, we list such support extensions that are actively used and maintained:

  • VsCode users can use the VsCoq extension that is actively maintained by Maxime Dénès as part of coq-community. VsCoq was initially authored by C.J. Bell, but was left unmaintained for several years before being forked in coq-community.
  • Emacs users can use the major Coq mode Proof General, that can be extended by the minor Coq mode Company-Coq. Proof General was one of the first user interface for proof assistants, and is one of the most used user interface for Coq today. Proof General and Company-Coq give access to many productivity shortcuts, including auto-completion and documentation. On the other hand, async proof processing is not supported.
  • Vim users can use the actively maintained Coqtail extension. This extension is partly based upon a previous, and now unmaintained, Vim extension called Coquille.
  • NeoVim users can use Julien Lepiller's Coquille fork.

An experimental alternative to the editors mentioned above is the computational notebook interface provided by Jupyter. A Jupyter kernel for Coq is available if you want to try this interface, for instance for pedagogical or readability purposes. One of the advantages of using a Jupyter notebook is that you can save and display a selection of intermediate proof steps, which your reader will see without the need to reexecute the document.

Standalone interfaces

Alternatively, you can use CoqIDE, which is developed and distributed alongside Coq. CoqIDE relies on Coq's XML protocol for IDEs and implements all of the features provided by this protocol, meaning in particular asynchronous evaluation. CoqIDE comes with standard basic Emacs-like bindings and with some specific Coq-related bindings but, as an editor, it is not as complete as a general-purpose editor could be (for instance it does not have automatic indentation).

As a way to try Coq without installing anything, you can use JsCoq. JsCoq loads Coq entirely in your browser. However, it is too limited to conduct actual projects: it lacks access to the VM and native computing machineries of Coq, and may hit out-of-memory and stack-overflow failures quicker than native versions of Coq.

Experimental / discontinued interfaces

There have been many experiments over the years. Here are some additional user interfaces that have stayed at the experimental level or whose maintenance has been discontinued and or is currently uncertain:

  • Proof General also has an experimental async branch that relies on Coq's XML protocol for IDEs, and supports new features such as asynchronous proof processing. Unfortunately, this branch is mostly unmaintained and quite unstable.
  • The Coqoon Eclipse plugin was initially based upon the PIDEtop Coq plugin (following Wenzel's asynchronous PIDE framework). Support for more recent versions of Coq (8.7 and 8.8) relies on Coq's XML protocol for IDEs.
  • The PeaCoq online web interface for Coq was focused on teaching (actively developed from 2014 to 2016).
  • The ProofWeb online web interface for Coq (and other proof assistants) was also focused on teaching (in 2006-2007).
  • ProverEditor was an experimental Eclipse plugin with support for Coq (in 2005-2006).
  • Pcoq (discontinued in 2003) was a first experiment at proof-by-pointing.