rocq-lsp
rocq-lsp is a Language Server Protocol (LSP) implementation for the Rocq Prover (formerly Coq), designed to provide advanced IDE features for formal proof development. It offers continuous incremental document checking, real-time interruptions and limits, programmable error recovery, and support for literate Markdown and LaTeX documents. The server implements the standard LSP protocol with custom extensions, the Petanque protocol for low-latency interaction ideal for AI applications, and upcoming MCP protocol support for LLM context standardization. Key capabilities include multiple workspaces, positional goals, information panels, performance data, completion, jump to definition, and an extensible command-line compiler with plugin support. Built on the Flèche document checking engine, rocq-lsp is designed for interactive use and web-native environments. The project includes a Visual Studio Code extension and supports integration with other editors including Emacs, Vim, and Neovim through separate community p