Agda MCP Server

agda mcp服务器

](https://www.npmjs.com/package/agda-mcp-server)   ](package.json)

agda-mcp-server 是有状态的 模型上下文协议 交互式服务器 阿格达 证明发展。

它使一个长期运行的Agda进程保持活力 --interaction-json MCP模式 客户端可以像人类在编辑器中一样使用Agda：加载文件、检查 目标、变量分割、细化漏洞、推断类型、规范表达式， 搜索本地环境，并在不重新启动Agda的情况下迭代证明 每一个请求。

此服务器提供什么

• 持续的交互式Agda会话。
• MCP上的目标意识证明行动。
• 当您只想快速通过验证时，进行无状态批处理类型检查。
• 大型Agda代码库的导航和范围检查助手。
• Literate Agda支持——从所有七种识字格式中提取代码块。
• 每个工具的结构化语义输出，以及人类可读的文本。
• 代理本机会话自检(agda_session_snapshot, agda_goal_catalog, agda_tool_recommend).
• 生成具有稳定指纹的Bug报告和问题更新包。
• 一个用于项目特定或领域特定工具的小型扩展系统。

运作原理

服务器在中启动Agda --interaction-json 通过模式和通信 Agda的IOTCM协议基于标准输入和输出。

在实践中，工作流程是：

1. 加载Agda文件 agda_load.
2. Agda为所有开放目标分配交互点ID。
3. 将这些目标ID与面向证明的工具一起使用，例如 agda_goal_type,

agda_case_split, agda_refine，或 agda_give.

1. 应用源代码编辑后重新加载文件，以便Agda可以刷新其目标。

这种庄重是两者的主要区别 agda_load 以及无国籍者 agda_typecheck 命令。

需求

在使用服务器之前，请确保您已经：

• Node.js >= 24
• Agda安装可作为 agda 在你的 PATH，或
• 回购本地固定运营商 tooling/scripts/run-pinned-agda.sh

如果两者都可用，则首选固定转轮。

安装

来源

npm install
npm run build

这将在中生成可分发服务器 dist/.

本地CLI入口点

构建后，可执行入口点为：

node dist/index.js

已发布的包还公开了 agda-mcp-server 二进制通过 bin 领域 package.json.

使用 --help 或 --version 在不启动的情况下检查已安装的二进制文件 MCP服务器：

agda-mcp-server --version   # prints the server version
agda-mcp-server --help      # prints usage and all environment variables

快速启动

使用项目根在stdio上启动服务器：

AGDA_MCP_ROOT=/path/to/agda/project node dist/index.js

如果 AGDA_MCP_ROOT 如果省略，则使用当前工作目录。

示例

示例：加载文件并检查目标

1. agda_load file="Nat/Properties.agda"
  → reports load status and goal IDs

2. agda_session_status
  → shows the loaded file and active goals

3. agda_goal_type goalId=0
  → returns the local context and expected type for `?0`

示例：细化验证孔

1. agda_goal_type goalId=0
  → inspect the goal before editing

2. agda_refine goalId=0 expr="suc"
  → apply a constructor or function

3. agda_metas
  → inspect any new subgoals created by the refinement

示例：在提交表达式之前检查它

1. agda_elaborate goalId=0 expr="map f xs"
  → see Agda's elaborated form

2. agda_infer goalId=0 expr="map f xs"
  → confirm the inferred type

3. agda_give goalId=0 expr="map f xs"
  → fill the goal once the expression looks correct

示例：CI中的无状态验证或编辑器自动化

agda_typecheck file="MyModule.agda"

当您希望在不创建持久会话的情况下出现错误和警告时，请使用此选项。

语义输出

每个工具都会返回：

• 现有MCP客户端的可读文本（in content[].text).
• 具有稳定包络字段的结构化内容(tool, ok, classification, summary, data, diagnostics, provenance, elapsedMs).

每个工具 data 至少包含渲染文本和特定工具 结构化有效载荷，例如。 solutions / rawSolutions / written 为了 agda_solve_*，已解析 clauses 为了 agda_case_split, goalType 和 context 用于目标查询的数组， success 和 output 对于后端， 显示切换/显示系列的状态快照等。代理 应该更喜欢结构化字段，而不是抓取markdown正文。

核心会话工具(agda_load, agda_load_no_metas, agda_typecheck) 公开完整性字段-- goalCount, invisibleGoalCount, hasHoles, isComplete和a classification 的 ok-complete / ok-with-holes / type-error --源自合并的震源孔+ 协议对信号进行计数，从而明确指出漏洞标记({!!} / ?)里面 abstract 块不能欺骗负载为false ok-complete.

MCP客户端配置

克劳德代码

在Claude Code设置中添加类似的服务器条目：

{
  "mcpServers": {
    "agda": {
      "command": "node",
      "args": ["mcp/agda-mcp-server/dist/index.js"],
      "env": {
        "AGDA_MCP_ROOT": "."
      }
    }
  }
}

其他MCP客户端

任何可以生成stdio服务器的MCP客户端都可以运行此包。使用相同 图案：

• 命令： node
• args：路径 dist/index.js
• 环境：设置 AGDA_MCP_ROOT 到Agda项目根

会话模型

此服务器有意具有状态。

• 一个共享的Agda会话保持活动状态。
• 会话跟踪当前加载的文件。
• 目标ID仅对当前加载的文件和当前Agda状态有意义。
• 如果磁盘上的文件发生更改，请使用以下命令重新加载 agda_load 在继续之前。

如果你只想快速进行编译检查，不需要目标，请使用 agda_typecheck 而不是创建会话。

写回证明行动

证明行动工具(agda_give, agda_refine, agda_refine_exact, agda_intro, agda_auto, agda_case_split, agda_solve_one, agda_solve_all) 默认情况下，将结果持久化到源文件并自动重新加载，因此 会话和磁盘保持同步，无需单独的编辑步骤。通过 writeToFile: false 在任何要求仅会话行为的呼吁中（旧 默认）。

agda_apply_edit(file, oldText, newText, occurrence?) 是兄弟原始 对于非目标编辑——添加导入、重命名符号、修复拼写错误。它 替代品 oldText 和 newText 在指定的文件中并重新加载。 oldText 必须精确匹配一次，除非 occurrence （1-基）。

两条路径共享相同的安全保证：

• 仅限Agda源文件。 agda_apply_edit 拒绝任何外界

.agda / .lagda[.md/.rst/.tex/.org/.typ] allowlist-不能使用 修改 .git/config, package.json、shell脚本或其他 项目根目录中的非Agda文件。

• 路径控制。 所有编辑都会解析目标路径

realpath 并验证它是否位于项目根内；一个符号链接 根之外的物理点被拒绝。

• Symlink种族防御。 源代码读取使用 O_NOFOLLOW；如果符号链接是

在路径解析后种植在规范路径上，读取失败 ELOOP 而不是默默地跟随它。

• 文件大小上限。 编辑管道拒绝读取或写入任何Agda

源文件大于 512千磅 （524288字节）。这保护了存储器， 扫描仪成本和爆炸半径——这是一个深思熟虑的软帽，而不是 协议限制。如果你有一个合法的Agda源文件会出错 这意味着文件应该被拆分，而不是 bug来解决。

• 原子写。 编辑会经过临时文件重命名，因此读者永远不会

观察部分书写的状态。临时文件名混合了pid和 randomUUID() 并且是通过以下方式创建的 O_EXCL 所以它不能预先种植 通过并发过程。

• 稳定性保护。 如果加载的文件自

最后的 agda_load，编辑被拒绝，会话被重新加载 为了匹配磁盘，写入永远不会破坏外部更改。

工具参考

协议覆盖范围

该存储库现在通过Agda的交互式数据库跟踪完整的命令库存奇偶性 中列出的IOTCM命令构造函数 Agda.Interaction.Base （验证日期：2026年3月24日）。

• 当前协议清单位于 src/protocol/command-registry.ts.
• 协议奇偶校验矩阵存在于 src/protocol/parity-matrix.ts.
• 库存和奇偶校验测试强制执行每个跟踪的上游命令

奇偶校验行，但语义奇偶校验与单纯的命令是分开跟踪的 地图。

• 架构仍然保持了传输、协议之间的干净分离

包括解码和MCP表示层。

使用 agda_protocol_parity 包括已知的间隙。

在当前的里程碑中，服务器现在公开了：

• agda_goal_type_context_infer 用于目标、上下文和推断类型查询
• agda_goal_type_context_check 用于目标、上下文和检查术语查询
• agda_goal 仅用于显示精确目标
• agda_context 仅用于精确上下文显示
• agda_refine_exact 为了准确 Cmd_refine
• agda_intro 为了准确 Cmd_intro
• agda_solve_one 为了准确 Cmd_solveOne
• agda_load_no_metas 用于没有未解决目标的严格加载
• agda_abort 和 agda_exit 用于过程控制
• agda_show_version 对于正在运行的Agda进程版本
• agda_load_highlighting_info, agda_token_highlighting，以及 agda_highlight 用于突出显示控件
• agda_show_implicit_args / agda_toggle_implicit_args 和 agda_show_irrelevant_args / agda_toggle_irrelevant_args 用于显示切换
• agda_compile, agda_backend_top，以及 agda_backend_hole 用于后端交互命令
• agda_tools_catalog 用于清单派生工具和模式自省
• agda_session_snapshot 对于一个呼叫代理会话，进行自省并建议采取行动
• agda_goal_catalog 对于一次通话，对所有目标进行全面的状态检查
• agda_tool_recommend 基于证明状态的优先级排序的下一个工具建议
• agda_bug_report_bundle 和 agda_bug_report_update_bundle 用于结构化的虫子摄入

会话管理

显示和突出显示

后端命令

报告和代理自省

目标检查和证明交互

这些工具需要先通过加载文件 agda_load.

航行和环境检查

典型的交互式工作流程

1. agda_load file="MyModule.agda"
     → Status: OK, 3 unsolved goals (?0, ?1, ?2)

2. agda_goal_type goalId=0
     → Context: (x : Nat), (p : x ≡ zero)
     → Goal: x + zero ≡ x

3. agda_auto goalId=0
     → No automatic solution found.

4. agda_elaborate goalId=0 expr="+-identityʳ x"
     → Elaborated: +-identityʳ x : x + zero ≡ x

5. agda_give goalId=0 expr="+-identityʳ x"
     → Goal solved.

6. Apply edits to the source file if needed.

7. agda_load file="MyModule.agda"
     → Reload to refresh remaining goals.

无状态操作与有状态操作

使用 agda_typecheck 当你想要：

• 关于文件是否检查的快速是或否答案，
• 仅输出错误和警告，
• 没有交互式目标信息，
• 没有持续的Agda会议。

使用 agda_load 当你想要：

• 稳定的目标ID，
• 针对孔洞的交互式命令，
• 证明搜索、精炼、细化和本地类型信息，
• 持久的Agda子流程。

环境变量

扩展模块

核心服务器是有意通用的，支持外部扩展模块。

有关完整的设置说明和多个扩展示例，请参阅：

• docs/extensions.md
• 示例/扩展/README.md

发展

脚本

当地开发流程

npm install
npm run build
npm test
npm run verify

测试

测试套件目前侧重于轻量级、确定性的行为，例如：

• 响应解析，
• Agda命令字符串转义，
• Agda二元发现，
• 会话清理行为。

这些测试有意避免依赖于实时的Agda安装，以便他们可以 在正常的CI环境中可靠运行。

集成支架也可用于Agda所在的环境 安装：

RUN_AGDA_INTEGRATION=1 npm run test:integration

后端集成命令可以通过以下方式执行：

RUN_AGDA_BACKEND_INTEGRATION=1 AGDA_BACKEND_EXPR=GHC npm run test:integration

AGDA_BACKEND_EXPR 接受后端构造函数表达式，例如 GHC, GHCNoMain, LaTeX, QuickLaTeX，或 OtherBackend "Name".

出版

该包已配置为公共npm发布。

出版前：

1. 更新中的版本 package.json.
2. 跑 npm run verify.
3. 使用正常的发布流程使用npm发布。

这 prepublishOnly 脚本在发布之前自动运行验证。

仅发布以下文件：

• dist/
• README.md
• LICENSE

持续集成

此存储库包括GitHub Actions工作流，位于 即：

• 安装依赖项 npm ci,
• 在推送和拉取请求上运行，
• 在Node.js 24上验证该包。

社区和维护文件

该存储库还包括：

• 贡献.md 用于贡献者设置和工作流程指导
• 安全.md 漏洞报告指南
• 更改日志.md 发布历史记录
• 并为结构化报告发布表格
• 用于一致的拉取请求
• .nvmrc 和那个 packageManager 领域 用于本地工具链对齐

体系结构概述

src/
  index.ts
    Bootstraps the MCP server, registers core tools, and loads extensions.

  agda-process.ts
    Public barrel for the Agda integration layer.

  agda/
    session.ts
      Owns the Agda subprocess, transport, buffering, and session state.
    batch.ts
      Stateless batch type-checking.
    goal-operations.ts
      Goal-centric interactive commands.
    expression-operations.ts
      Expression normalization and type inference.
    advanced-queries.ts
      Constraints, scope, elaboration, module inspection, and search.
    display-operations.ts
      Highlighting and display-toggle command delegates.
    backend-operations.ts
      Compile and backend payload command delegates.
    backend-expression.ts
      Backend expression validation and normalization.
    response-parsing.ts
      Helpers for extracting user-facing messages from Agda responses.
    types.ts
      Shared types for the Agda integration layer.

  protocol/
    command-registry.ts
      Upstream command inventory and parity metadata.
    responses/
      goal-display.ts
      proof-actions.ts
      process-controls.ts
      backend.ts
        Focused response decoders per command family.

  tools/
    session.ts
      MCP tool registration for loading and status operations.
    proof.ts
      MCP tool registration for goal-oriented proof actions.
    navigation.ts
      MCP tool registration for source and environment navigation.
    display.ts
      MCP tool registration for highlighting and display toggles.
    backend.ts
      MCP tool registration for compile and backend payload commands.

  session/
    session-state.ts
      High-level session phase derivation used to keep process lifecycle concerns explicit.

协议说明

服务器使用 IOTCM协议 结束 --interaction-json 模式。

在高层次上：

• 命令作为IOTCM字符串写入stdin上的Agda，
• Agda在stdout上发出换行符分隔的JSON响应，
• 捕获stderr输出用于诊断，
• 会话完成是从状态和运行信息消息推断出来的。

故障排除

agda 找不到

请确保：

• agda 已安装在您的 PATH，或
• tooling/scripts/run-pinned-agda.sh 存在于repo根目录中。

目标ID停止工作

目标ID与当前加载的文件和当前Agda状态相关联。如果 源代码已更改或您应用了案例拆分，请使用以下命令重新加载文件 agda_load.

顶级命令失败，显示“未加载文件”

大多数交互式命令都需要一个活动加载的文件，因为它们需要 Agda会议背景。从...开始 agda_load.

证明搜索或细化返回意外输出

Agda响应格式因命令而异。有疑问时，检查目标 再次与 agda_goal_type 并用更简单的表达式重试。

许可证

该项目根据MIT许可证获得许可。外部扩展模块可能 使用不同的许可证。