local-only server

The server can only run on the client’s local machine because it depends on local resources.

Integrations

The README lists 'XML Protocol Integration' as a feature, describing it as providing 'reliable structured communication with Coq', indicating that the MCP server uses XML for protocol communication.

MCP-RoCQ (Coq推論サーバー)

現在ツールが表示されていますが、何らかの理由で Claude はそれを適切に使用できません。無効な構文が一般的に問題であると思われますが、他に何か原因がある可能性もあります。

coq cli などを使って、もっと良い設定方法があるかもしれません。どなたか、この問題を解決したい方、あるいは何をしているのか分かっている方がいらっしゃいましたら、ぜひ教えてください。

MCP-RoCQは、Coq証明支援ツールとの統合により高度な論理推論機能を提供するモデルコンテキストプロトコル（MCP）サーバーです。カスタムタクティクスと自動化の両方を活用し、依存型チェック、帰納的型定義、プロパティ証明の自動化を可能にします。

特徴

自動依存型チェック:複雑な依存型に対して項を検証する
帰納的型定義:カスタム帰納的データ型を定義し、自動的に検証します
プロパティ証明: カスタム戦術と自動化を使用して論理プロパティを証明します
XMLプロトコル統合: Coqによる信頼性の高い構造化通信
豊富なエラー処理: 型エラーや失敗した証明に関する詳細なフィードバック

インストール

Coq Platform 8.19 (2024.10) をインストールする

Coqは形式的な証明管理システムです。数学的な定義、実行可能なアルゴリズム、定理を記述するための形式言語と、機械検証された証明を半対話的に開発するための環境を提供します。

https://github.com/coq/プラットフォーム

このリポジトリをクローンします:

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

リポジトリにcd

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

Claude アプリまたは 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"
      ]
    },

これはうまくいくかもしれない。UV で実行できたが、そのほとんどは幻覚である可能性がある。

依存関係をインストールします:

pip install -r requirements.txt

使用法

サーバーは主に 3 つの機能を提供します。

1. 型チェック

{
    "tool": "type_check",
    "args": {
        "term": "<term to check>",
        "expected_type": "<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": "<statement>",
        "tactics": ["<tactic sequence>"],
        "use_automation": true
    }
}

ライセンス

このプロジェクトは MIT ライセンスに基づいてライセンスされています - 詳細については LICENSE ファイルを参照してください。

This server cannot be installed

-

security - not tested

A

license - permissive license

-

quality - not tested

MCP-RoCQ は Coq 証明アシスタントと統合され、XML プロトコル通信による自動依存型チェック、帰納的型定義、プロパティ証明を可能にします。

Related Resources

Reddit Discussion about this server