项目简介

'Rocq MCP Server' 是一个基于 Model Context Protocol (MCP) 的后端服务，旨在让大型语言模型 (LLM) 能够以标准化的方式与 Rocq/Coq 证明助手进行交互。它通过暴露一系列工具，将 Rocq/Coq 的功能提供给 MCP 兼容的 LLM 客户端（如 Claude Desktop），从而实现对定理证明的自动化辅助和智能交互。

主要功能点

定理证明交互: 启动证明会话，逐步执行策略或命令，进行交互式定理证明。
证明状态查询: 获取当前证明目标的详细信息，以及当前证明状态下可用的引理和定义。
代码分析: 解析 Coq/Rocq 命令的抽象语法树 (AST)，或查询文件中特定位置的证明状态。
内容检索: 获取 Coq/Rocq 文件的目录（可用的定义和定理），并支持在当前上下文中搜索定理或定义。
会话管理: 支持创建和管理多个并发的证明会话。
两种通信模式: 支持通过标准输入/输出 (Stdio) 或 TCP/IP 套接字与 'pet' 进程进行通信，适应单客户端或多客户端使用场景。

安装步骤

在安装 Rocq MCP 服务器之前，您需要先安装 'coq-lsp' 并确保其支持 Petanque 协议。

安装 'coq-lsp' 并支持 Petanque: 请确保您已安装 OCaml 的包管理器 'opam'。
```
opam install lwt logs coq-lsp
```

安装 Rocq MCP 服务器: 推荐使用 'uv' 包管理器进行安装（如果没有 'uv'，可以使用 'pip'）。

uv pip install git+https://github.com/llm4rocq/rocq-mcp.git

如果您更习惯使用 'pip'：

pip install git+https://github.com/llm4rocq/rocq-mcp.git

服务器配置（MCP客户端使用）

MCP客户端需要配置 Rocq MCP 服务器的启动命令及其参数才能建立连接。以下是两种常用模式的配置示例：

默认 Stdio 模式（推荐用于单客户端）： 此模式下，MCP客户端会直接通过标准输入/输出来运行 'rocq-mcp' 命令。

{
  "server_name": "rocq-mcp",
  "command": "rocq-mcp",
  "args": [],
  "description": "Rocq MCP 服务器 (Stdio 模式)"
}

TCP 模式（推荐用于多客户端或远程连接）： 此模式下，'rocq-mcp' 将作为一个独立的服务器进程运行，MCP客户端通过 TCP 连接。在启动 MCP 客户端前，需要先手动启动 'rocq-mcp' 服务器： 'rocq-mcp --tcp --host 127.0.0.1 --port 8833'

然后配置 MCP 客户端连接到该服务器：

{
  "server_name": "rocq-mcp",
  "command": "rocq-mcp",
  "args": ["--tcp", "--host", "127.0.0.1", "--port", "8833"],
  "description": "Rocq MCP 服务器 (TCP 模式)"
}

请确保配置中的 'host' 和 'port' 与您启动 'rocq-mcp' 服务器时使用的参数一致。

基本使用方法

以一个 MCP 兼容的客户端（如 Claude Desktop）为例：

添加 MCP 服务器到客户端：

claude mcp add rocq-mcp -- rocq-mcp
# 如果您使用 uv 工具链：
# claude mcp add rocq-mcp -- uv run rocq-mcp

在 Claude 会话中验证服务器状态： 启动一个 Claude 会话，并输入 '/mcp' 命令。您应该能看到 'rocq-mcp' 服务器的列表。
向 Claude 提问以使用 Rocq/Coq 工具： 现在，您可以向 Claude 提问，它将能够利用 Rocq MCP 服务器提供的工具来辅助 Rocq/Coq 证明。例如： 'help me prove addnC in test.v' Claude 将能够调用 'rocq_start_proof' 等工具来开始并辅助您的证明过程。

关键词

项目简介

主要功能点

安装步骤

服务器配置（MCP客户端使用）

基本使用方法

信息