简介这份资源是面向 Agda 依赖类型语言开发者的 VS Code 扩展为习惯在 VS Code 中编写证明与函数式程序的用户提供 agda-mode 支持解决 Agda 官方工具链长期依赖 Emacs 环境、编辑器选择受限的问题。压缩包共 179 个文件约 457KB以 67 个 js 与 64 个 resReScript源码为主体辅以 13 个 out、13 个 in 测试用例、5 个 json 配置、4 个 agda 示例文件及 less、yml、ttf 等资源结构紧凑便于阅读扩展实现与调试。扩展支持通过 C-c C-l 加载 Agda 文件并已引入仍处于开发阶段的 Agda 语言服务器启用后可在面板右上角看到 LSP 标识针对 VS Code 无法像 Emacs 那样使用 C-u 前缀的问题改用 C-x、C-y 等按键映射来切换类型命令的规范化级别。目前已有 236 人学习下载适合希望迁移到 VS Code 的 Agda 使用者、ReScript 扩展开发者以及研究编辑器与语言服务器集成的读者参考。1. 在 VS Code 里写 Agda为什么值得折腾这套模式如果你写过一段时间的 Agda大概率经历过这种割裂终端里agda --interactive敲得飞起但一转头想看看定义、跳个文件、顺手改两行就得在编辑器和命令行之间反复横跳。agda-mode-vscode 要解决的就是这件事——把 Agda 的交互式开发体验搬进 VS Code让「写证明」和「写代码」在同一块屏幕里完成。它适合已经装好 Agda 编译器、想换一个更顺手的编辑器前端的人也适合刚接触依赖类型、被 Emacs 劝退的新手。核心价值只有一句话用 VS Code 的补全、跳转、多光标去驱动 Agda 的 goal 求解和类型检查。这篇不聊 Agda 语言本身只讲这套模式怎么装、怎么配、怎么用以及我踩过的那些坑。2. agda-mode-vscode 到底在做什么前端与编译器的分工2.1 它不是编译器是 Agda 的「遥控器」很多人第一次搜 agda-mode-vscode会误以为它是一个独立的 Agda 实现。不是。Agda 的编译、类型检查、goal 求解全部由本地的agda可执行文件完成agda-mode-vscode 只是 VS Code 的一个扩展负责把编辑器的按键、光标位置、文件内容翻译成 Agda 的交互命令再把返回的 goal 状态、类型信息、错误位置渲染回编辑器。理解这个分工很重要因为它决定了排错方向。扩展本身出问题表现为命令无响应、面板空白Agda 编译器出问题表现为类型检查报错、agda命令找不到。两者要分开看。常见做法是先确认agda --version在终端能跑通再装扩展。顺序反了你会花大量时间怀疑扩展其实是编译器没配好。2.2 交互式开发的核心goal 与 holeAgda 写证明时最常用的动作是「留一个洞让编译器告诉我这里该填什么」。这个洞就是 hole写成?或{! !}。agda-mode-vscode 把围绕 hole 的操作做成了命令加载文件Load把当前文件送给 Agda 检查所有 hole 变成待填的 goal显示 goal 类型Goal Type光标放在 hole 上看这个位置需要什么类型显示上下文Context看当前作用域里有哪些变量、它们的类型是什么自动求解Auto让 Agda 尝试用简单策略填上这个 hole精细化Refine给出一个候选构造子把 hole 拆成更小的 hole这套流程是 Agda 交互式开发的主循环。agda-mode-vscode 的价值就是让这个循环不用离开 VS Code。2.3 安装扩展与前置依赖前置依赖只有两个Agda 编译器和 VS Code。Agda 的安装方式取决于你的平台常见的是用包管理器或从源码构建。装完后确认agda --version能打印版本号即可。然后装扩展。VS Code 的扩展市场里搜agda找到 agda-mode-vscode 安装。装完重启 VS Code。如果你用的是 VS Code 的远程开发或容器环境注意扩展要装在「远程」那一侧不是本地。这是新手最容易翻车的地方本地装了扩展但 Agda 跑在容器里命令发不过去。2.4 最小可跑通示例建一个文件Hello.agdamodule Hello where data Bool : Set where true : Bool false : Bool not : Bool → Bool not true false not false true保存后用命令面板CtrlShiftP执行Agda: Load。如果底部状态栏出现Checking Hello然后变成Hello: Ok说明链路通了。此时把not的某一行改成not true ?再 Load光标放到?上执行Agda: Goal Type应该能看到期望类型是Bool。这一步跑通后面所有操作才有意义。跑不通先查agda是否在 PATH 里再查扩展的输出面板有没有报错。3. 把 agda-mode-vscode 配到顺手按键、路径与语言服务器3.1 按键绑定默认不够用得自己改agda-mode-vscode 默认的按键绑定沿用了 Emacs agda-mode 的习惯比如C-c C-l加载、C-c C-,看上下文。但 VS Code 的按键生态和 Emacs 不同直接照搬会冲突。我一般会做两件事第一把最常用的几个命令绑到顺手的组合上。在keybindings.json里加[ { key: ctrlaltl, command: agda.load, when: editorLangId agda }, { key: ctrlaltt, command: agda.goalType, when: editorLangId agda }, { key: ctrlaltc, command: agda.context, when: editorLangId agda } ]when条件限定只在 Agda 文件里生效避免污染其他语言的按键。命令名以扩展实际注册的为准可以在命令面板里搜Agda:看到完整列表。第二把输入 Unicode 符号的方式理顺。Agda 大量使用→、∀、λ这类符号手打不现实。agda-mode-vscode 提供了输入法式的符号替换比如输入\to自动变成→。这个功能默认开启但如果你的输入法或 VS Code 的其他扩展也抢这个行为就会打架。遇到符号不替换先禁用其他输入类扩展试试。3.2 Agda 路径与命令行参数扩展需要知道agda可执行文件在哪。如果agda已经在系统 PATH 里通常不用配。但如果你用 cabal 或 stack 装的或者装在非标准路径就要在 VS Code 设置里指定{ agda.path: /home/user/.cabal/bin/agda, agda.args: [--no-libraries] }agda.path是编译器路径agda.args是每次调用时附加的参数。--no-libraries在你不使用 Agda 标准库、或者库路径没配好时很有用能避免加载库导致的卡顿。参数怎么设取决于你的项目结构。如果项目有自己的.agda-lib文件扩展一般能自动识别。识别不到时手动指定--include-path指向库目录。3.3 语言服务器模式与旧版交互模式的区别agda-mode-vscode 有两种工作模式一种是基于 Agda 的交互式命令老模式一种是基于 Agda 语言服务器协议ALS。语言服务器模式提供更完整的补全、跳转、悬停提示但要求 Agda 版本较新且需要额外安装语言服务器。我一般会先试语言服务器模式因为它对「跳转到定义」「查找引用」支持更好。配置方式是在设置里启用{ agda.useLanguageServer: true }如果启用后扩展无响应或者日志里报语言服务器启动失败就退回交互模式。退回不是退步交互模式在 goal 操作上反而更直接。两种模式的命令名可能不同切换后如果按键失效重新检查一遍命令面板里的可用命令。3.4 多文件项目的加载策略Agda 项目通常由多个模块组成模块之间有 import 关系。agda-mode-vscode 加载一个文件时Agda 会连带检查它依赖的模块。如果依赖链很长每次 Load 都会很慢。常见做法是把不常改的底层模块先单独 Load 一次让 Agda 缓存住。之后改上层文件时只要底层没动检查会快很多。另外避免在项目根目录放太多无关的.agda文件Agda 扫描目录时会被拖慢。如果项目用了标准库确认.agda-lib里的depend写对了。写错的表现是 import 报「找不到模块」但文件明明存在。4. 日常写证明的工作流从 hole 到完整定义4.1 一个完整的 goal 求解循环假设要证明not (not b) ≡ b。先写框架not-invol : (b : Bool) → not (not b) ≡ b not-invol b ?Load 之后光标放在?上执行 Goal Type看到目标是not (not b) ≡ b。执行 Context看到b : Bool。接下来对b做情况分析。Agda 的 case 命令可以自动把b拆成true和false两个分支not-invol : (b : Bool) → not (not b) ≡ b not-invol true ? not-invol false ?两个分支分别 Load各自看 goal。true分支的目标变成not (not true) ≡ true执行 Refine 或 AutoAgda 通常能直接化简成refl。false分支同理。这个循环——留洞、看类型、看上下文、case 拆分、refine、auto——就是 Agda 交互式开发的全部。agda-mode-vscode 把每一步都做成了命令熟练之后几乎不用离开键盘。4.2 常用命令与触发时机命令作用什么时候用Load检查文件生成 goal每次改完代码Goal Type显示当前 hole 的目标类型不知道填什么时Context显示作用域内变量需要知道有哪些可用变量Case对变量做情况分析目标依赖某个变量的取值Refine用构造子细化 hole目标类型有明确的构造子Auto自动求解简单 goal目标是 refl 或简单组合Normalize化简表达式想看看表达式化简成什么这些命令不需要背命令面板里搜Agda:都能找到。关键是知道什么时候用哪个。我的习惯是先 Context 看有什么再 Goal Type 看要什么然后决定是 Case 还是 Refine。4.3 处理类型错误与未解决交互点Agda 报错时错误信息会定位到具体位置。agda-mode-vscode 会在编辑器里标出错误行并在面板里显示详细信息。常见的错误类型类型不匹配期望A但得到B通常是构造子用错或参数顺序错未解决的交互点还有 hole 没填Load 后 goal 列表里能看到终止检查失败递归定义不满足终止条件需要调整结构遇到类型不匹配不要急着改代码先用 Goal Type 和 Context 确认当前上下文再决定怎么改。很多时候错误不在报错那一行而在它依赖的某个定义。未解决的交互点会累积。如果 goal 列表里有一堆陈旧的 hole先清理掉不再需要的再重新 Load避免干扰。4.4 与版本控制配合的注意点Agda 文件里如果有未填的 hole提交上去会让协作者也看到这些 goal。团队协作时通常约定不提交带 hole 的文件或者用{! !}显式标记待办。另外Agda 的编译产物.agdai文件一般不入版本控制在.gitignore里排除。这些文件是缓存不同机器上重新生成即可。5. 避坑与排查agda-mode-vscode 最常见的五类翻车5.1 现象Load 无响应状态栏一直转圈原因Agda 编译器路径不对或者 Agda 在检查一个很大的依赖链。扩展发出命令后等不到返回就一直挂起。解决先在终端手动跑agda Hello.agda确认编译器本身能跑通且速度正常。如果终端也慢是项目结构问题不是扩展问题。如果终端快但扩展慢检查agda.path是否指向了错误的可执行文件比如指向了一个包装脚本。5.2 现象Unicode 符号不替换输入\to出来还是\to原因VS Code 的输入法拦截了按键或者扩展的符号替换功能被其他扩展覆盖。解决禁用其他输入类扩展重启 VS Code。如果还不行检查设置里agda相关的输入法选项是否开启。有些键盘布局下反斜杠本身需要组合键输入也会导致替换失败。5.3 现象语言服务器模式启动失败日志报连接错误原因Agda 语言服务器没装或者版本与 Agda 编译器不匹配。解决确认语言服务器可执行文件存在且在 PATH 里。如果不想折腾直接关掉agda.useLanguageServer退回交互模式。交互模式在 goal 操作上完全够用只是少了跨文件跳转的便利。5.4 现象import 标准库报「找不到模块」原因.agda-lib文件里的depend没写对或者--include-path没指向库目录。解决检查项目根目录的.agda-lib确认depend里的库名和实际安装的库名一致。用agda --print-agda-lib之类的命令查看库解析情况。如果库装在非标准位置在agda.args里加--include-path/path/to/library。5.5 现象改了底层模块上层文件不重新检查原因Agda 的缓存机制。底层模块的.agdai缓存还在Agda 认为没变。解决删掉对应的.agdai文件或者用agda --ignore-interfaces强制重新检查。日常开发中如果确认底层改了但上层没反应先删缓存再 Load。6. 进阶把 agda-mode-vscode 用出肌肉记忆写到一定程度你会发现真正的瓶颈不是工具而是「想清楚下一步该做什么」。agda-mode-vscode 能帮你的是把「想」和「做」之间的延迟压到最低。我的习惯是左手放在 Case 和 Refine 的快捷键上右手不离方向键眼睛盯着 goal 面板。一个证明写下来大部分时间花在思考上操作本身几乎无感。几个能明显提速的技巧。第一把Agda: Load绑到一个不需要看键盘的位置因为你会按它几百次。第二善用 Auto但不要依赖它——Auto 解不出来的 goal往往说明你对目标的理解还不够这时候应该回去看 Context 和 Goal Type而不是反复按 Auto。第三定期清理 hole不要让未解决的交互点堆积堆积的 goal 会让你误判当前进度。验证你的配置是否到位有个简单方法找一个中等规模的证明比如标准库里的某个引理从零开始用 agda-mode-vscode 写一遍全程不碰终端。如果能在不查文档的情况下完成说明工具链已经内化成习惯。如果中途卡住卡住的地方就是你该补的配置或该练的操作。我自己的血泪经验是不要一开始就追求语言服务器模式的全功能。先用交互模式把 goal 循环跑熟再逐步开启语言服务器。反过来做你会被各种启动失败和版本不匹配消耗掉耐心最后误以为这套工具不好用。工具没问题是顺序错了。希望帮到你。本文还有配套的精品资源点击获取