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 (Servidor de razonamiento Coq)

Actualmente se muestran herramientas, pero Claude no puede usarlas correctamente por alguna razón: la sintaxis no válida generalmente parece ser el problema, pero podría haber algo más.

Quizás haya una mejor manera de configurar esto con la CLI de Coq o algo similar. Si alguien sabe lo que hace y quiere intentar solucionarlo, sería genial.

MCP-RoCQ es un servidor de Protocolo de Contexto de Modelo que proporciona capacidades avanzadas de razonamiento lógico mediante la integración con el asistente de pruebas Coq. Permite la verificación automatizada de tipos dependientes, la definición inductiva de tipos y la verificación de propiedades con tácticas personalizadas y automatización.

Características

Comprobación automatizada de tipos dependientes : verifique términos contra tipos dependientes complejos
Definición de tipo inductivo : defina y verifique automáticamente tipos de datos inductivos personalizados
Comprobación de propiedades : pruebe propiedades lógicas utilizando tácticas personalizadas y automatización
Integración del protocolo XML : comunicación estructurada confiable con Coq
Manejo de errores enriquecido : comentarios detallados sobre errores de tipo y pruebas fallidas

Instalación

Instalar la plataforma Coq 8.19 (2024.10)

Coq es un sistema de gestión de pruebas formales. Proporciona un lenguaje formal para escribir definiciones matemáticas, algoritmos ejecutables y teoremas, junto con un entorno para el desarrollo semiinteractivo de pruebas verificadas por máquina.

https://github.com/coq/platform

Clonar este repositorio:

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

cd al repositorio

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

JSON para la aplicación Claude o configuración de mcphost: configure sus rutas de acuerdo con cómo instaló coq y el repositorio.

    "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"
      ]
    },

Esto podría funcionar. Lo hice funcionar con luz ultravioleta y la mayor parte de esto podría ser alucinante.

Instalar dependencias:

pip install -r requirements.txt

Uso

El servidor proporciona tres capacidades principales:

1. Comprobación de tipos

{
    "tool": "type_check",
    "args": {
        "term": "<term to check>",
        "expected_type": "<type>",
        "context": ["relevant", "modules"] 
    }
}

2. Tipos inductivos

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

3. Prueba de propiedad

{
    "tool": "prove_property",
    "args": {
        "property": "<statement>",
        "tactics": ["<tactic sequence>"],
        "use_automation": true
    }
}

Licencia

Este proyecto está licenciado bajo la licencia MIT: consulte el archivo de LICENCIA para obtener más detalles.

This server cannot be installed

-

security - not tested

A

license - permissive license

-

quality - not tested

MCP-RoCQ se integra con el asistente de prueba Coq para permitir la verificación de tipos dependientes automatizada, definiciones de tipos inductivos y comprobación de propiedades a través de la comunicación del protocolo XML.

Related Resources

Reddit Discussion about this server