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 install either the VsCoq extension, or the coq-lsp extension. Both extensions are now based on the Language Server Protocol standard, with custom extensions.
• Emacs users can use the major Coq mode Proof General, that can be extended by the minor Coq mode Company-Coq.
• Vim/NeoVim users can use the Coqtail extension. NeoVim users can also test the experimental support for VsCoq's vscoqtop server or for coq-lsp.

Alternatively, you can use CoqIDE, a standalone desktop application which is developed and distributed alongside Coq.

As a way to try Coq without installing anything, you can use JsCoq. JsCoq loads Coq entirely in your browser.

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

• A Jupyter kernel for Coq (supports Coq 8.6 and newer versions using Coq's XML protocol for IDEs).
• 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.