项目介绍
Rocq MCP Server
概述
此MCP服务器通过一组工具暴露了Rocq/Coq证明助手的功能，这些工具可以被兼容MCP的客户端（如Claude Desktop）使用。它使用Pytanque与coq-lsp通过Petanque服务器进行通信。
功能
可用工具
- rocq_start_proof: 对Coq/Rocq文件中的特定定理开始一个证明会话
- rocq_run_tactic: 在当前证明状态下执行战术或命令
- rocq_get_goals: 获取会话的当前证明目标
- rocq_get_premises: 获取当前证明状态下的可用前提（引理、定义）
- rocq_get_file_toc: 获取Coq/Rocq文件的目录（可用定义和定理）
- rocq_search: 在当前上下文中搜索定理、定义和其他对象
- rocq_parse_ast: 解析命令并返回其抽象语法树（仅适用于coq-lsp的开发版本）
- rocq_get_state_at_position: 获取文件中特定位置的证明状态（仅适用于coq-lsp的开发版本）
关键能力
-
两种通信模式：
- 标准输入输出模式（默认）：通过标准输入输出直接与
pet进程通信。 - TCP模式：通过TCP套接字与
pet-server通信。
- 标准输入输出模式（默认）：通过标准输入输出直接与
-
交互式定理证明：逐步执行战术和命令
-
全面反馈：访问所有Rocq消息（错误、警告、搜索结果）
-
状态管理：导航证明状态并比较它们
-
会话管理：支持多个并发证明会话
-
抽象语法树解析：获取命令和文件位置的抽象语法树（仅适用于coq-lsp的开发版本）
-
基于位置的查询：获取文件中特定位置的状态（仅适用于coq-lsp的开发版本）
预备条件
安装带有Petanque支持的coq-lsp：
# 安装依赖项
opam install lwt logs coq-lsp
# 或者安装coq-lsp的一个开发版本，例如针对Coq.8.20
opam install lwt logs coq.8.20.0
opam pin add coq-lsp https://github.com/ejgallego/coq-lsp.git#v8.20
安装
从GitHub安装（推荐）
pip install git+https://github.com/llm4rocq/rocq-mcp.git
开发安装
我们建议使用uv。
- 克隆此仓库
- 使用项目工作流：
cd rocq-mcp uv sync
使用
运行MCP服务器
# 默认：标准输入输出模式（直接使用'pet'命令）
rocq-mcp
# 使用TCP模式以支持多客户端使用
rocq-mcp --tcp
# 带有自定义服务器配置的TCP模式
rocq-mcp --tcp --host 127.0.0.1 --port 8833
开发模式（如果使用uv sync）：
uv run rocq-mcp
uv run rocq-mcp --tcp
通信模式：
- 标准输入输出模式（默认）：直接启动并使用标准输入输出与
pet进程通信。这种方式更高效且简单，因为它不需要单独的服务器进程。 - TCP模式：启动
pet-server进程并通过TCP套接字进行通信。在需要多个应用程序连接到同一Petanque实例的多客户端使用场景中使用此模式。
MCP客户端配置
运行以下命令以在Claude代码中安装rocq-mcp。
claude mcp add rocq-mcp -- rocq-mcp
注意：如果你正在使用虚拟环境，rocq-mcp可能不会默认出现在路径中。首先激活虚拟环境，并复制由which rocq-mcp返回的路径。然后使用这个绝对路径安装rocq-mcp：
claude mcp add rocq-mcp -- /path/to/rocq-mcp
当你启动一个Claude会话时，你可以通过以下命令检查服务器：
> /mcp
然后，只需向Claude提问即可。
> 帮助我证明test.v中的addnC
测试
# 安装开发依赖项
uv sync --dev
# 运行测试
uv run pytest tests/
故障排除
常见问题
服务器连接错误
- 确认端口可用性
- 检查coq-lsp是否正确安装
安装问题
- 确保coq-lsp正确安装
- 在安装
coq-lsp之前安装lwt和logs（pet和pet-server所需） - 确认pytanque依赖项已正确解决
注意：此项目是在Claude的帮助下，基于pytanque的代码构建的。