The Coq Proof Assistant

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:

• Visual Studio Code and VSCodium users can use either of the VsCoq extension, which is actively maintained by several contributors as part of coq-community, or the new coq-lsp extension, which is based on an implementation of the Language Server Protocol standard, with custom extensions. coq-lsp provides continous document checking and position-based document navigation (an interaction model similar to what is found in e.g., Lean, and which departs from the model found in other Coq user interfaces). See coq-lsp's FAQ for more information.
• 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/NeoVim users can use the actively maintained Coqtail extension. This extension is partly based upon a previous, and now unmaintained, Vim extension called Coquille.

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.

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.

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.