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

check_idris2 - Type-check Idris2 code and return compiler output
explain_error - Plain language error explanations with suggestions
get_template - Generate code templates for common patterns
validate_syntax - Quick syntax validation (detects long parameter names!)
suggest_fix - Intelligent error fix suggestions
search_guidelines ⭐ - Search across all guidelines for specific topics
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

URI	Description	Use When
`idris2://guidelines/project`	Project-specific parser rules	Always read first when generating code
`idris2://guidelines/syntax`	Basic syntax and constructs	Learning Idris2, basic syntax questions
`idris2://guidelines/types`	Type system features	Working with dependent types, proofs, QTT
`idris2://guidelines/modules`	Module organization	Organizing code, imports, visibility
`idris2://guidelines/advanced`	Advanced patterns	Views, theorem proving, FFI, metaprogramming
`idris2://guidelines/pragmas`	Pragma reference	Need compiler directives, optimization
`idris2://guidelines/index`	Quick reference	Overview, finding right document

🎓 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:

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

Before submitting code:

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

If compilation fails:

Use suggest_fix (intelligent suggestions)
Use get_guideline_section for specific topics
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:

Fork the repository
Create a feature branch (git checkout -b feature/amazing)
Commit your changes (git commit -m 'Add amazing feature')
Push to the branch (git push origin feature/amazing)
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

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

Name		Name	Last commit message	Last commit date
Latest commit History 4 Commits
guidelines		guidelines
.gitignore		.gitignore
CLAUDE.md		CLAUDE.md
CONTRIBUTING.md		CONTRIBUTING.md
LICENSE		LICENSE
README.md		README.md
requirements.txt		requirements.txt
server.py		server.py
test_cli.py		test_cli.py
test_guidelines.py		test_guidelines.py
test_mcp_inspector.sh		test_mcp_inspector.sh

Folders and files

Latest commit

History

Repository files navigation

Idris2 MCP Server

✨ Features

🎯 Smart Code Generation Support

🛠️ Powerful Tools

📚 Comprehensive Documentation

🚀 Quick Start

Prerequisites

Installation

Configure with Claude Code

🧪 Testing

Method 1: CLI Test Suite (Fastest ⚡)

Method 2: Interactive CLI (Exploration 🔍)

Method 3: MCP Inspector (Full Protocol Testing 🌐)

📖 Usage Examples

Example 1: Search for Dependent Types

Example 2: Get Multiplicities Section

Example 3: Validate Syntax Before Type-Checking

Example 4: Get Fix Suggestions

🚨 Critical Rules (Must Know!)

1. Short Parameter Names (MOST IMPORTANT!)

2. Use Operators, Not Functions

3. One-Line Declarations Preferred

📚 Available Resources

🎓 Topics Supported

🤖 For AI Agents

Recommended Workflow

Context Window Management

🏗️ Project Structure

🔧 Requirements

Python Dependencies

Optional Dependencies

🐛 Troubleshooting

MCP Inspector won't start

Import error: No module named 'mcp'

Idris2 command not found

📊 Statistics

🤝 Contributing

Areas for Contribution

📝 Changelog

v2.0.0 (2025-10-27)

v1.0.0 (2025-10-27)

📄 License

🙏 Acknowledgments

🔗 Links

⭐ Star History

About

Resources

License

Contributing

Uh oh!

Stars

Watchers

Forks

Releases

Packages 0

Uh oh!

Contributors

Uh oh!

Languages

Packages