twoLoop-40/idris2-mcp-server

Idris2 MCP Server

Enhanced MCP (Model Context Protocol) server for Idris2 with intelligent guideline access from official documentation.

Perfect for AI agents generating type-safe Idris2 code with compile-time verification!

✨ Features

🎯 Smart Code Generation Support

• 7 Structured Resources - Organized official Idris2 documentation
• Contextual Search - Find relevant guidelines by keyword (search_guidelines)
• Section Extraction - Get focused information without loading entire documents (get_guideline_section)
• Project-Specific Rules - Critical parser constraints discovered during real-world usage

🛠️ Powerful Tools

1. check_idris2 - Type-check Idris2 code and return compiler output
2. explain_error - Plain language error explanations with suggestions
3. get_template - Generate code templates for common patterns
4. validate_syntax - Quick syntax validation (detects long parameter names!)
5. suggest_fix - Intelligent error fix suggestions
6. search_guidelines ⭐ - Search across all guidelines for specific topics
7. get_guideline_section ⭐ - Extract focused sections (11 topics supported)

📚 Comprehensive Documentation

• Syntax Basics - Primitive types, functions, data types, records, I/O
• Type System - Dependent types, multiplicities (QTT), proofs, interfaces
• Modules - Module organization, exports, imports, namespaces
• Advanced Patterns - Views, theorem proving, FFI, metaprogramming
• Pragmas Reference - Complete reference for all Idris2 pragmas

🚀 Quick Start

Prerequisites

• Python 3.11+
• Idris2 v0.7.0+ (for check_idris2 tool only, other tools work without it)
• Node.js 18+ (for MCP Inspector testing, optional)

Installation

# 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

Configure with Claude Code

Add to your .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"
    }
  }
}

Note: Use absolute path! Restart Claude Code after configuration.

🧪 Testing

Method 1: CLI Test Suite (Fastest ⚡)

python test_cli.py

Output:

✅ All tests completed!
- search_guidelines: 3 queries tested
- get_guideline_section: 3 topics tested
- read_resource: 3 resources tested

Method 2: Interactive CLI (Exploration 🔍)

python test_cli.py --interactive

Commands:

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

Method 3: MCP Inspector (Full Protocol Testing 🌐)

./test_mcp_inspector.sh
# Or: npx @modelcontextprotocol/inspector python server.py

Opens web UI at http://localhost:5173

📖 Usage Examples

Example 1: Search for Dependent Types

Tool: search_guidelines

Input:

{
  "query": "dependent types",
  "category": "types"
}

Output: 2-3 relevant excerpts from 02-TYPE-SYSTEM.md with context

Example 2: Get Multiplicities Section

Tool: get_guideline_section

Input:

{
  "topic": "multiplicities"
}

Output: Complete "Multiplicities (QTT)" section (~60 lines) with examples

Example 3: Validate Syntax Before Type-Checking

Tool: validate_syntax

Input:

{
  "code": "data Expense : Type where\n  MkExpense : (govSupport : Nat) -> (cashMatch : Nat) -> (inKindMatch : Nat) -> Expense"
}

Output:

⚠️ 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)

Example 4: Get Fix Suggestions

Tool: suggest_fix

Input:

{
  "error_message": "Expected 'case', 'if', 'do', application or operator expression",
  "code": "data Expense : Type where\n  MkExpense : (govSupport : Nat) -> (cashMatch : Nat) -> (inKindMatch : Nat) -> Expense"
}

Output:

## 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

🚨 Critical Rules (Must Know!)

1. Short Parameter Names (MOST IMPORTANT!)

-- ❌ 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

Why: Idris2 parser fails when data constructors have 3+ parameters with long names (>8 characters) on one line.

2. Use Operators, Not Functions

-- ❌ FAILS: plus/minus don't exist in Prelude
(pf : total = plus supply vat)

-- ✅ WORKS: Use operators
(pf : total = supply + vat)

3. One-Line Declarations Preferred

Multi-line indentation can cause parser errors. Prefer one-line declarations.

See: guidelines/IDRIS2_CODE_GENERATION_GUIDELINES.md for full details (Korean)

📚 Available Resources

🎓 Topics Supported

The get_guideline_section tool supports 11 focused topics:

• parser_constraints - Critical parser rules (MUST READ!)
• multiplicities - QTT and linear types
• dependent_types - Dependent type patterns
• interfaces - Type classes
• modules - Module organization
• views - Views and with rule
• proofs - Theorem proving
• ffi - Foreign Function Interface
• pragmas_inline - %inline pragma
• pragmas_foreign - %foreign pragma
• totality - Totality checking

🤖 For AI Agents

Recommended Workflow

Before generating Idris2 code:

1. Read idris2://guidelines/project (critical rules)
2. Search for similar patterns: search_guidelines("data types")
3. Generate code following guidelines

Before submitting code:

1. Run validate_syntax (catches parser issues)
2. Check manually: parameter names ≤ 8 chars?
3. Using operators (+, -) not functions (plus, minus)?

If compilation fails:

1. Use suggest_fix (intelligent suggestions)
2. Use get_guideline_section for specific topics
3. Search for error pattern: search_guidelines("error keyword")

Context Window Management

Load guidelines on-demand based on need:

• Syntax question → idris2://guidelines/syntax
• Type system → idris2://guidelines/types
• Specific topic → get_guideline_section("topic")
• Keyword search → search_guidelines("keyword")

This prevents context window bloat while maintaining access to comprehensive documentation.

🏗️ Project Structure

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

🔧 Requirements

Python Dependencies

mcp>=1.0.0

Install:

pip install -r requirements.txt

Optional Dependencies

• Idris2: Only needed for check_idris2 tool
• Node.js: Only needed for MCP Inspector testing

All other tools work without these dependencies!

🐛 Troubleshooting

MCP Inspector won't start

# Check Node.js version
node --version  # Need v18+

# Clear cache and retry
npx clear-npx-cache
npx @modelcontextprotocol/inspector python server.py

Import error: No module named 'mcp'

# Install MCP package
pip install mcp

# Or with uv (faster)
uv pip install mcp

Idris2 command not found

# Install Idris2 (for check_idris2 tool only)
brew install idris2  # macOS

Note: Other tools work without Idris2!

📊 Statistics

• 7 Resources - Organized documentation
• 7 Tools - Code generation & validation
• 11 Topics - Focused section extraction
• 6 Guidelines - 39KB of documentation
• 100% Test Coverage - All features tested

🤝 Contributing

Contributions welcome! Please:

1. Fork the repository
2. Create a feature branch (git checkout -b feature/amazing)
3. Commit your changes (git commit -m 'Add amazing feature')
4. Push to the branch (git push origin feature/amazing)
5. Open a Pull Request

Areas for Contribution

• Add more guideline topics
• Improve error detection patterns
• Add caching for frequently accessed guidelines
• Create video tutorials
• Translate documentation to other languages
• Add more code templates

📝 Changelog

v2.0.0 (2025-10-27)

New Features:

• ✨ Added 7 structured resource URIs for official guidelines
• ✨ Added search_guidelines tool for keyword search
• ✨ Added get_guideline_section tool for focused retrieval
• ✨ Enhanced validate_syntax with long parameter name detection
• ✨ Organized official Idris2 documentation (39KB)

Improvements:

• 🐛 Fixed suggest_fix to recommend relevant resources
• 📚 Comprehensive documentation with usage patterns
• ✅ Added CLI test suite and interactive mode

v1.0.0 (2025-10-27)

• Initial release with basic type-checking and validation
• Project-specific guideline resource

📄 License

MIT License

Copyright (c) 2025 Idris2 MCP Server Contributors

Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

🙏 Acknowledgments

• Idris2 Team - For the amazing dependently-typed language
• Anthropic - For the Model Context Protocol specification
• Community - For feedback and contributions

🔗 Links

• Idris2 Official Docs: https://idris2.readthedocs.io/
• MCP Specification: https://modelcontextprotocol.io/
• Issue Tracker: https://github.com/twoLoop-40/idris2-mcp-server/issues
• Source Code: https://github.com/twoLoop-40/idris2-mcp-server

⭐ Star History

If you find this project useful, please consider giving it a star! ⭐

Made with ❤️ for the Idris2 community