Coq LSP
A language server and VS Code extension providing incremental checking, error recovery, and IDE features for the Rocq/Coq proof assistant.
What is Coq LSP?
Rocq LSP is a Language Server Protocol implementation for the Rocq/Coq proof assistant, providing IDE-like features such as incremental document checking, error recovery, and goal display. It solves the problem of inefficient, stop-and-go proof development by enabling continuous, interactive validation of formal documents.
Researchers, students, and developers working with the Rocq/Coq proof assistant who seek a modern, responsive editing environment with advanced tooling for formal verification and literate programming.
Developers choose Rocq LSP for its incremental checking engine (Flèche), which drastically reduces recompilation time, and its robust error recovery that allows working with partially correct proofs. Its support for multiple protocols and web-native design makes it a versatile platform for both interactive use and research.
Overview
Visual Studio Code Extension and Language Server Protocol for Rocq / Coq [maintainers=@gbdrt,@SkySkimmer,@tabareau]
Use Cases
Best For
- Interactive proof development in Rocq/Coq with real-time feedback
Related Projects
Found a gem we're missing?
Open-Awesome is built by the community, for the community. Submit a project, suggest an awesome list, or help improve the catalog on GitHub.
