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

Related MCP server: Chiasmus

Instalación

1. 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

2. 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.

3. 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.