MCP Rocq

MCP RoCQ（Coq推理服务器）

目前显示了工具，但由于某种原因，Claude无法正确使用它——无效语法通常是问题所在，但可能还有其他问题。

使用coq-cli或其他工具可能有更好的设置方法。 任何想尝试修复它的人，只要知道他们在做什么，那就太好了。

MCP RoCQ是一个模型上下文协议服务器，通过与Coq证明助手集成提供高级逻辑推理能力。它能够通过自定义策略和自动化实现自动依赖类型检查、归纳类型定义和属性证明。

特性

• 自动依赖类型检查：根据复杂的依赖类型验证术语
• 归纳型定义：定义并自动验证自定义归纳数据类型
• 财产证明：使用自定义策略和自动化证明逻辑属性
• XML协议集成：与Coq进行可靠的结构化沟通
• 丰富的错误处理：类型错误和失败证明的详细反馈

安装

1. 安装Coq平台8.19（2024.10）

Coq是一个正式的证明管理系统。它提供了一种形式化语言来编写数学定义、可执行算法和定理，以及一个用于机器检查证明半交互式开发的环境。

1. 克隆此存储库：

git clone https://github.com/angrysky56/mcp-rocq.git

cd到repo

uv venv
./venv/Scripts/activate
uv pip install -e .

Claude App或mcphost配置的JSON-根据您安装coq和存储库的方式设置路径。

    "mcp-rocq": {
      "command": "uv",
      "args": [
        "--directory",
        "F:/GithubRepos/mcp-rocq",
        "run",
        "mcp_rocq",
        "--coq-path",
        "F:/Coq-Platform~8.19~2024.10/bin/coqtop.exe",
        "--lib-path",
        "F:/Coq-Platform~8.19~2024.10/lib/coq"
      ]
    },

这可能会奏效——我用紫外线启动了它，但其中大部分可能是幻觉：

1. 安装依赖项：

pip install -r requirements.txt

用法

服务器提供三个主要功能：

1.类型检查

{
    "tool": "type_check",
    "args": {
        "term": "",
        "expected_type": "",
        "context": ["relevant", "modules"] 
    }
}

2.归纳类型

{
    "tool": "define_inductive",
    "args": {
        "name": "Tree",
        "constructors": [
            "Leaf : Tree",
            "Node : Tree -> Tree -> Tree"
        ],
        "verify": true
    }
}

3.财产证明

{
    "tool": "prove_property",
    "args": {
        "property": "",
        "tactics": [""],
        "use_automation": true
    }
}

许可证

此项目根据MIT许可证获得许可-有关详细信息，请参阅许可证文件。