MCP-RoCQ：Coq 推理服务器

MCP-RoCQ：Coq 推理服务器

RoCQ 是一个集成 Coq 的推理服务器，支持自动化类型检查、归纳类型定义和属性证明。

GitHub
Created Byangrysky56angrysky56

快速入门

  1. 安装 Coq 平台 8.19 (2024.10)。

  2. 克隆本仓库并安装依赖：

    git clone https://github.com/angrysky56/mcp-rocq.git
cd mcp-rocq
uv venv
./venv/Scripts/activate
uv pip install -e .
pip install -r requirements.txt

  3. 配置 JSON 文件（适用于 Claude 或 mcphost）： 修改路径以匹配您的 Coq 和仓库位置。

  4. 使用以下功能与服务器交互：

    • 类型检查：发送 type_check 工具请求。
    • 归纳类型定义：使用 define_inductive 工具。
    • 属性证明：调用 prove_property 工具。

详细示例请参考 README。