Welcome to coq-lsp, a Language Server Protocol-based extension for the Coq Interactive Proof Assistant
coq-lsp aims to provide a modern and streamlined experience for
VSCode users, relying on the new coq-lsp language
server.
The server provides many nice features such as incremental checking,
advanced error recovery, document information, ... See the server
documentation at the project page for more information and full
changelog.
Features
The coq-lsp VSCode extension relies on the standard VSCode LSP
client by Microsoft, with 2 main addons:
information / goal panel: this will display goals, messages, and
errors at point. It does also support client-side rendering. By
default, Cmd-Enter and mouse click will enable the panel for the
current point.
document checking progress, using the right lane decoration.
See the extension configuration options for more information.
How to install the server:
To install the server please do:
opam install coq-lsp
The server should also appear in the Coq Platform, and likely by other
channels.
