Skip to main content
Glama
enesjakozh

MCP-RoCQ

by angrysky56
GitHub
Python
MIT License
2
OverviewInspectNewSchemaRelated ServersReviewsScore
Need Help?View Source CodeReport Issue

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

  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

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

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

How are these scores calculated?

local-only server

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

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.

  1. 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.
    1. Características
    2. Instalación
  2. JSON para la aplicación Claude o configuración de mcphost: configure sus rutas de acuerdo con cómo instaló coq y el repositorio.
    1. Esto podría funcionar. Lo hice funcionar con luz ultravioleta y la mayor parte de esto podría ser alucinante.
      1. Uso
      2. Licencia

    Related Resources

    Related MCP Servers

    • MCP-Logic

      angrysky56
      -
      security
      A
      license
      -
      quality
      MCP-Logic is a server that provides AI systems with automated reasoning capabilities, enabling logical theorem proving and model verification using Prover9/Mace4 through a clean MCP interface.
      Last updated -
      20
      MIT License
      • Linux
      • Apple

    • Trello MCP Server

      andypost
      A
      security
      F
      license
      A
      quality
      Enables interaction with Trello boards, lists, and cards through Model Context Protocol (MCP) tools, leveraging TypeScript for type safety and asynchronous operations.
      Last updated -
      5
      JavaScript

    • MCP Server Starter

      GreatAuk
      A
      security
      A
      license
      A
      quality
      A TypeScript-based template for building Model Context Protocol servers, featuring fast testing, automated version management, and a clean structure for MCP tool implementations.
      Last updated -
      1
      1
      2
      TypeScript
      MIT License

    • MCPKit

      ribeirogab
      -
      security
      F
      license
      -
      quality
      A simple TypeScript library for creating Model Context Protocol (MCP) servers with features like type safety, parameter validation, and a minimal code API.
      Last updated -
      1
      TypeScript
      MIT License

    View all related MCP servers

    Appeared in Searches

    New MCP Servers

    MCP directory API

    We provide all the information about MCP servers via our MCP API.

    curl -X GET 'https://glama.ai/api/mcp/v1/servers/angrysky56/mcp-rocq'

    If you have feedback or need assistance with the MCP directory API, please join our Discord server