简介面向 Agda 开发者的 VS Code 扩展旨在将 Agda 的交互式编辑、文件加载与类型归一化能力带入该编辑器。资源共 179 个文件包含 67 个 JS 与 64 个 RES 源码、13 组 in/out 测试数据、4 个 Agda 示例文件以及 JSON、Markdown、CSS 等配置和说明文档压缩包仅 457KB。目前已有 237 人学习下载。包内提供扩展核心实现附带命令按键映射、LSP 接入示例和输入法说明并收录子句切分、引号文法、特定 issue 复现等典型场景读者可对照源码、测试用例与示例配置快速掌握扩展结构并在 VS Code 中复现加载、类型询问等操作。适合从 Emacs 迁移至 VS Code 的 Agda 用户也为二次开发提供完整参考。1. agda-mode 到底是什么依赖类型语言的编辑体验问题如果你只是想在 VS Code 里把.agda文件的高亮和缩进搞定那 agda-mode 对你来说是杀鸡用牛刀。这个标题指向的是一整套交互式开发模式你能在编辑器里「问」类型、拆 case、自动补全证明项甚至让 Agda 告诉你接下来该想什么。它的作用是解决一个很实际的痛点——依赖类型语言不可能靠「写完再编译」的循环来开发因为错误信息长得像天书你得让编辑器时刻盯着类型上下文边写边验证。适合两种人一是在学依赖类型、被 Emacs 配置劝退的初学者二是在做形式化、验证、证明相关工作的研究者。它把原来只能在 Emacs 里体验的 agda-mode 工作流几乎原样搬进了 VS Code 的界面里至少表面流程是一致的。2. 装到能用agda-mode 的安装链路与最小验证很多人装这个扩展第一次失败不是因为 VS Code 这边出了问题而是 Agda 工具链本身没有装对。agda-mode-vscode 本身只是一个壳子它负责和 VS Code 交互、显示高亮和信息面板真正干活的是命令行里的agda可执行文件。所以安装顺序有个讲究先装 Agda 本体再装扩展最后才去点命令面板。2.1 先搞定 Agda 工具链版本与安装方式Agda 官方推荐的安装方式是通过 Haskell 的包管理器cabal或发行版包管理器。我在这边一般推荐直接装预编译包省掉一两个小时编译期。装完之后最重要的验证不是版本号而是agda命令能不能被 VS Code 的集成终端直接找到。# 验证 agda 可执行文件位置 which agda # 在 Linux/macOS 上通常输出 /usr/local/bin/agda 或者 ~/.cabal/bin/agda # 验证版本agda-mode 对版本敏感建议 2.6.x agda --version # 顺便确认标准库路径可访问没有装标准库时这条命令会报错 agda -l standard-library --help 21 | head -n 3逻辑说明which agda查的是 PATH 里的执行路径这个路径决定了扩展能不能正常启动进程。如果你在~/.bashrc或~/.zshrc里配了 PATH 但 VS Code 还是找不到常见坑是 VS Code 的 GUI 启动方式没有继承 shell 配置文件的环境变量。解决办法是手动在扩展设置里把agda-mode.executablePath指到绝对路径一劳永逸。参数说明--help只是顺手验证一下标准库能否被加载。如果这里输出像Failed to find source之类的信息说明标准库安装位置不对或者AGDA_DIR环境变量指向了错误目录。后面会专门讲这个排查。常见的发行版仓库里装的 Agda 版本通常偏旧。如果你发现某些交互命令不可用例如 case split 的行为和文档描述不一致十有八九是版本不对。能装多新就装多新特别是 2.6.4 之后的版本很多 agda-mode 协议细节在重构后和旧版本不兼容。我用的是 2.6.x 的中间版本跑基础设施没问题但如果你直接用最新开源库的语法有些实验性特性会提示「需要更高版本」。这个不算 bug算预期行为。2.2 在 VS Code 里安装扩展并配置可执行文件路径扩展市场里搜 agda-mode装那个名字最直接的就行。装好后不要急着打开.agda文件先去设置里把可执行文件路径配好。// .vscode/settings.json { agda-mode.executablePath: /home/YOUR_USER/.cabal/bin/agda, // 下面这个放扩展日志排查时会用到 agda-mode.debug.enable: true }逻辑说明agda-mode.executablePath是连接扩展和 Agda 的桥梁。不配这个扩展会在 PATH 里找agda这个行为在 macOS 上尤其坑因为 GUI 应用进程拿到的 PATH 非常短$HOME/.cabal/bin这种路径根本不在里面。因此建议所有安装方式下都显式配置这个绝对路径确定性最好。参数说明debug.enable平时没必要开但遇到「点击命令没反应」「加载卡死」这类问题时打开它可以让扩展日志暴露在输出面板里。日志里会有完整的 agda 进程输出注意观察有没有报模块找不到或者协议错误。配完路径重启窗口再打开任何一个.agda文件。此时右下角状态栏如果出现Loading ...到Idle的切换说明扩展和 Agda 进程已经正常通信。这个状态栏提示比任何配置检查都直接。2.3 最小验证跑通一个含类型的加载流程配置完成后你需要跑一个真实文件来确认整套链路通畅而不是只看高亮有没有生效。先建一个最简文件然后加载它。module hello where open import Data.Nat using (ℕ) open import Relation.Binary.PropositionalEquality using (_≡_) n : ℕ n 1 1 proof : n ≡ 2 proof refl用CtrlEntermacOS 上是CmdEnter加载。加载成功后编辑器里每个字符下方会出现金色点状高亮光标移动到proof那一行按CtrlC CtrlD查询类型应该显示n ≡ 2。逻辑说明这个验证文件不只是测高亮它的核心价值在于验证三件事一是 Agda 进程能正常启动并加载库二是Data.Nat等标准库路径被找到三是查询类型命令能正常回传数据。三者全通过后面写代码才算真正进入 agda-mode 工作流。参数说明refl是自反性证明项open import是模块导入这两行代码如果报错不需要看具体错误——先确认你的 agda 版本是否自带标准库很多发行版安装的 agda 包里并不包含标准库需要单独装。验证标准库路径可以用agda -l standard-library命令如果报找不到回到 2.1 的第三行验证命令去查。3. 日常开发核心命令把 agda-mode 用成交互式 REPL装了 agda-mode 不是只为了看彩色高亮。它的价值在于「增量检查」和「洞驱动开发」。这两个词听起来玄实际操作就是你不需要把整个文件写完一次性编译而是写一个?占位让 Agda 告诉你这个洞需要什么类型再一点一点填。这套流程在 Emacs 的 agda-mode 里打磨了很多年VS Code 移植版把这套按键映射基本照搬过来了。3.1 增量加载CtrlEnter 是怎么工作的打开一个.agda文件按CtrlEnter会对当前文件做增量加载。第一次加载会拉取所有依赖库之后再次修改文件时它只重载改动点速度明显快。module incremental where open import Data.Nat using (ℕ; __) addOne : ℕ → ℕ addOne n n 1修改addOne n n 1里的 1为 2再次按CtrlEnter。注意观察右下角状态变化正常情况是Checking ...不到一秒后回到Idle。如果文件里有未闭合的括号或错误的类型签名扩展会在问题行下方画红色波浪线同时在问题面板里给出错误类型。逻辑说明增量加载的核心是 Agda 的模块缓存机制。每个.agdai文件记录了这个模块的类型检查结果重新加载时只有依赖关系变化的模块会重新检查。这个机制也是后续自动补全和类型查询能瞬时响应的基础。注意一点CtrlEnter不是全量编译它只检查当前文件及其依赖。如果你的项目包含多个文件且改动了某个底层模块需要先加载底层模块再重新加载引用它的文件否则会提示模块已经过时。3.2 hole 与 goal让类型告诉你下一步写什么这是 agda-mode 最核心的工作方式。在 Emacs 里输入?并加载后会产生一个 goalVS Code 移植版主要展示在左侧的Agda Goals面板里。把光标移动到?上按CtrlC CtrlC可以对目标变量做 case split。module hole-demo where open import Data.Nat using (ℕ; __) open import Data.Nat.Properties using (-comm) comm : ∀ (m n : ℕ) → m n ≡ n m comm m n ?加载后左侧 goals 面板显示目标类型m n ≡ n m。此时按CtrlC CtrlC扩展会询问要拆分哪个变量——光标所在位置默认是你正在试图定义的变量。对m做 case split 后编辑器自动生成两个分支comm zero n ? comm (suc m) n ?逻辑说明case split 不是简单的「展开定义」而是根据类型构造器自动生成所有可能的模式分支。对于自然数就是zero和suc m对于列表就是[]和x ∷ xs。这样自动生成分支的正确性由 Agda 保证而不是你手写猜的可以减少很多低级模式匹配错误。参数说明CtrlC CtrlC之后会弹出输入框默认填写光标处的变量名。如果你有多个变量需要拆分可以手动输入m n用空格分隔一次生成嵌套分支。实际项目里我更习惯逐个拆因为每个分支生成后还能看 goals 面板变化更容易判断方向对不对。3.3 自动补全与 refine半自动填洞填洞有两招一个是CtrlC CtrlSpace调起自动补全菜单一个是CtrlC CtrlR做 refine后者会尝试用当前环境中已有的定义去填洞。module refine-demo where open import Data.Nat using (ℕ; __) open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym) sym-demo : ∀ {m n : ℕ} → m ≡ n → n ≡ m sym-demo {m} {n} p ?把光标放在?上按CtrlC CtrlR扩展会搜索sym和trans等可用定理生成一个候选列表。选择sym p后洞被填上类型检查直接通过。逻辑说明refine 的粒度比 auto 小它不尝试猜整个证明项而是检查环境中每个名字的类型签名看哪个能匹配当前目标类型。对m ≡ n → n ≡ m这个洞sym : m ≡ n → n ≡ m正好完全匹配所以会被列在最前面。对于更复杂的目标refine 通常会列出多个候选你的工作是判断哪个语义上是对的。这里有个使用习惯新手容易把所有希望寄托在 auto 上但 agda-mode 的 auto 能力比主流语言的代码补全弱很多它更擅长的是「帮你把已有定义对上类型」而不是「替你发明证明」。真正的证明思路要靠你自己想编辑器只负责验证。理解了这一点agda-mode 在项目中的定位就清晰了。日常开发时把「打洞」当成常态写代码的过程就是不断填洞并看反馈这与传统编辑器里写代码完全不是一个节奏。4. 配置与项目级设置让 agda-mode 符合你的工作方式安装完成只是开始。实际项目中最常遇到的问题不是「命令怎么按」而是「为什么我的文件加载这么慢」「为什么这个库 import 失败」「为什么字体显示方块」。这些都要靠配置解决。agda-mode-vscode 把大部分配置项放在扩展设置里但真正影响行为的配置分散在语言服务端的启动参数和环境变量中。4.1 扩展设置与 AGDA_DIR 环境变量Agda 运行时会查找一组配置和库文件根目录由AGDA_DIR决定默认是~/.agda。这个目录下有libraries文件记录了系统里所有标准库和第三方库的位置。# 查看当前 AGDA_DIR 指向哪里 echo $AGDA_DIR # 输出为空时默认就是 ~/.agda # 查看 libraries 配置文件的内容 cat ~/.agda/libraries # 内容类似 # /usr/share/agda-stdlib/standard-library.agda-lib # 查看默认使用的库列表 cat ~/.agda/defaults逻辑说明libraries文件是库注册表defaults文件是默认加载列表。如果你的项目 import 某个库失败先去这两个文件里看库是否注册、是否加入 defaults。很多所谓「标准库没装上」的问题实际上是 libraries 路径配了但defaults没更新。参数说明如果AGDA_DIR没设置但你想强制指定可以在 VS Code 的终端配置里添加环境变量。不想全局改的话在项目settings.json里给agda-mode的进程单独配置也是可行的——但这个扩展有些版本不支持传入环境变量稳妥做法还是改.bashrc或系统环境变量后重启窗口。4.2 用 agda 命令行参数控制加载行为扩展设置字段agda-mode.agdaArgs可以把参数传给底层的 agda 进程。这是最灵活的一层因为 Agda 的命令行参数很丰富比如--local-interaction可以禁用一些远程交互特性某些网络环境或特殊文件系统下能减少卡顿。// .vscode/settings.json 中的完整配置示例 { agda-mode.executablePath: /home/user/.cabal/bin/agda, agda-mode.agdaArgs: [ --no-libraries, // 只用于确认库注册问题平时不要开 --include-path, /home/user/projects/my-lib/src ], agda-mode.loadOnOpen: true, agda-mode.verbose: false }逻辑说明--include-path是经常用到的参数。当你项目里有一个本地库没有装进系统级的libraries注册表时用这个参数直接告诉 agda 去哪里找模块。比改~/.agda/libraries更轻量而且不污染全局配置项目换一台机器也能通过settings.json里这行配置保持可复现。参数说明--no-libraries一般是排查用的开了它 agda 就不会加载 defaults 里的库如果此时你的代码能加载而之前加载不了说明问题出在库注册表配置上。排查完记得关掉否则后面所有依赖标准库的文件都会报错。loadOnOpen决定打开文件是否立即加载在超大文件上建议关掉避免打开瞬间卡住编辑器。4.3 多文件项目模块路径与依赖顺序真实项目很少只有一个文件。多文件时的第一个坑是 import 路径Agda 的模块名由文件路径推导但基路径由AGDA_DIR或 include path 决定。一个常见的项目结构是project-root/ ├── src/ │ ├── Foo.agda │ └── Bar.agda ├── .vscode/ │ └── settings.json └── project.agda-lib# 项目库文件内容示例 project.agda-lib name: my-project depend: standard-library include: src逻辑说明project.agda-lib文件声明了这个项目是一个 Agda 库include: src指明模块根目录是src。有了这个文件Foo.agda在其他模块里被import Foo引用时agda 会去src目录下找Foo.agda。如果不建这个 lib 文件你就得在每个需要引用 Foo 的文件里写相对路径极容易出错。还有一个依赖顺序的坑import只是声明不会自动触发重新加载。如果你的Foo.agda改了定义而Bar.agda里有import Foo光是保存Foo文件还不够要在Bar.agda里再按一次CtrlEnter重新加载才能拿到新的接口类型检查结果。这个行为和直觉相反很多从 Rust、Go 转过来的开发者会在这个地方卡半天。5. 避坑agda-mode 最常见的 5 个翻车现场这个扩展最大的问题不是功能少而是错误提示不直观。很多时候屏幕上什么都没发生你以为插件坏了其实只是某个路径没指对或者某个协议握手失败。下面这几条都是我自己和旁边同事反复踩过的真实场景按「现象 → 原因 → 解决」写清楚。5.1 扩展装好了按 CtrlEnter 完全没反应现象文件打开了高亮也正常但按下CtrlEnter毫无反应状态栏一直停留在空状态不看日志根本不知道发生了什么。原因绝大多数情况是agda-mode.executablePath没指向有效文件或者扩展压根没启动 Agda 进程。还有一种隐蔽的情况是装了多个 Agda 版本PATH 里指向 A扩展里配置指向 B两者版本不一致导致握手失败。解决先把agda-mode.debug.enable打开看输出面板有没有内容。如果日志显示Error: ENOENT说明路径不对。这时用which agda拿到真实路径填进executablePath重启窗口再试。如果是版本不一致在终端里分别执行agda --version和扩展配置路径下agda --version确保两个输出一致。5.2 大量 Unicode 字符显示成方块或问号现象代码里到处是∀、→、≡这些字符编辑器里渲染成豆腐块或者空格错乱。原因VS Code 的默认字体不支持 Agda 常用的 Unicode 数学符号。这不是 agda-mode 的问题而是字体渲染问题但代码里全是怪异符号时很多人会误以为是扩展的高亮坏了。解决在 VS Code 设置里把editor.fontFamily改成支持这些字符的字体。常用的有 Noto Sans Mono、更纱黑体Sarasa Mono SC、Fira Code 加一个 fallback。// .vscode/settings.json { editor.fontFamily: Sarasa Mono SC, Fira Code, monospace }逻辑说明字体列表的 fallback 机制是第一个字体缺字符时逐个向后查直到找到能渲染某个字符的字体。所以前面可以放自己最喜欢的编程字体最后加一个必然支持 Unicod e 运算符号的字体兜底。配完之后→、∀、≡、ℕ这些符号都会正常显示整体观感提升非常大。5.3 AgdaGoals 面板一直转圈加载不结束现象状态栏卡在Checking ...超过几十秒或者模块改动量很小但加载时间异常长。原因大多是模块缓存问题。.agdai文件过期但没触发重新编译或是某个库模块被强制重新加载导致连锁反应。另一个常见原因是文件里有个变量名拼写错误Agda 尝试在环境里找该定义但找不到错误信息被隐藏。解决先按CtrlC中断当前加载检查文件里有没有明显参考不存在的名字。如果实在找不出来直接把.agdai缓存文件和.agda同目录下的_build目录清掉重新加载。# 清除当前目录下的 Agda 缓存 find . -name *.agdai -delete rm -rf _build逻辑说明.agdai文件是 Agda 模块的编译产物类似于.o文件。正常增量构建非常快但一旦某个依赖模块的接口变了而缓存没更新agda 会陷入奇怪的加载循环。强制清理是最后的办法代价是本次加载会全量编译但能一口气解决所有缓存不一致的问题。5.4 保存文件后自动加载失败报no such module现象文件保存后状态栏显示错误点开看是Failed to find source of module ...但同一个模块在终端里手动agda加载是成功的。原因工作目录的问题。扩展启动 agda 进程时的工作目录可能不是你的项目根目录导致 include path 解析不到。也可能项目级settings.json的agdaArgs里 include path 写的是相对路径而进程工作目录不同相对路径解析结果就不对。解决在agdaArgs里用绝对路径写 include path或者干脆在项目根目录建.vscode/settings.json并确保 VS Code 工作区根目录就是项目根目录。路径不要写相对当前文件的方式。{ agda-mode.agdaArgs: [ --include-path, /absolute/path/to/project/src ] }5.5 自动补全CtrlC CtrlSpace永远返回空列表现象在 hole 里按自动补全快捷键弹出菜单但显示 No results或者完全没有任何反应但加载和类型查询都正常。原因很大概率是你不在一个合法的 hole 里。光标必须停留在某个?或洞的位置普通代码区域没有补全目标。另外CtrlC CtrlSpace的候选来自当前加载的环境如果改动还没被CtrlEnter加载进去候选列表就是旧的甚至为空。解决先确认光标位置——在 VS Code 里洞会有特殊边界标记现在版本会直接给?一个高亮背景。然后按CtrlEnter重新加载等状态栏回到Idle再按补全快捷键。如果还是空回到 5.3 清理缓存。记得补全不返回结果不等于插件坏了它更可能是因为环境中确实没有类型匹配的候选。6. 进阶技巧把 agda-mode 当成依赖类型的 REPL 终端不满足于「能用」那接下来值得做的两件事是自定义 keybinding 和把 hole 当作临时求值器用。VS Code 的 keybinding 可以覆盖 agda-mode 自带的快捷键。我习惯把 case split 从CtrlC CtrlC改成AltC因为后者的手指移动距离小很多在频繁拆变量的场景下省力。// keybindings.json [ { key: altc, command: agda-mode.case, when: editorTextFocus agdaModeActive }, { key: ctrlenter, command: agda-mode.load, when: editorTextFocus agdaModeActive } ]逻辑说明agdaModeActive条件确保了快捷键只在加载了 agda-mode 的文件里生效不会污染其他语言文件的按键。这个 when 子句是 VS Code 扩展约定里的标准条件配置后即全局生效但不误触。第二个技巧是把 hole 当临时终端用。当你拿不准一个表达式类型时不用另建文件测试直接在当前文件的任意洞里输入表达式加载后看 goals 面板里显示的类型。例如你忘了__和_*_混合表达式需要什么优先级括号拆个洞试一下就行。这比任何文档都准确因为 Agda 显示的就是最终的类型检查结果。久而久之会形成一个习惯任何不确定的语法和类型都先打洞让系统回答而不是翻文档猜。这个习惯一旦养成依赖类型开发的节奏就顺了希望你也能在 agda-mode 里找到这种感觉。配 keybinding 的时候注意一个细节修改完keybindings.json之后不用重启 VS Code它热生效。但 agda-mode 扩展的when条件会感知当前文件是否为 agda-mode 管理状态第一次打开文件时可能需要按一次任意 agda 命令触发扩展激活否则快捷键会短暂不响应。这个延迟激活是正常的生命周期行为几秒后就会恢复。自动补全、查询类型这些命令去 Home 键都能用的默认配置和 Emacs 里的 agda-mode 保持一致的肌肉记忆位置也是这个移植版的一个优势——换编辑器时按键手感没变适应成本低。最后想提醒的是真正的瓶颈通常来自文件依赖关系设计和模块划分而不是编辑器本身希望这一套下来能帮你少走弯路。本文还有配套的精品资源点击获取