使用说明

Agda MCP服务器

A. 模型上下文协议（MCP）提供交互式Agda开发功能的服务器。这使得人工智能辅助的证明开发、交互式定理证明以及通过标准化协议探索Agda代码成为可能。

特性

持久REPL会话：维护跨命令的Agda交互状态，保留目标、上下文和类型检查结果
24个交互式命令：全面覆盖Agda交互操作，包括证据搜索、案例分割和模块探索
自动文件持久化：修改代码的命令（give、refinement、case split、auto）会自动将更改持久化到磁盘
HTTP传输：符合标准的MCP服务器，具有HTTP/JSON-RPC传输
类型安全集成：使用Haskell的类型系统构建，用于健壮的MCP协议处理
智能响应格式：默认情况下，简洁的人类可读输出（约90%的大小减少），具有可选的完整JSON模式

建筑学

服务器在后台线程中运行一个持久的Agda REPL，通过通道进行通信：

命令通过 Chan CommandWithResponse
响应通过路由返回 MVar Response
每个MCP工具调用都转换为 IOTCM 命令并在持久REPL中执行
目标、上下文和交互状态在命令之间持续存在

文件编辑持久性

当命令修改Agda代码时，更改会自动持久化到磁盘：

响应捕获：键入的REPL回调拦截 Response 值（例如。， Resp_GiveAction, Resp_MakeCase)
一元的：编辑操作在TCM monad上下文中使用Agda的原生API
特定类型的策略：针对不同操作的不同编辑类型：
- ReplaceHole：就地补孔（给予、精炼、自动）
- ReplaceLine：带线条插入的结构编辑（案例分割）
- BatchEdits：以相反的位置顺序应用多个操作（auto_all）
位置感知：编辑保留文件结构并正确处理位置无效

这种架构确保了像“加载文件”这样的操作→ “获得目标”→ “give solution”不仅更新REPL状态，还将更改持久化到源文件。

先决条件

尼克斯启用薄片
阿格达（由Nix环境自动提供）
Claude 代码或另一个MCP客户端

安装

克隆存储库：

git clone https://github.com/faezs/agda-mcp.git
cd agda-mcp

进入Nix开发shell：

nix develop

构建服务器：

cabal build

运行服务器：

cabal run agda-mcp

服务器启动于 http://localhost:3000/mcp 默认情况下。

配置

Claude 代码

添加到您的Claude Code MCP配置文件中(~/.config/claude-code/mcp.json):

{
  "mcpServers": {
    "agda-mcp": {
      "transport": "http",
      "url": "http://localhost:3000/mcp",
      "command": "cabal",
      "args": ["run", "agda-mcp"],
      "cwd": "/path/to/agda-mcp"
    }
  }
}

其他MCP客户端

服务器使用HTTP传输实现MCP协议版本2025-06-18。将您的客户端配置为：

连接到： http://localhost:3000/mcp
通过HTTP POST使用JSON-RPC 2.0
包括 Content-Type: application/json 头球
可选包括 MCP-Protocol-Version: 2025-06-18 头球

可用工具

所有工具都遵循MCP命名约定（snake_case）。参数以JSON对象的形式提供。

1. `agda_load`

加载并键入Agda文件。

论据：

file （string）：Agda文件的绝对或相对路径

例子：

{
  "name": "agda_load",
  "arguments": {
    "file": "/path/to/Example.agda"
  }
}

用例： 必须在任何其他操作之前先调用。使用指定的文件初始化Agda交互会话。

2. `agda_get_goals`

列出当前加载文件中的所有目标/漏洞。

论据： 无

例子：

{
  "name": "agda_get_goals",
  "arguments": {}
}

退货： 目标列表及其ID、类型和文件中的位置。

用例： 加载文件后，使用此功能查看需要验证或填写的内容。

3. `agda_get_goal_type`

获得特定目标所期望的类型。

论据：

goalId （整数）：目标的数字ID（从0开始）

例子：

{
  "name": "agda_get_goal_type",
  "arguments": {
    "goalId": 0
  }
}

退货： 应该填充此目标的预期类型。

用例： 了解完成证明需要什么类型的表达式。

4. `agda_get_context`

获取特定目标的上下文（可用变量及其类型）。

论据：

goalId （integer）：目标的数字ID

例子：

{
  "name": "agda_get_context",
  "arguments": {
    "goalId": 0
  }
}

退货： 此目标范围内的变量及其类型列表。

用例： 看看在证明中可以使用哪些变量和假设。

5. `agda_give`

用完整的表情填补一个目标/洞。

论据：

goalId （integer）：要填充的目标的数字ID
expression （string）：要使用的Agda表达式（例如，“zero”、“suc n”、“refl”）
format （字符串，可选）：“简明”（默认）或“完整”

例子：

{
  "name": "agda_give",
  "arguments": {
    "goalId": 0,
    "expression": "refl"
  }
}

效果：

在REPL中填写目标
自动更新文件：替换 {! !} 与表达式
将成功/失败返回给LLM

用例： 当你有完整的解决方案时，完成一个目标。文件会自动编辑。

6. `agda_refine`

使用构造函数或函数细化目标，引入新的子目标。

论据：

goalId （整数）：要细化的目标的数字ID
expression （string）：构造函数或函数名（例如，“suc”、“zero”、“+")
format （字符串，可选）：“简明”（默认）或“完整”

例子：

{
  "name": "agda_refine",
  "arguments": {
    "goalId": 0,
    "expression": "suc"
  }
}

效果：

将构造函数/函数应用于目标
自动更新文件：替换 {! !} 使用应用的构造函数和新孔
返回新的目标结构

用例： 通过应用构造函数，为构造函数的参数创建新的子目标，从而在目标上取得进展。该文件会自动根据细化进行编辑。

7. `agda_case_split`

通过变量的模式匹配来分割目标。

论据：

goalId （integer）：目标的数字ID
variable （string）：要进行模式匹配的变量的名称
format （字符串，可选）：“简明”（默认）或“完整”

例子：

{
  "name": "agda_case_split",
  "arguments": {
    "goalId": 0,
    "variable": "n"
  }
}

效果：

为所有构造函数生成模式匹配子句
自动更新文件：删除带孔的线，插入多个子句
保留压痕
备注：案例拆分后应重新加载文件以查看新目标

用例： 对变量进行案例分析（例如，将自然数拆分为零和后继案例）。整行被多个模式匹配子句替换。

8. `agda_compute`

在目标的上下文中规范和显示表达式。

论据：

goalId （整数）：目标的数字ID（用于上下文）
expression （string）：要规范化的表达式

例子：

{
  "name": "agda_compute",
  "arguments": {
    "goalId": 0,
    "expression": "2 + 2"
  }
}

退货： 表达式的标准化形式。

用例： 计算表达式以查看其简化形式。

9. `agda_infer_type`

推断目标上下文中表达式的类型。

论据：

goalId （整数）：目标的数字ID（用于上下文）
expression （string）：用于类型检查的表达式

例子：

{
  "name": "agda_infer_type",
  "arguments": {
    "goalId": 0,
    "expression": "suc zero"
  }
}

退货： 表达式的推断类型。

用例： 在使用表达式之前，请先检查它的类型。

10. `agda_intro`

使用介绍策略引入变量。

论据：

goalId （integer）：目标的数字ID

例子：

{
  "name": "agda_intro",
  "arguments": {
    "goalId": 0
  }
}

用例： 自动引入lambda绑定变量或Agda建议的模式变量。

11. `agda_why_in_scope`

查找文档和范围信息以获取名称。

论据：

name （string）：要查找的名称

例子：

{
  "name": "agda_why_in_scope",
  "arguments": {
    "name": "suc"
  }
}

退货： 有关名称定义位置及其在范围内的原因的信息。

用例： 了解函数、类型或构造函数的起源和定义。

可用资源

资源将Agda信息作为可读数据源公开。它们使用基于URI的路由。

1. `Goals`

URI模式： resource://goals/{file}

列出指定Agda文件中的所有目标。

2. `GoalInfo`

URI模式： resource://goal_info/{file}/{id}

关于特定目标的详细信息，包括其类型、背景和位置。

3. `FileContext`

URI模式： resource://file_context/{file}

Agda文件的总体上下文和范围信息。

工作流示例

# 1. Start the server
cabal run agda-mcp

# 2. In Claude Code, load an Agda file
/mcp agda-mcp agda_load file="/path/to/Example.agda"

# 3. Get all goals in the file
/mcp agda-mcp agda_get_goals
# Output: 5 goals: ?0:Nat(10:12) ?1:Nat(11:12) ?2:Nat(15:12) ?3:Nat(16:12) ?4:A(20:18)

# 4. Check the type of goal 0
/mcp agda-mcp agda_get_goal_type goalId=0
# Output: ?0 : Nat

# 5. See available variables
/mcp agda-mcp agda_get_context goalId=0
# Output: Context:
#   n : Nat

# 6. Fill the goal - FILE IS AUTOMATICALLY EDITED
/mcp agda-mcp agda_give goalId=0 expression="n"
# ✓ Filled ?0 with 'n'
# File now shows: zero + n = n

# 7. Case split on a variable - FILE IS AUTOMATICALLY EDITED
/mcp agda-mcp agda_case_split goalId=1 variable="m"
# Split ?1 into 2 clauses:
#   suc zero + n = {! !}
#   suc (suc m) + n = {! !}
# File now has 2 lines instead of 1

# 8. Reload to see new goals after case split
/mcp agda-mcp agda_load file="/path/to/Example.agda"
/mcp agda-mcp agda_get_goals
# Now shows updated goal structure

文件持久化

当您使用以下命令时 agda_give, agda_refine，或 agda_case_split:

✅ 该命令在REPL中执行
✅ 在JSON编码之前捕获响应
✅ 文件编辑被自动提取和应用
✅ JSON响应返回给LLM
✅ 更改会立即持久化到磁盘

无需手动编辑文件！ MCP服务器处理所有源代码修改。

发展

项目结构

agda-mcp/
├── src/
│   ├── AgdaMCP/
│   │   ├── Types.hs        # MCP tool and resource definitions
│   │   ├── Server.hs       # MCP handlers, REPL integration, file edit extraction
│   │   ├── FileEdit.hs     # File editing strategies (ReplaceHole, ReplaceLine, BatchEdits)
│   │   ├── Format.hs       # Response formatting (Concise/Full modes)
│   │   └── Repl.hs         # Persistent REPL adapter
│   └── Main.hs             # Entry point
├── patches/
│   └── mcp-server-header-optional.patch  # Compatibility patch
├── test/
│   ├── Example.agda        # Sample Agda file for testing
│   ├── SearchTest.agda     # Integration test with 1Lab library
│   └── PostulateTest.agda  # Postulate detection tests
├── agda-mcp.cabal          # Cabal package definition
├── flake.nix               # Nix flake for reproducible builds
└── README.md               # This file

从源头构建

# Enter development environment
nix develop

# Build
cabal build

# Run tests (TODO)
cabal test

# Install locally
cabal install

以开发模式运行

# Rebuild and run
cabal run agda-mcp

# With verbose output (TODO: add verbose flag)
cabal run agda-mcp -- --verbose

故障排除

服务器无法启动

问题： 端口3000已在使用中

bind: address already in use (Address already in use)

解决方案： 终止现有进程或更改端口（目前硬编码为3000）。

克劳德代码拒绝连接

问题： Failed to reconnect to agda-mcp

可能的原因：

服务器未运行：从开始 cabal run agda-mcp
配置错误：验证MCP配置文件
网络问题：检查localhost:3000是否可访问

目标不坚持

问题： 加载文件后目标消失

解决方案： 持久REPL架构不应该发生这种情况。如果是这样：

检查服务器日志是否有错误
验证文件是否已成功加载 agda_load
检查REPL线程是否正在运行（在日志中查找“正在启动持久Agda REPL线程…”）

类型检查错误

问题： Agda报告类型错误或缺少模块

解决方案：

确保安装了所有依赖项
检查您的Agda库路径是否配置正确
首先加载文件 agda_load 在其他操作之前

mcp服务器补丁

此项目包括一个补丁 mcp-server Haskell库（版本0.1.0.15），以提高与不发送 MCP-Protocol-Version HTTP标头。

补丁的作用：

使 MCP-Protocol-Version: 2025-06-18 HTTP标头可选
在 initialize 握手
当标头丢失时记录警告，但继续处理

为什么需要： Claude Code的HTTP传输（自2.0.13版本起）将协议版本发送到 initialize JSON-RPC消息，但不是HTTP标头。mcp服务器0.1.0.15严格要求mcp规范2025-06-18的标头，导致连接失败。

补丁位置： patches/mcp-server-header-optional.patch

此补丁在Nix构建过程中通过以下方式自动应用 pkgs.applyPatches 在 flake.nix.

技术细节

文件编辑实现

文件持久性功能是通过结构感知实现的：

三种编辑类型：

更换孔 （给予、精炼、自动）：就地替换 {! expr !} 带有新文本
- 根据具体情况删除或保留牙套 GiveResult 类型
- 保留周围的代码结构
替换线 （案例拆分）：结构线替换
- 删除包含目标的行
- 插入N个保留缩进的新子句
- 处理函数和扩展lambda情况
批次编辑 （SolveAll）：多个孔填充
- 在中应用编辑 反向位置顺序 （从下到上）
- 防止早期编辑导致职位失效
- 从混凝土中提取的每种溶液 Expr

位置安全：

使用Agda的 Range 精确位置类型（1-索引线/列）
杠杆作用 getInteractionRange :: InteractionId -> TCM Range
按位置对批量编辑进行排序，以避免坐标偏移

TCM上下文提取：

使用打字 Response JSON编码前的值
无需JSON解析-使用本机Agda类型
与Agda交互在相同的TCM单子中运行

贡献

欢迎投稿！需要改进的地方：

[x] ~~添加全面的测试套件~~（✓已实施15+个测试）
[x] ~~持续的文件编辑~~（✓以结构意识实现）
[x] ~~响应格式~~（✓简洁/完整模式，尺寸缩小90%）
[]除了HTTP之外，还支持stdio传输
[]可配置的端口和主机
[]goal_info查询的资源URI路径解析
[]带有--Verbose标志的详细/调试日志记录模式
[]CI/CD管道
[]扩展的lambda案例拆分支持

许可证

BSD-3条款（与Agda相同）

致谢

内置于 mcp服务器 Haskell库
由...驱动阿格达
受...启发 agda模式对于VSCode

注：这是一个实验项目。MCP协议和Claude Code的实现正在不断发展，此服务器可能需要更新以与未来版本兼容。

使用说明

Agda MCP服务器

特性

建筑学

文件编辑持久性

先决条件

安装

配置

Claude 代码

其他MCP客户端

可用工具

1. agda_load

2. agda_get_goals

3. agda_get_goal_type

4. agda_get_context

5. agda_give

6. agda_refine

7. agda_case_split

8. agda_compute

9. agda_infer_type

10. agda_intro

11. agda_why_in_scope

可用资源

1. Goals

2. GoalInfo

3. FileContext

工作流示例

文件持久化

发展

项目结构

从源头构建

以开发模式运行

故障排除

服务器无法启动

克劳德代码拒绝连接

目标不坚持

类型检查错误

mcp服务器补丁

技术细节

文件编辑实现

贡献

许可证

致谢

相关 MCP

逻辑推理服务器

Z3定理求解器服务

AI辅助测试自动化工具

一阶逻辑推理服务器

MCP开发工具包

Lean验证MCP服务

1. `agda_load`

2. `agda_get_goals`

3. `agda_get_goal_type`

4. `agda_get_context`

5. `agda_give`

6. `agda_refine`

7. `agda_case_split`

8. `agda_compute`

9. `agda_infer_type`

10. `agda_intro`

11. `agda_why_in_scope`

1. `Goals`

2. `GoalInfo`

3. `FileContext`