简介这份资源是面向 Agda 语言开发者与函数式编程学习者的 VS Code 扩展用于在 VS Code 中提供 agda-mode 支持解决 Agda 代码编辑、加载与类型交互操作的问题。安装前需确认终端中已正确安装 Agda打开 .agda 文件后可通过 C-c C-l 等组合键加载文件扩展还处于开发阶段的 Agda 语言服务器启用后可在面板右上角看到 LSP 标识。资源包共 179 个文件以 67 个 js 与 64 个 res 源码为主另含 out/in 测试用例、json 配置、md 文档、agda 示例及 less、yml、ttf 等资源压缩包约 457KB结构紧凑。已有 237 人学习下载。读者可借此了解 VS Code 扩展的按键映射设计、归一化级别命令与 Emacs 键位差异并参考其中的 Agda 示例与测试输入输出快速上手 Agda 开发环境配置与日常编辑操作。1. 在 VS Code 里让 Agda 真正跑起来从语法高亮到交互式证明很多人第一次在 VS Code 里打开.agda文件看到的是满屏白色文本没有语法高亮、没有类型提示、C-c C-l按下去毫无反应——于是得出一个结论Agda 在 VS Code 上不好用。问题几乎从来不在 Agda 本身而在于编辑器扩展、语言服务器和 Agda 可执行文件这三者没有接上。agda-mode-vscode要解决的就是这件事把 Agda 的交互式证明能力搬进 VS Code让你在编辑器里直接 load 文件、看 goal 上下文、做 case split、求值归一化而不是在终端和编辑器之间来回切。它适合两类人一类是从 Emacs 的agda-mode迁过来、舍不得交互式证明体验的另一类是刚学依赖类型、想用更熟悉的编辑器降低上手门槛的。这篇笔记按「装什么、怎么配、怎么用、哪里会翻车」的顺序讲清楚目标是让你照着做完就能在 VS Code 里完成一次完整的证明交互。2. 装之前先理清三件套Agda 可执行文件、语言服务器、编辑器扩展Agda 在 VS Code 里的工作方式和普通语言不太一样。它不是扩展自己解析源码而是扩展通过语言服务器协议去调用一个独立的 Agda 进程。所以「装扩展」只是三件事里的一件另外两件没做对扩展装十个也没用。2.1 三件套各自的职责与依赖关系先把角色分清楚Agda 可执行文件真正做类型检查、归一化、给出 goal 上下文的东西。它通常由 Haskell 工具链编译安装或者从系统包管理器装。没有它后面全是空转。Agda 语言服务器Agda 自带的一个模式让 Agda 以服务器方式启动通过标准输入输出和编辑器通信。它不是一个单独要下载的二进制而是 Agda 可执行文件的一个启动参数。VS Code 扩展负责把编辑器的按键、光标位置、文件内容翻译成语言服务器能懂的请求再把返回的 goal 信息渲染到界面上。依赖关系是单向的扩展依赖语言服务器语言服务器依赖 Agda 可执行文件。排查问题时永远从最底层往上查先确认agda命令本身能跑再确认语言服务器能启动最后才怀疑扩展。2.2 用命令行确认 Agda 与语言服务器可用在装扩展之前先在终端把底层确认掉。这一步能省掉后面大量「到底是扩展坏了还是 Agda 没装好」的扯皮。# 确认 agda 可执行文件在 PATH 里并看版本 agda --version # 确认语言服务器模式能启动会进入等待输入状态Ctrl-C 退出即可 agda --lsp # 看 agda 实际用的是哪个库路径后面配 includePath 要对上 agda --print-agda-dir逻辑说明agda --version验证可执行文件存在且版本可读agda --lsp验证这个版本支持语言服务器模式老版本 Agda 可能没有这个参数agda --print-agda-dir打印标准库安装目录后面配置搜索路径时要用到。参数说明--lsp是启动语言服务器的开关不带其他参数时它会从标准输入读请求。如果你执行后卡住不动说明启动成功按Ctrl-C退出。如果报unrecognized option说明 Agda 版本偏旧需要升级。2.3 安装扩展并指定 Agda 路径底层确认无误后在 VS Code 扩展面板搜索 Agda 相关扩展安装。安装完成后关键动作是告诉扩展去哪里找agda可执行文件——尤其是你用版本管理工具装了多个版本、或者agda不在默认 PATH 里的时候。在 VS Code 的settings.json里加{ agda.executable.path: /home/user/.local/bin/agda, agda.executable.args: [], agda.libraryPath: [ /home/user/.agda/defaults, /home/user/.agda/libraries ] }逻辑说明agda.executable.path直接指向可执行文件的绝对路径绕开 PATH 解析问题agda.executable.args留空表示不加额外启动参数需要调 RTS 参数时再填agda.libraryPath指向 Agda 的库索引文件让扩展在加载文件时能找到依赖库。参数说明路径一定要写绝对路径写相对路径或~在部分平台上不展开。libraryPath里放的是.agda/defaults和.agda/libraries这两个索引文件不是库源码目录本身。如果你只用标准库确认这两个文件里已经登记了标准库路径。提示改完settings.json后要重启 VS Code 窗口扩展不会热加载可执行文件路径。3. 在 VS Code 里跑通第一个 Agda 文件从 load 到 goal 交互配置接上之后真正的价值在于交互式证明。这一章用一个最小例子把 load、goal 查看、case split、求值这几步走一遍每一步都对应一个具体按键和预期结果。3.1 写一个最小可加载的 Agda 文件先建一个Hello.agda内容尽量简单只验证加载链路通不通module Hello where open import Data.Nat using (ℕ; zero; suc; __) open import Data.Nat.Properties using (-comm) -- 一个最简单的证明0 n 等于 n -identityˡ : ∀ (n : ℕ) → zero n ≡ n -identityˡ n refl逻辑说明module Hello where声明模块名Agda 要求模块名和文件名对应两个open import引入自然数和加法交换律最后这个引理用refl直接成立因为zero n在定义上就归约到n。这个文件故意写得极简目的是让加载失败时排除掉复杂证明的干扰。参数说明∀是全称量词的语法糖≡是命题相等类型。refl能成立的前提是两边在定义上相等这里zero n按__的定义展开后就是n所以成立。3.2 load 文件与查看 goal 上下文打开Hello.agda后用命令面板执行 Agda 的 load 命令或者用默认快捷键C-c C-l。加载成功后编辑器底部状态栏会显示已检查文件里每个绑定旁边可能出现类型信息。如果加载失败错误会以诊断形式标在对应行上。常见的是模块名不匹配、导入路径找不到、或者某个洞没填。加载这一步是整个交互的基础没 load 成功之前后面所有命令都不会有正确响应。查看 goal 的方式是把光标放在一个洞里。洞的写法是?或{! !}。比如把上面的证明改成-identityˡ : ∀ (n : ℕ) → zero n ≡ n -identityˡ n {! !}重新 load 后光标放进洞里执行「显示 goal」命令编辑器会弹出一个面板显示当前 goal 的类型和上下文里所有变量的类型。这个面板就是交互式证明的核心界面等价于 Emacs 里的 goal buffer。3.3 case split 与自动求解把洞填上的两条路有了洞之后最常用的两个操作是 case split 和 auto。case split 针对的是「对某个变量分情况讨论」。把光标放在洞里执行 case split 命令扩展会提示你输入要拆分的变量名。比如输入nAgda 会把当前 goal 替换成两个分支-identityˡ : ∀ (n : ℕ) → zero n ≡ n -identityˡ zero {! !} -identityˡ (suc n) {! !}逻辑说明case split 本质是让 Agda 根据变量的构造子把目标拆成多个子目标每个子目标对应一个构造子。ℕ有两个构造子zero和suc所以拆成两支。这一步省去了手写模式匹配的机械劳动。参数说明输入变量名时要和上下文里的名字完全一致。如果变量在上下文里叫n你输入mAgda 会报找不到变量。auto 则是让 Agda 尝试自动填洞。对上面两个分支第一个分支zero情况下zero zero ≡ zero直接refl成立第二个分支需要一点归纳auto 不一定能一次搞定但简单情形它能直接补上。执行 auto 命令后如果成功洞会被替换成具体证明项。注意auto 不是万能的复杂归纳它经常填不上。填不上不代表你的方向错了只是需要手动给归纳假设。3.4 求值与归一化确认你的表达式到底算成了什么调试证明时经常需要确认某个表达式在 Agda 眼里到底归约成了什么。把光标放在一个表达式上执行「求值」命令扩展会显示这个表达式的范式。-- 把光标放在下面这个表达式上求值 _ : zero suc (suc zero) ≡ suc (suc zero) _ refl逻辑说明求值命令会把选中的表达式做完整归一化显示最简形式。上面这个表达式求值后应该显示suc (suc zero) ≡ suc (suc zero)确认两边确实相等refl才成立。参数说明求值默认做完整归一化遇到大项可能很慢。如果只想看弱头部范式可以在设置里调整归一化策略但多数调试场景完整归一化更直观。4. 参数怎么调搜索路径、超时与内存的实战设置扩展能跑通之后接下来影响体验的就是参数。配错了不会报错但会表现为「加载特别慢」「找不到库」「大文件卡死」这类玄学问题。这一章把几个真正需要调的参数讲清楚。4.1 includePath 与 libraryPath 的区别和配法这两个参数最容易混。简单说libraryPath指向 Agda 的库索引文件告诉 Agda「有哪些库可用」。includePath指向额外的源码搜索目录告诉 Agda「去哪些目录找 import 的模块」。如果你用的是标准库libraryPath配好就够了。如果你有自己的项目模块分散在多个目录才需要includePath。{ agda.includePath: [ ${workspaceFolder}/src, ${workspaceFolder}/lib ] }逻辑说明${workspaceFolder}是 VS Code 的变量展开为当前工作区根目录。把项目源码目录加进去Agda 在解析import时就会去这些目录找。参数说明includePath里的路径顺序影响查找优先级靠前的先找。如果两个目录有同名模块靠前的胜出。这一点在模块重名时是坑配的时候尽量保证模块名全局唯一。4.2 加载超时与内存参数大文件不卡死的调法Agda 类型检查是出了名的吃内存和时间尤其是带大量隐式参数和元变量的文件。扩展默认的超时对中等文件够用对大文件会直接超时断开。{ agda.timeout: 60000, agda.executable.args: [ RTS, -M4G, -RTS ] }逻辑说明agda.timeout把单次请求的超时从默认值拉长到 60 秒给大文件检查留时间agda.executable.args里的RTS -M4G -RTS是给 Agda 运行时传堆内存上限限制在 4GB防止它无限吃内存把机器拖垮。参数说明-M4G里的4G按你机器内存调整一般给到物理内存的一半以内。RTS和-RTS是 Haskell 运行时参数的包裹标记中间才是真正的 RTS 参数。如果你的 Agda 不是 GHC 编译的这组参数可能不生效。提示超时和内存是一对权衡。超时调太大、内存不限制遇到死循环的证明会让整个编辑器卡住内存限制太小大文件会直接 OOM 退出。4.3 交互命令的快捷键映射与冲突处理VS Code 的 Agda 扩展默认会注册一批C-c开头的快捷键和 Emacs 的agda-mode保持一致。但C-c在 VS Code 里本身也被大量使用冲突很常见。处理方式是打开键盘快捷方式设置搜索agda看哪些命令没绑上或者被覆盖。常见的冲突是C-c C-lload被其他扩展占用。解决办法是改成C-c C-l之外的两段式组合或者用命令面板直接调用。{ key: ctrlc ctrll, command: agda.load, when: editorLangId agda }逻辑说明这条绑定把 load 命令限定在 Agda 语言的文件里生效避免影响其他语言的编辑。when条件是关键不加的话C-c C-l会在所有文件里拦截。参数说明editorLangId agda是 VS Code 的语言标识条件Agda 文件的languageId就是agda。如果你的文件没被识别成 Agda先检查文件关联设置。5. 避坑与排查那些让 agda-mode-vscode 看起来「坏了」的瞬间这一章记录几个我实际踩过的坑每个都按现象、原因、解决写。这些问题的共同点是表面看是扩展坏了实际根因都在配置或环境。5.1 现象文件打开没有高亮所有命令无响应原因文件没有被识别为 Agda 语言。VS Code 靠扩展名和文件关联判断语言.agda默认应该关联但如果之前手动改过关联或者用了非标准扩展名比如.lagda.md这种文学化 Agda就会落到纯文本模式。解决打开命令面板执行「更改语言模式」选 Agda。如果是文学化 Agda确认扩展支持该格式并在设置里检查文件关联。改完后重新 load。5.2 现象load 报找不到模块但文件明明在原因includePath或libraryPath没配对Agda 的搜索路径里没有你的源码目录。Agda 找模块是按模块名映射到文件路径的Data.Nat对应Data/Nat.agda路径根目录必须在搜索路径里。解决用agda --print-agda-dir确认库目录检查libraryPath指向的索引文件内容。项目自己的模块把源码根目录加进includePath。注意模块名大小写敏感data.nat和Data.Nat不是一回事。5.3 现象goal 面板显示的类型信息是旧的原因文件改了但没重新 load。Agda 的交互信息是 load 那一刻的快照改了源码不重新 loadgoal 上下文不会更新。解决养成改完就C-c C-l的习惯。如果 load 很慢可以只 load 当前文件而不是整个项目。部分扩展支持增量检查但 Agda 本身的增量能力有限别指望它像 TypeScript 那样秒级响应。5.4 现象case split 后变量名变了证明对不上原因case split 会重命名变量以避免冲突尤其是嵌套拆分时。你原来写的引理引用了旧名字拆分后名字变了引用就断了。解决拆分后检查新生成的变量名把后续引用同步改掉。更稳的做法是拆分前先想清楚要拆哪个变量一次拆到位减少反复重命名。5.5 现象大文件 load 到一半扩展断开连接原因超时或内存不足。Agda 检查大文件时可能几十秒不返回扩展默认超时到了就断开表现为「语言服务器已停止」。解决调大agda.timeout给 Agda 加 RTS 内存参数。如果还是断考虑把大文件拆成多个小模块用import组织。Agda 的模块化对检查性能帮助很大一个几千行的单文件是性能灾难。6. 把交互式证明用顺几个让效率翻倍的进阶习惯前面讲的都是「能用」这一章讲「用顺」。Agda 的交互式证明有一套自己的节奏掌握几个习惯之后写证明的速度会有明显变化。第一个习惯是先写类型再写洞最后填。不要一上来就试图写完整证明。先把引理的签名写出来body 放一个洞load看 goal 上下文里有什么。上下文会告诉你手上有哪些假设、目标是什么类型很多时候看一眼就知道该用哪个引理。这个习惯的价值在于把「想」和「写」分开减少在错误方向上写一堆代码再删掉的时间。第二个习惯是善用 refine。refine 命令让你输入一个表达式Agda 会尝试把它应用到当前 goal 上如果类型能对上就把 goal 替换成这个表达式需要的子目标。比如 goal 是a ≡ c你 refine 一个传递性引理Agda 会自动生成两个子 goala ≡ b和b ≡ c。这比手动写trans再填两个洞快得多。第三个习惯是把常用引理放进一个自己的工具模块。标准库很全但每次都要open import一长串。建一个MyLib.agda把项目里反复用的引理重新导出其他文件只 import 这一个。这样既减少重复导入也方便统一改。第四个习惯是用求值确认而不是猜。遇到refl不成立别盯着代码猜把表达式选中求值看 Agda 到底把它归约成了什么。十次里有八次是某个隐式参数没推断对或者某个定义没展开。求值结果会直接告诉你差在哪。最后一个习惯是控制单文件规模。Agda 的类型检查对文件大小很敏感一个文件超过几百行load 时间会明显上升。把证明按主题拆成多个模块每个模块几十到一两百行用import串起来。这样每次只 load 当前模块交互响应快很多。我自己的经验是单文件超过五百行就该考虑拆了超过一千行基本没法愉快交互。这套习惯没有一条是扩展特有的但agda-mode-vscode把这些操作都做成了编辑器命令用起来比在终端里手动调 Agda 舒服得多。真正决定效率的还是你对 Agda 本身的理解工具只是把反馈循环缩短了。希望帮到你。本文还有配套的精品资源点击获取