AI导哈

Agda MCP服务器

用于Agda的MCP服务器，提供类型检查、跳转到定义、案例拆分、自动证明搜索等功能，适用于开发环境中的代码交互。

  • by DreamLinuxer
  • Python
  • 本地部署
  • 3 星标
  • 更新于
在 GitHub 查看 DreamLinuxer/agda-mcp

使用说明

agda mcp

MCP服务器 阿格达，直接从Claude Code或任何MCP客户端提供类型检查、转到定义、案例拆分、自动证明搜索等。

对话 agda --interaction-json （Emacs/VS Code中支持agda模式的相同界面），因此它可以访问agda的所有交互功能，而无需 agda-language-server.

安装

先决条件

1.克隆和构建

git clone https://github.com/DreamLinuxer/agda-mcp.git
cd agda-mcp
uv sync

2.添加到您的MCP客户端

克劳德代码 （全球范围内，所有项目）：

claude mcp add --scope user agda-lsp -- uv run --directory /path/to/agda-mcp agda-mcp

其他MCP客户端 --添加到客户端的MCP配置中：

{
  "mcpServers": {
    "agda-lsp": {
      "command": "uv",
      "args": ["run", "--directory", "/path/to/agda-mcp", "agda-mcp"],
      "type": "stdio"
    }
  }
}

替换 /path/to/agda-mcp 使用克隆仓库的绝对路径。

工具

文件和导航

工具 说明
agda_load 加载/类型检查文件，获取目标+错误+警告
agda_hover 符号类型+某一位置的定义位置
agda_definition 转到定义（文件：行：col）

目标操纵（修改源）

工具 说明
agda_give 用完整的溶液填补一个洞
agda_elaborate_give 用精心设计的解决方案填补漏洞
agda_refine 细化目标（可能创建新的子目标）
agda_intro 引入构造函数或lambda
agda_refine_or_intro 在精炼和介绍之间自动选择
agda_case_split 目标中变量的案例分割
agda_auto 尝试自动解决一个目标
agda_solve_one 如果由统一决定，则解决目标

目标检查

工具 说明
agda_goal_info 获取目标的类型和背景
agda_goal_type 获得目标类型
agda_context 获取目标的上下文（绑定）
agda_goal_type_context_infer 目标类型+上下文+expr的推断类型
agda_goal_type_context_check 目标类型+上下文+根据类型检查expr
agda_infer_in_goal 推断目标处表达式的类型
agda_compute_in_goal 在目标处规范表达式
agda_helper_function 为目标生成辅助函数类型
agda_why_in_scope_goal 解释一个名字从哪里来（在一个目标上）
agda_module_contents_goal 列出模块内容（目标）

顶级命令

工具 说明
agda_infer 推断表达式的类型
agda_compute 规范化/计算表达式
agda_why_in_scope 解释名字的来源
agda_constraints 显示所有未解决的约束
agda_metas 显示所有开放目标/元变量
agda_search_about 搜索提到给定名称的定义
agda_module_contents 列出模块导出的名称
agda_solve_all 解决统一确定的所有目标
agda_auto_all 尝试自动解决所有目标

使用示例

加载并键入检查文件

agda_load("/path/to/file.agda")
→ Checked. No errors, warnings, or goals.

推断类型

agda_infer("/path/to/file.agda", "map")
→ {a b : Set} {n : ℕ} → (a → b) → Vec a n → Vec b n

计算表达式

agda_compute("/path/to/file.agda", "2 + 3")
→ 5

案件分割

agda_case_split("/path/to/file.agda", 0, "xs")
→ f [] = ?
  f (x ∷ xs) = ?

自动解决目标

agda_auto("/path/to/file.agda", 0)
→ a , b

运作原理

服务器生成一个持久 agda --interaction-json 通过stdio上的IOTCM协议进行处理和通信。文件状态（突出显示跳转定义、目标类型、诊断的数据）按文件缓存，并在每个文件上刷新 agda_load 电话。

相关 MCP