Idris2 MCP Server

Idris2 MCP服务器

  

Idris2的增强型MCP（模型上下文协议）服务器 智能指南访问 从官方文件。

非常适合AI代理生成具有编译时验证的类型安全Idris2代码！

______________________________________________________________________

✨ 特性

🎯 智能代码生成支持

• 7结构化资源 -整理Idris2官方文件
• 上下文搜索 -按关键字查找相关指南(search_guidelines)
• 剖面提取 -无需加载整个文档即可获取重点信息(get_guideline_section)
• 项目特定规则 -在实际使用过程中发现的关键解析器约束

🛠️ 强大的工具

1. check_idris2 -类型检查Idris2代码并返回编译器输出
2. 解释错误 -简明的语言错误解释和建议
3. get_template -为常见模式生成代码模板
4. validate_syntax -快速语法验证（检测长参数名！）
5. suggest_fix -智能错误修复建议
6. 搜索指南 ⭐ - 在所有指南中搜索特定主题
7. 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 详细信息（韩语）

______________________________________________________________________

📚 可用资源

______________________________________________________________________

🎓 支持的主题

这 get_guideline_section 该工具支持11个重点主题：

• parser_constraints -关键解析器规则（必须阅读！）
• multiplicities -QTT和线性类型
• dependent_types -依赖类型模式
• interfaces -类型类别
• modules -模块组织
• views -观点和 with 规则
• proofs -定理证明
• ffi -外部功能接口
• pragmas_inline -内联语法百分比
• pragmas_foreign -外来语法百分比
• totality -总体检查

______________________________________________________________________

🤖 对于AI代理

推荐工作流程

在生成Idris2代码之前:

1. 阅读 idris2://guidelines/project （关键规则）
2. 搜索类似模式： search_guidelines("data types")
3. 根据准则生成代码

提交代码之前:

1. 跑 validate_syntax （捕获解析器问题）
2. 手动检查：参数名称≤8个字符？
3. 使用运算符（+，-）而不是函数（加号，减号）？

如果编译失败:

1. 使用 suggest_fix （智能建议）
2. 使用 get_guideline_section 针对特定主题
3. 搜索错误模式： 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%测试覆盖率 -所有功能均已测试

______________________________________________________________________

🤝 贡献

欢迎投稿！拜托：

1. 分叉存储库
2. 创建要素分支(git checkout -b feature/amazing)
3. 提交您的更改(git commit -m 'Add amazing feature')
4. 推到分支(git push origin feature/amazing)
5. 打开拉取请求

贡献领域

• \[\]添加更多指南主题
• \[\]改进错误检测模式
• \[\]为频繁访问的指南添加缓存
• \[\]创建视频教程
• \[\]将文档翻译成其他语言
• \[\]添加更多代码模板

______________________________________________________________________

📝 更新日志

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社区