Basic architecture of Coq User Interfaces

General design

User interfaces for Coq are generally made of the following components:

• a graphical interface that provides access to graphical features (editing, highlighting, completion, extracting information, ...), generally called the client
• a server, extending Coq:
  • to associate specific Coq actions to specific graphical actions
  • to provide a document manager to manage interactivity: backtracking, updating, ...
• a protocol between the client and the server

In some cases, the actions are implemented directly in the graphical interface (e.g. for some Proof General features).

We list below the different components. A table of user interfaces summarizing the main combinations can be found at the end of the page.

Graphical clients

The graphical interfaces manage interactive actions of the user:

• it maps mouse and keyboard events to a language of semantic actions
• it renders the results of these actions
• in general, actions have a semantic part which is provided by a server with which the graphical interface communicates (though some actions, like adding a character, are generally managed direction by the interface)
• it maintains a state of interaction

The main graphical interfaces available are typically:

• standard editors:
  • either stand-alone: VsCode/VsCodium, Emacs, Vim/NeoVim, Jupyter, ...
  • or in the browser: VsCode.dev, Jupyter, ...
• custom editors: CoqIDE, based on the lablgtk3 wrapper to gtk+3
• custom browser editors such as e.g. CodeMirror (jsCoq 1), or CodeMirror and ProseMirror (jsCoq 2)

The language to implement (new) graphical features in graphical interfaces is:

• VsCode/VsCodium: TypeScript
• Emacs: Elisp
• Vim: Vim script
• Jupyter: Python, JavaScript
• CoqIDE: OCaml
• CodeMirror, ProseMirror: JavaScript?

All the interfaces above support editing, highlighting, completion, go-to-error, a variety of shortcuts. Standard editors generally come with a rich variety of shortcuts or extensions.

Document managers

A document manager handles the interactive development of proof assistant documents. It provides methods to:

• add contents to the proof assistant environment
• query the proof assistant environment
• support backtracking to a previous version of the environment

The main document managers, all part of Coq or linked with Coq, are:

• the (historical) Coq Reset mechanism, used by Proof General
• the State Transition Machine (STM) manager, used by the coqidetop, serapi and jsCoq 1 servers
• the VsCoq 2 document manager used by the VsCoq 2 server
• Flèche used by coq-lsp

Document managers can be more or less sophisticated:

• e.g. some provide a tree or graph-like environment with local addition or removal of nodes, according to dependency rules, and thus supporting an asynchronous evaluation of documents controlled by a scheduler; this is the case of the STM, the VsCoq 2 document manager, and Flèche

Communication protocols

The main protocols to communicate with Coq are:

• textual: passing Coq commands over a channel
• Coq XML-based protocol, which supports asynchronous evaluation of commands and a few features (such as structured goals)
• the LSP protocol, extended with specific features for interactive proof development (VsCoq 2 extension of LSP, coq-lsp extension of LSP)
• the Serapi protocol using either JSON or SEXP syntax, encapsulating the STM API

Servers

The main available servers are:

• coqtop with "-emacs" option: provides a (slightly-enriched) textual communication where querying and backtracking have the form of ordinary commands

• coqidetop: which is accessed through the XML protocol

• serapi server and jsCoq 1 server: used in research and for the jsCoq 1 interface client

• VsCoq 2 server: which is accessed through the LSP protocol and which is used by the VsCoq 2 vscode client

• coq-lsp server: which is accessed through the LSP protocol and which is used by the coq-lsp client and by jsCoq 2

Main combinations of client/server

GUI	client	server	document manager
ProofGeneral	Emacs	coqtop	coqtop backtracking mechanism
CoqIDE	Custom Gtk+3 interface	coqidetop	STM
jsCoq 1	browser (node + CodeMirror)	coqidetop	STM
jsCoq 2	browser (node + CodeMirror + ProseMirror)	coq-lsp server	Flèche
VsCoq 1	VsCode/VsCodium	coqidetop	STM
VsCoq 2	VsCode/VsCodium	VsCoq 2 server	VsCoq 2 document manager
coq-lsp	VsCode (or browser)	coq-lsp server	Flèche
Jupyter	browser	coqidetop	STM
Coqtail	Vim/NeoVim	coqidetop	STM

Features

All of them support editing, highlighting, completion, go-to-error, a variety of shortcuts. Support for specific features include:

List to be continued:

• CoqIDE: Ltac debugger, specific shortcut for printing/querying, asynchronous evaluation of documents, Unicode input method, proof difference highlighting, ...
• Coqtail: specific shortcut for printing/querying, script indentation, proof difference highlighting, ...
• Proof General: specific shortcut for printing/querying, Unicode input method, proof difference highlighting, auto-compilation on Require, script indentation, auto-insertion of suggested Proof using annotations.
• VsCoq 1: proof difference highlighting, ...
• VsCoq 2: ...
• coq-lsp: ...
• Jupyter: ...

Unmaintained interfaces

Here is a list of unmaintained interfaces:

• PIDEtop: based on Wenzel's asynchronous PIDE framework for Isabelle, using the XML protocol
• Coqoon: Eclipse using the XML protocol
• PeaCoq: online web interface for Coq was focused on teaching (actively developed from 2014 to 2016)
• ProofWeb: online web interface for Coq (and other proof assistants); was also focused on teaching (in 2006-2007).
• ProverEditor: an experimental Eclipse plugin with support for Coq (in 2005-2006).
• Pcoq (discontinued in 2003): was a first experiment at proof-by-pointing.
• Papuk: a modified CoqIDE for teaching
• Elcoq.el: serapi-based emacs interface
• Coquille: a precursor of Coqtail for Vim

Related tools

• Alectryon: produces annotated Coq documents using Serapi

See also

• The Coq Zulip channel on user interfaces
• A 2019 discussion about ProofGeneral, VsCode and LSP on discourse