简介这份资源是面向 Agda 依赖类型语言学习者的 VS Code 编辑器扩展帮助习惯现代编辑器工作流的开发者摆脱 Emacs 环境限制在 VS Code 中完成 Agda 代码的编写、加载与类型检查。扩展支持通过 CtrlC 组合键触发加载、归一化等常用命令并针对 VS Code 键位特点重新映射了 Emacs 中的 Cu、Cu Cu 前缀同时提供仍处于开发阶段的 Agda 语言服务器启用后可在面板右上角看到 LSP 标识。压缩包共 179 个文件约 457KB以 67 个 js 与 64 个 res 源码文件为主体辅以 out、in 测试用例、json 配置、md 文档及少量 agda 示例文件结构紧凑便于二次开发与问题排查。目前已有 237 人学习下载适合希望迁移到 VS Code 的 Agda 用户、扩展开发者以及研究编辑器语言支持实现的技术人员参考。1. 在 VS Code 里写 Agda为什么值得折腾以及谁适合入坑如果你写过一段时间的 Agda大概率经历过这种分裂一边是语言本身那种“证明即程序”的优雅一边是编辑器交互的割裂感。Agda 的核心工作流不是“写完再编译”而是“边写边问编译器”——这个洞的类型是什么这个目标能不能用cong化简把光标放在?上按一下快捷键右侧面板立刻告诉你上下文和目标类型。这套交互如果断了写证明就变成盲人摸象。agda-mode-vscode要解决的就是这件事把原本在 Emacs 里那套成熟的 Agda 交互模式搬到 VS Code 上。它不是一个新语言工具链而是一个编辑器前端适配层——底层还是agda可执行文件加agda --interaction的 JSON 协议上层用 VS Code 的 Language Server 机制把命令、目标、上下文、规范化结果渲染出来。适合谁三类人一是日常主力编辑器已经是 VS Code、不想为 Agda 单独开 Emacs 的开发者二是刚学依赖类型、需要频繁看 goal 和 context 的新手三是想在 CI 或远程开发环境里统一编辑体验的团队。不适合谁如果你的项目重度依赖 Emacs 特有的 Agda 插件生态比如某些自定义 keybind 和agda2-mode-hook迁移成本可能高于收益。2. 环境搭建从零把 agda-mode-vscode 跑起来2.1 先确认 Agda 本体和版本匹配很多人翻车不是翻在 VS Code 插件上而是翻在 Agda 本体没装对。agda-mode-vscode本质是客户端它通过标准输入输出和agda --interaction通信。所以第一步永远是命令行里agda --version能正常输出。常见做法是用包管理器装# 以常见 Haskell 工具链为例用 cabal 安装指定版本 cabal update cabal install Agda-2.6.4 --installdir$HOME/.local/bin # 确认可执行文件在 PATH 里 which agda agda --version逻辑说明cabal install会把agda和agda-mode两个可执行文件放到指定目录。参数--installdir决定安装位置建议放在用户目录下避免权限问题。装完后必须确认which agda返回的路径和 VS Code 继承的 PATH 一致——这是后面“插件找不到 agda”问题的根源。2.2 安装插件并配置 agda 路径在 VS Code 扩展面板搜索agda-mode安装后不要急着打开.agda文件。先做两件事一是确认 VS Code 的集成终端里agda --version能跑通二是如果用了版本管理工具如 ghcup、nix需要在设置里显式指定路径。// settings.json 片段 { agdaMode.connection.agdaPath: /home/user/.local/bin/agda, agdaMode.connection.agdaArgs: [--interaction], agdaMode.languageServer.enabled: true }逻辑说明agdaPath是绝对路径避免依赖 shell 初始化脚本agdaArgs里--interaction是必须的否则插件无法进入交互模式languageServer.enabled打开后才会启用 goal 面板和命令面板。参数改完记得重启 VS Code 窗口不是重载插件——很多配置项在窗口级别缓存。2.3 验证最小工作流一个带洞的证明新建Test.agda写一个最简例子module Test where open import Data.Nat using (ℕ; zero; suc) open import Relation.Binary.PropositionalEquality using (_≡_; refl) -- 目标证明 0 n ≡ n -identityˡ : (n : ℕ) → zero n ≡ n -identityˡ n ?把光标放在?上按C-c C-l加载文件再按C-c C-,显示 goal 和 context。如果右侧面板出现Goal: zero n ≡ n和n : ℕ说明链路通了。这一步是分水岭通了后面都好说不通就要回到 2.1 检查 Agda 本体。3. 核心交互命令与参数调优把证明效率拉满3.1 必须记住的六个命令和它们的触发时机agda-mode-vscode的命令面板里有一长串命令但日常高频的就六个。我一般建议新手先把这六个练到肌肉记忆命令默认快捷键使用时机LoadC-c C-l改完文件后刷新所有 goalGoal type and contextC-c C-,看当前洞的目标和上下文Goal type and normalized contextC-c C-.上下文里有复杂表达式需要化简RefineC-c C-r目标能由构造子直接拆分时Case splitC-c C-c对变量做模式匹配AutoC-c C-a简单目标让 Agda 自己搜参数说明这些快捷键在 VS Code 里可能和系统或输入法冲突。如果按了没反应先去键盘快捷方式里搜agda-mode看绑定是否被覆盖。常见冲突是C-c开头的组合被终端复用解决方法是把 Agda 命令改成C-c C-之外的前缀或者只在.agda文件里启用。3.2 交互协议背后的 JSON 消息长什么样理解底层协议能帮你排查“命令没反应”的问题。agda --interaction模式下客户端和 Agda 之间传的是 JSON 行。比如请求 goal 类型{type:GoalType,params:{interactionPoint:?0,normalise:false}}Agda 返回{type:DisplayInfo,params:{info:{kind:GoalType,goalInfo:{interactionPoint:?0,type:zero n ≡ n,context:[{name:n,type:ℕ}]}}}}逻辑说明interactionPoint是洞的标识?0对应文件里第一个洞normalise控制是否对类型做规范化对应C-c C-.和C-c C-,的区别。如果插件面板空白可以在 VS Code 输出面板选Agda通道看原始 JSON——这是排查黑匣子问题的后悔药。3.3 性能相关参数大文件下怎么不卡Agda 的类型检查是出了名的吃资源。当文件超过几百行、goal 数量多时每次C-c C-l全量加载会明显卡顿。可调参数集中在 Agda 本体侧# 在项目根目录放一个 .agda-lib 或直接命令行传参 agda --interaction \ --no-libraries \ --local-interfaces \ --syntax highlighting逻辑说明--local-interfaces让 Agda 把接口文件放在本地而不是全局缓存适合多项目并行--no-libraries在只验证单文件时跳过库解析能省几秒。注意这些参数要加到agdaArgs里不是插件设置里单独开关。如果还是慢优先检查是不是每次都在重新类型检查整个依赖链——把常用库预编译成.agdai接口文件是标准做法。4. 避坑与排查那些让 agda-mode-vscode 装死的问题4.1 现象插件显示已激活但所有命令无响应原因VS Code 继承的 PATH 和终端里的 PATH 不一致插件找不到agda可执行文件。解决在settings.json里写死agdaMode.connection.agdaPath绝对路径然后重启窗口。验证方法是打开输出面板看Agda通道有没有spawn agda ENOENT之类的报错。4.2 现象goal 面板一直转圈不显示类型原因Agda 进程启动了但交互协议握手失败常见于 Agda 版本和插件期望的协议版本不匹配。解决先确认agda --version输出的版本号然后看插件文档里标注的兼容范围。如果版本差一个大版本要么升级 Agda要么降级插件。不要同时装多个 Agda 版本而不指定路径——这是血泪经验。4.3 现象C-c C-c做 case split 后文件乱码或缩进错乱原因VS Code 的自动缩进和 Agda 返回的文本编辑指令冲突。解决在.agda文件的语言设置里关掉editor.autoIndent改成editor.autoIndent: none让 Agda 自己控制缩进。另外检查文件编码必须是 UTF-8Agda 的ℕ、≡这些字符对编码敏感。4.4 现象改了.agda-lib后插件不认新库原因Agda 的库解析有缓存插件不会主动重读。解决执行一次Agda: Restart命令命令面板搜或者直接重启 VS Code 窗口。如果还不行删掉项目下的_build目录和*.agdai接口文件强制全量重建。4.5 现象远程开发SSH/容器里插件连不上 Agda原因插件默认在本地找agda但远程场景下 Agda 装在远端。解决VS Code 远程开发时插件会跑在远端扩展宿主里所以agdaPath要填远端路径。常见错误是填了本地路径结果远端找不到。验证方法是在远程终端里which agda把输出原样填进设置。5. 进阶技巧把 agda-mode-vscode 用出肌肉记忆5.1 自定义快捷键把高频命令压到单手可及默认的C-c前缀在 VS Code 里其实不太顺手因为C-c常被终端和复制占用。我一般会把最常用的三个命令改到Alt系列// keybindings.json [ { key: altl, command: agda-mode.load, when: editorLangId agda }, { key: alt,, command: agda-mode.goalTypeContext, when: editorLangId agda }, { key: altr, command: agda-mode.refine, when: editorLangId agda } ]逻辑说明when条件限定只在 Agda 文件里生效避免污染其他语言。altl对应 loadalt,对应看 goalaltr对应 refine。改完后建议把默认绑定禁用防止两套快捷键打架。5.2 用任务Task做批量类型检查插件适合交互式开发但提交前想全量检查所有文件时用 VS Code 任务更稳// .vscode/tasks.json { version: 2.0.0, tasks: [ { label: Agda: Check All, type: shell, command: agda, args: [--no-libraries, src/Everything.agda], group: test, problemMatcher: [] } ] }逻辑说明Everything.agda是一个 import 了所有模块的聚合文件Agda 会递归检查整条依赖链。--no-libraries在 CI 里能避免库路径问题。problemMatcher留空是因为 Agda 的错误格式需要自定义匹配规则简单场景直接看终端输出即可。5.3 验证方法怎么确认交互模式真的在工作一个可靠的验证流程打开一个带洞的文件按 load然后看输出面板的Agda通道。正常情况会看到类似Interaction started和Loading module的日志。如果只有Loading没有后续说明卡在类型检查如果连Interaction started都没有说明进程根本没起来。另一个技巧是在洞里写一个明显错误的表达式比如zero n ≡ suc n看 Agda 是否返回类型错误——如果返回了说明双向通信正常。5.4 一个具体技巧用C-c C-.排查隐式参数Agda 的隐式参数经常让人迷惑明明目标看起来一样为什么 refine 不通过这时候C-c C-.normalized context比C-c C-,更有用因为它会把上下文里的表达式规范化。比如上下文里有f (g x)规范化后可能变成h x你就能看出该用哪个引理。我自己的习惯是先C-c C-,看原始类型如果目标里有未化简的表达式再按C-c C-.看规范化版本。这两个命令交替用能省掉大量“为什么类型不匹配”的困惑。最后说一个我踩过的坑不要一边开着agda-mode的自动加载一边手动在终端跑agda检查同一个文件。两个进程会争抢.agdai接口文件的写权限轻则报错重则接口文件损坏然后你要删掉整个_build重来。我的习惯是交互开发时只用插件提交前用任务跑一次全量两者不同时进行。希望帮到你。本文还有配套的精品资源点击获取