mcp-coq-lsp

它的功能

mcp-coq-lsp 是一个 Model Context Protocol (MCP) 服务器，提供 Coq 的语言服务器协议 (LSP) 集成，这是一个形式化证明助手。它使开发人员能够在与 MCP 兼容的环境中使用 Coq，提供完整的 IDE 支持，包括代码补全、错误诊断、文档查找和实时反馈证明开发。

如何设置

安装需要在系统上安装 Coq 及其 LSP 实现。可以通过将其添加到 MCP 客户端配置文件中来配置 MCP 服务器，指定服务器可执行文件路径和任何必要的参数。配置完成后，重新启动 MCP 客户端以激活 Coq LSP 支持。

主要特性

• Coq 的完整语言服务器协议实现
• 实时语法高亮和错误检测
• 代码补全和智能建议
• 悬停文档和类型信息
• 与 MCP 兼容的工具和编辑器的集成
• 支持形式验证和证明开发工作流程