Idris2 MCP服务器
Idris2的增强型MCP（模型上下文协议）服务器 智能指南访问 从官方文件。
非常适合AI代理生成具有编译时验证的类型安全Idris2代码！
______________________________________________________________________
✨ 特性
🎯 智能代码生成支持
- 7结构化资源 -整理Idris2官方文件
- 上下文搜索 -按关键字查找相关指南(
search_guidelines) - 剖面提取 -无需加载整个文档即可获取重点信息(
get_guideline_section) - 项目特定规则 -在实际使用过程中发现的关键解析器约束
🛠️ 强大的工具
- check_idris2 -类型检查Idris2代码并返回编译器输出
- 解释错误 -简明的语言错误解释和建议
- get_template -为常见模式生成代码模板
- validate_syntax -快速语法验证（检测长参数名！）
- suggest_fix -智能错误修复建议
- 搜索指南 ⭐ - 在所有指南中搜索特定主题
- get_guide_liction ⭐ - 提取重点部分（支持11个主题）
📚 综合文档
- 语法基础 -基本类型、函数、数据类型、记录、I/O
- 类型系统 -依赖类型、乘法（QTT）、证明、接口
- 模块 -模块组织、导出、导入、命名空间
- 高级模式 -视图、定理证明、FFI、元编程
- Pragmas参考 -所有Idris2 pragmas的完整参考
______________________________________________________________________
🚀 快速开始
先决条件
- Python 3.11+
- 伊德里斯2 v0.7.0+ （为
check_idris2仅限工具，其他工具无需工具即可工作） - Node.js 18+ （用于MCP检验员测试，可选）
安装
# Clone the repository
git clone https://github.com/twoLoop-40/idris2-mcp-server.git
cd idris2-mcp-server
# Option 1: Using uv (Recommended - Fast!)
uv venv
source .venv/bin/activate # On Windows: .venv\Scripts\activate
uv pip install -r requirements.txt
# Option 2: Using pip
pip install -r requirements.txt
# Test the server
python test_cli.py使用Claude代码进行配置
添加到您的 .mcp-config.json:
{
"mcpServers": {
"idris2-helper": {
"command": "python",
"args": ["/absolute/path/to/idris2-mcp-server/server.py"],
"description": "Enhanced Idris2 type-checking and intelligent guideline access"
}
}
}备注：使用绝对路径！配置后重新启动Claude Code。
______________________________________________________________________
🧪 测试
方法1:CLI测试套件（最快⚡)
python test_cli.py输出:
✅ All tests completed!
- search_guidelines: 3 queries tested
- get_guideline_section: 3 topics tested
- read_resource: 3 resources tested方法2：交互式CLI（探索🔍)
python test_cli.py --interactive命令:
idris2-mcp> list # Show all topics/resources
idris2-mcp> search multiplicities types # Search guidelines
idris2-mcp> section dependent_types # Get specific section
idris2-mcp> resource idris2://guidelines/types # Read full resource
idris2-mcp> quit方法3:MCP检查员（全协议测试🌐)
./test_mcp_inspector.sh
# Or: npx @modelcontextprotocol/inspector python server.py在以下位置打开web UIhttp://localhost:5173
______________________________________________________________________
📖 使用示例
示例1：搜索依赖类型
工具: search_guidelines
输入:
{
"query": "dependent types",
"category": "types"
}输出：2-3段相关摘录 02-TYPE-SYSTEM.md 根据上下文
______________________________________________________________________
示例2：获取乘法部分
工具: get_guideline_section
输入:
{
"topic": "multiplicities"
}输出：用示例完成“乘法（QTT）”部分（约60行）
______________________________________________________________________
示例3：在类型检查之前验证语法
工具: validate_syntax
输入:
{
"code": "data Expense : Type where\n MkExpense : (govSupport : Nat) -> (cashMatch : Nat) -> (inKindMatch : Nat) -> Expense"
}输出:
⚠️ Potential syntax issues found:
- Line 2: 🚨 CRITICAL - Long parameter names detected: govSupport, cashMatch, inKindMatch
Parser may fail with 3+ params having long names (>8 chars)______________________________________________________________________
示例4：获取修复建议
工具: suggest_fix
输入:
{
"error_message": "Expected 'case', 'if', 'do', application or operator expression",
"code": "data Expense : Type where\n MkExpense : (govSupport : Nat) -> (cashMatch : Nat) -> (inKindMatch : Nat) -> Expense"
}输出:
## Suggested Fixes
1. 🚨 CRITICAL: This is likely caused by LONG PARAMETER NAMES in data constructors!
2. Idris2 parser fails when 3+ parameters with long names (>8 chars) are on one line
3. FIX: Shorten parameter names to 6-8 characters or less
4. Example: Change (govSupport : Nat) -> (gov : Nat)
5. 📖 See: idris2://guidelines/project resource for full details______________________________________________________________________
🚨 关键规则（必须知道！）
1.短参数名称（最重要！）
-- ❌ FAILS: Long names with 3+ params → Parser Error
data Expense : Type where
MkExpense : (govSupport : Nat) -> (cashMatch : Nat) -> (inKindMatch : Nat) -> Expense
-- ✅ WORKS: Short names (≤8 chars)
data Expense : Type where
MkExpense : (gov : Nat) -> (cash : Nat) -> (inKind : Nat) -> Expense为什么：当数据构造函数在一行上有3+个长名称（>8个字符）的参数时，Idris2解析器会失败。
2.使用运算符，而不是函数
-- ❌ FAILS: plus/minus don't exist in Prelude
(pf : total = plus supply vat)
-- ✅ WORKS: Use operators
(pf : total = supply + vat)3.首选单行声明
多行缩进可能会导致解析器错误。更喜欢单行声明。
看: guidelines/IDRIS2_CODE_GENERATION_GUIDELINES.md 详细信息（韩语）
______________________________________________________________________
📚 可用资源
| URI | 描述 | 使用时间 |
|---|---|---|
idris2://guidelines/project | 特定于项目的解析器规则 | 总是先读 生成代码时 |
idris2://guidelines/syntax | 基本语法和构造 | 学习Idris2，基本语法问题 |
idris2://guidelines/types | 类型系统特征 | 处理依赖类型、证明、QTT |
idris2://guidelines/modules | 模块组织 | 组织代码、导入、可见性 |
idris2://guidelines/advanced | 高级模式 | 视图、定理证明、FFI、元编程 |
idris2://guidelines/pragmas | Pragma参考 | 需要编译器指令，优化 |
idris2://guidelines/index | 快速参考 | 概述，找到合适的文档 |
______________________________________________________________________
🎓 支持的主题
这 get_guideline_section 该工具支持11个重点主题：
parser_constraints-关键解析器规则（必须阅读！）multiplicities-QTT和线性类型dependent_types-依赖类型模式interfaces-类型类别modules-模块组织views-观点和with规则proofs-定理证明ffi-外部功能接口pragmas_inline-内联语法百分比pragmas_foreign-外来语法百分比totality-总体检查
______________________________________________________________________
🤖 对于AI代理
推荐工作流程
在生成Idris2代码之前:
- 阅读
idris2://guidelines/project（关键规则） - 搜索类似模式：
search_guidelines("data types") - 根据准则生成代码
提交代码之前:
- 跑
validate_syntax（捕获解析器问题） - 手动检查：参数名称≤8个字符？
- 使用运算符（+，-）而不是函数（加号，减号）？
如果编译失败:
- 使用
suggest_fix（智能建议） - 使用
get_guideline_section针对特定主题 - 搜索错误模式：
search_guidelines("error keyword")
上下文窗口管理
根据需要按需加载指南：
- 语法问题→
idris2://guidelines/syntax - 类型系统→
idris2://guidelines/types - 特定主题→
get_guideline_section("topic") - 关键词搜索→
search_guidelines("keyword")
这可以防止上下文窗口膨胀，同时保持对全面文档的访问。
______________________________________________________________________
🏗️ 项目结构
idris2-mcp-server/
├── server.py # Main MCP server
├── guidelines/ # Official Idris2 documentation
│ ├── README.md # Quick reference and index
│ ├── 01-SYNTAX-BASICS.md # Basic syntax (4KB)
│ ├── 02-TYPE-SYSTEM.md # Type system (6.5KB)
│ ├── 03-MODULES-NAMESPACES.md # Modules (6KB)
│ ├── 04-ADVANCED-PATTERNS.md # Advanced (7KB)
│ └── 05-PRAGMAS-REFERENCE.md # Pragmas (8.5KB)
├── test_cli.py # CLI test tool
├── test_guidelines.py # Unit tests
├── test_mcp_inspector.sh # MCP Inspector launcher
├── README.md # This file
├── LICENSE # MIT License
└── requirements.txt # Python dependencies______________________________________________________________________
🔧 需求
Python依赖关系
mcp>=1.0.0安装：
pip install -r requirements.txt可选依赖
- 伊德里斯2：只需要
check_idris2工具 - Node.js：仅用于MCP检验员测试
所有其他工具都可以在没有这些依赖关系的情况下工作！
______________________________________________________________________
🐛 故障排除
MCP检查器无法启动
# Check Node.js version
node --version # Need v18+
# Clear cache and retry
npx clear-npx-cache
npx @modelcontextprotocol/inspector python server.py导入错误：没有名为“mcp”的模块
# Install MCP package
pip install mcp
# Or with uv (faster)
uv pip install mcp找不到Idris2命令
# Install Idris2 (for check_idris2 tool only)
brew install idris2 # macOS备注：其他工具在没有Idris2的情况下也能工作！
______________________________________________________________________
📊 统计
- 7资源 -有组织的文件
- 7工具 -代码生成和验证
- 11主题 -重点部分提取
- 6指南 -39KB文档
- 100%测试覆盖率 -所有功能均已测试
______________________________________________________________________
🤝 贡献
欢迎投稿！拜托：
- 分叉存储库
- 创建要素分支(
git checkout -b feature/amazing) - 提交您的更改(
git commit -m 'Add amazing feature') - 推到分支(
git push origin feature/amazing) - 打开拉取请求
贡献领域
- \[\]添加更多指南主题
- \[\]改进错误检测模式
- \[\]为频繁访问的指南添加缓存
- \[\]创建视频教程
- \[\]将文档翻译成其他语言
- \[\]添加更多代码模板
______________________________________________________________________
📝 更新日志
v2.0.0（2025-10-27）
新功能:
- ✨ 为官方指南添加了7个结构化资源URI
- ✨ 添加
search_guidelines关键字搜索工具 - ✨ 添加
get_guideline_section聚焦检索工具 - ✨ 增强
validate_syntax具有长参数名称检测功能 - ✨ 整理Idris2官方文件（39KB）
改进:
- 🐛 固定的
suggest_fix推荐相关资源 - 📚 包含使用模式的全面文档
- ✅ 添加了CLI测试套件和交互模式
v1.0.0（2025-10-27）
- 带有基本类型检查和验证的初始版本
- 项目特定指南资源
______________________________________________________________________
📄 许可证
MIT许可证
版权所有（c）2025 Idris2 MCP服务器贡献者
特此免费向任何获得副本的人授予许可 本软件和相关文档文件（“软件”），以处理 在软件中不受限制，包括但不限于权利 使用、复制、修改、合并、发布、分发、再许可和/或销售 软件的副本，并允许软件的接收者 根据以下条件提供：
上述版权声明和本许可声明应包含在所有 软件的副本或实质性部分。
软件按“原样”提供，不提供任何形式的明示或明示担保 隐含的，包括但不限于适销性保证， 适用于特定目的且不造成伤害。在任何情况下 作者或版权持有人对任何索赔、损害赔偿或其他 因以下原因产生的责任，无论是在合同、侵权或其他诉讼中， 出于或与软件、使用或其他交易有关 软件。
______________________________________________________________________
🙏 致谢
- Idris2团队 -对于令人惊叹的依赖型语言
- Anthropic -对于模型上下文协议规范
- 社区 -获取反馈和贡献
______________________________________________________________________
🔗 链接
- Idris2官方文件: https://idris2.readthedocs.io/
- MCP规范: https://modelcontextprotocol.io/
- 问题追踪: https://github.com/twoLoop-40/idris2-mcp-server/issues
- 源代码: https://github.com/twoLoop-40/idris2-mcp-server
______________________________________________________________________
⭐ 明星历史
如果你觉得这个项目有用，请考虑给它一颗星！ ⭐
______________________________________________________________________
由以下材料制成❤️ Idris2社区