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 证明助手集成,提供高级逻辑推理功能。它支持自动依赖类型检查、归纳类型定义和属性证明,并支持自定义策略和自动化功能。
特征
- 自动依赖类型检查:根据复杂的依赖类型验证术语
- 归纳类型定义:定义并自动验证自定义归纳数据类型
- 属性证明:使用自定义策略和自动化来证明逻辑属性
- XML 协议集成:与 Coq 进行可靠的结构化通信
- 丰富的错误处理:类型错误和失败证明的详细反馈
安装
- 安装 Coq 平台 8.19(2024.10)
Coq 是一个形式化证明管理系统。它提供了一种用于编写数学定义、可执行算法和定理的形式化语言,并提供了一个用于机器验证证明的半交互式开发环境。
https://github.com/coq/platform
- 克隆此存储库:
Copy
cd 到 repo
Copy
Claude App 或 mcphost 配置的 JSON - 根据您安装 coq 和存储库的方式设置您的路径。
Copy
这可能有效——我用紫外线照射它,但其中大部分可能是幻觉:
- 安装依赖项:
Copy
用法
该服务器提供三种主要功能:
1.类型检查
Copy
2. 归纳类型
Copy
3. 财产证明
Copy
执照
该项目根据 MIT 许可证获得许可 - 有关详细信息,请参阅 LICENSE 文件。
This server cannot be installed
MCP-RoCQ 与 Coq 证明助手集成,通过 XML 协议通信实现自动依赖类型检查、归纳类型定义和属性证明。
- Currently shows tools but Claude can't use it properly for some reason- invalid syntax generally seems the issue but there could be something else.
- JSON for the Claude App or mcphost config- set your paths according to how you installed coq and the repository.
- This might work- I got it going with uv and most of this could be hallucinatory though: