Agda交互模式迁移VS Code：配置、用法与排错指南

简介面向Agda开发者的VS Code扩展集成包在VS Code中提供类Emacs的Agda交互模式支持通过快捷键加载文件、执行命令并可将后端切换至Agda语言服务器LSP在面板中看到更智能的类型检查反馈。压缩包共179个文件、约457KB代码以ReScript源文件res为主并编译为js同时包含agda测试示例、in/out输入输出测试数据、json/yml配置、less/css样式与Markdown说明模块划分清晰适合直接当作VSCode扩展开发的参考项目。已有237人浏览学习适合熟悉Agda或函数式编程、希望提升编辑体验的读者从示例中可以学到大小写拆分、输入法支持、特定问题单复现等功能的落地方式也能了解如何用ReScript编写扩展、绑定快捷键、配置LSP对接以及替换主题样式为后续二次开发或移植到其他编辑器提供基础。1. 为什么我最终把 Agda 的交互模式搬回了 VS Code如果你写过几天 Agda一定对那个窗口布局有印象左边是源码底下是 Emacs 的交互缓冲区所有命令都绑在 CtrlC 的组合键上。我最早也是从 Emacs 入的门但后来换机器、换显示器、换工作环境Emacs 配置反复翻车最终被 agda-mode-vscode 这个扩展说服把日常证明工作迁到了 VS Code 上。它做的事不是“多加一个语法高亮”而是把 Agda 的整条交互链路搬进编辑器加载、聚焦洞口、自动补全、做 case split全都能在 VS Code 的命令面板里直接触发。这篇文章覆盖的是我实际在多个项目里验证过的落地路径怎么把 agda 本体和扩展装通怎么跑通第一个交互闭环按项目做哪些配置以及我踩过的那些不查几个小时的源码根本看不出原因的坑。看完你至少能判断一件事它到底适不适合你手头的工作以及如果决定用第一天应该做什么、遇到问题先查哪里。2. agda-mode-vscode 在跑什么从 Emacs 键位到扩展进程2.1 交互模式的本质是“编辑器 ↔ Agda 进程”的双向会话Agda 给你的不仅是编译错误提示它更核心的价值是“类型驱动编辑”你在源码里写一个洞hole让 Agda 告诉你这里需要什么类型的项然后你一边补一边让类型检查器反馈。这个能力来自 Agda 本体而不是编辑器所以无论用什么编辑器都要完成同一件事和 Agda 交互进程建立双向通信。agda-mode-vscode 沿用的还是 Agda 交互协议没有拐到通用的语言服务器协议上。扩展启动一个agda --interaction进程然后用 stdin/stdout 传命令、收结果。理解这一点排错思路就清楚很多界面上的“没反应”往往不是扩展坏了而是那条 stdin/stdout 链路断了或者 agda 进程卡在一个错误的解析状态里。我在模拟项目 X 里前后遇到的十几次“假死”几乎都是因为源码里有语法错误导致 Agda 进程没有返回负载。所以先别急着怀疑键盘绑定。第一步永远是确认 agda 本身能跑、能读你当前这个文件。2.2 装好一条链路Agda、标准库、扩展三件事按顺序做我推荐三件事按顺序来省的后面互相甩锅。先装 Agda 本体再装标准库如果你要写稍大一点的证明最后再装 VS Code 扩展。反着装的后果就是你打开第一个.agda文件时扩展已经激活了但底层 agda 不在 PATH 里加载一直转圈报错信息却藏在输出面板深处。安装 Agda 的方式要看你系统里已有的包管理器。常见的做法是直接用系统包管理器装稳定且依赖处理得干净# macOS 上用 Homebrew 装 Agda brew install agda # 装完看一眼版本确认真的可用 agda --version # Ubuntu/Debian 系 apt install agda # Windows 上建议用 winget 或直接下载安装包装完把 agda.exe 所在目录加进 PATH # 这一步做完最好重启 VS Code让扩展重新读环境变量装完 agda 之后有一个步骤很多人会跳过初始化标准库的接口文件。Agda 对标准库不是“编译成二进制”而是生成.agdai接口文件缓存。除非你的agda安装包自带缓存否则在 VS Code 里加载带标准库 import 的文件时会非常慢或者直接报 Not in scope 一类让人摸不着头脑的错。# 先确认标准库装到哪里了 which agda # 如果标准库在 ~/agda-stdlib 下通常需要先把库注册文件写好 mkdir -p ~/.agda echo $HOME/agda-stdlib/standard-library.agda-lib ~/.agda/libraries echo standard-library ~/.agda/defaults这里~/.agda/libraries是全局库列表~/.agda/defaults是每个新项目默认打开的库。如果你的标准库路径不同把第一行换成实际路径即可。做完这一步再去 VS Code 里加载带import Data.Nat的文件速度完全是两种体验。2.3 装配前后先验证 agda 本体最小加载命令不要一上来就在 VS Code 里建大文件。我习惯先在最普通的终端里做一次“冒烟测试”写一个三行的.agda文件不依赖任何标准库只检查 Agda 进程能起、能解析、能退出。# 把下面内容存成 smoke.agda # module smoke where # open import Agda.Builtin.Nat # test : Nat # test 42 # 用交互模式加载它正常的话不会有任何输出 agda --interaction smoke.agda # 终端里应该能看到 agda 进入等待状态按 CtrlD 退出这里的关键参数是--interaction。它告诉 agda 不要走普通编译流程而是进入交互会话。如果在这一步就启动失败问题基本锁定在 Agda 安装本身要么 PATH 没写对要么动态库缺失。此时不用在 VS Code 里折腾把这一层治好再回来。等这层通了再去命令面板里搜索Agda Mode: Load通常绑定 CtrlC CtrlL加载同一个文件。如果状态栏出现绿色的 loaded 提示链路就算通了。之后出现任何花式问题基本都是配置级或者源码级而不是“扩展装坏了”。3. 用 agda-mode-vscode 写完第一个带 proof 的文件加载、目标与补洞3.1 加载文件与聚焦目标CtrlC CtrlL 和 CtrlC CtrlS 的最小闭环先看一张对照表记住这四个最常用的就行其他命令都能通过命令面板搜到操作Emacs 键位agda-mode-vscode 命令面板里的名字加载文件CtrlC CtrlLAgda Mode: Load查看目标类型CtrlC CtrlD 或直接悬停Agda Mode: Goal and context (inferred)在洞口内填充表达式CtrlC CtrlSAgda Mode: Refine hole自动搜索可用的证明CtrlC CtrlAAgda Mode: Auto proof search写文件不是最后才“编译”而是写完一个模块先加载一次。比如下面这个最小定义module min where data Bool : Set where true : Bool false : Bool not : Bool → Bool not true false not false true我把光标停在not true false那一行按 CtrlC CtrlL 加载。状态栏如果显示Loaded说明定义已被接受。接着我把右侧的false删掉写成?也就是留一个 holenot : Bool → Bool not true ? not false true此时再按 CtrlC CtrlLAgda 会把?识别成目标VS Code 里通常会在那个位置显示一个高亮的 “goal” 标记旁边能看到目标类型Bool和上下文true : Bool。按 CtrlC CtrlS扩展会提示Refine你输入一个候选表达式比如这里输入false然后按回车洞就被填上且类型检查直接通过。这个闭环的意义在于有了它你不再需要先想完整答案再写。你可以把不确定的部分留成洞让 Agda 告诉你这里需要什么再把尝试填进去让类型检查器给你反馈。我的习惯是每个函数定义都先把骨架写出来匹配分支用?占位再逐个 refine而不是一次性写完再回头看错误。3.2 case split 一步一步来让类型替你把可能性列出来在写依赖类型的证明时最常遇到的情况是“不想自己枚举所有模式匹配分支”。Agda 的 case split 命令CtrlC CtrlC能根据洞所在的变量类型自动生成所有分支。以自然数加法为例最常见的写法是递归定义module add where data Nat : Set where zero : Nat suc : Nat → Nat __ : Nat → Nat → Nat m n ?光标停在?上按 CtrlC CtrlC扩展会问你要对哪个变量做 case split输入m。Agda 自动把m枚举成两个构造子生成__ : Nat → Nat → Nat zero n ? suc m n ?这里要重点看参数变化在第二个分支里类型检查器把整体变量m替换成了suc m所以递归调用的结构应该侧重m而不是n。我先填第一个分支zero n n。第二个分支先留洞加载再 refine 成suc (m n)。整个过程里case split 帮我把“模式匹配骨架”生成出来我只需要按类型填空。这也引出一个使用原则当你的证明走到某一步不知道该怎么写时先把当前变量做一次 case split多出的分支会直接告诉你需要处理哪些情况很多时候比空想快得多。3.3 让扩展帮你搜证明auto 与 refine 的差异Auto 证明搜索是 agda-mode-vscode 里最让人上头的功能。光标停在目标洞上按 CtrlC CtrlA扩展会尝试用当前上下文里的变量、以及已定义的函数组合出一个符合目标类型的项。它背后做的是穷举式搜索不是随机猜测。我经常被问它和 refine 的区别。Refine 是你给出一个候选表达式Agda 负责检查它是否与目标类型统一Auto 是你给一个问题Agda 自己去找答案。实际用法是先用refine处理 80% 的简单洞剩下的复杂目标才交给 auto。有一类情况 auto 特别好用目标类型和上下文里某个变量类型完全一致只是形式不同。比如上下文里有H : x ≡ y目标y ≡ x按 CtrlC CtrlA它很可能直接给出sym H。这类“缺一层包装函数”的洞手动写容易拼错函数名让机器搜更稳。需要注意的是auto 搜索规模会随上下文变大而变慢。如果你的洞所在函数有大量 in-scope 定义搜索可能要好几秒甚至十分钟都不一定停。我的习惯是先用普通文本写清楚类型签名、加载确认无误再开 auto如果上下文太胖就先局部where缩小搜索范围而不是放任它在整个模块里乱翻。3.4 把常用命令绑定成自己的快捷键agda-mode-vscode 提供的默认键位继承自 EmacsCtrlC 开头的组合在 VS Code 里能用但如果你不是 Emacs 老用户按起来其实别扭。所以我会把最常用的三个动作改成自己的键位在 VS Code 的keybindings.json里加绑定{ key: ctrlaltl, command: agda-mode-vscode.load, when: editorLangId agda }, { key: ctrlaltright, command: agda-mode-vscode.give, when: editorLangId agda agdaMode.active }, { key: ctrlaltenter, command: agda-mode-vscode.goal, when: editorLangId agda agdaMode.active }这三个绑定分别对应加载、填洞、查看目标。把when条件加好不影响在其他文件里的使用。我个人的血泪经验是不要一次改太多键位先改这一组用一周再慢慢调整否则你会忘了哪个键是干嘛的最后还不如用默认。想让别人帮你排错时说默认键位也比说你自定义的键位更容易沟通。4. 按项目做配置可执行路径、快捷键、unicode 输入与库管理4.1 必调的三个 settings.json 参数我把最常调的三项列成表都是我实际改过的配置项作用建议值agda-mode.moduleName指定 Agda 模块前缀你的项目名比如myprojectagda-mode.pathagda 可执行文件的绝对路径/usr/local/bin/agda或你通过which agda拿到的路径agda-mode.includeDirs告诉扩展去哪里找库源码和接口文件标准库路径写成数组例如[~/agda-stdlib/src]第一项moduleName决定你在 VS Code 里创建新文件的模块名。如果这里设置和你实际项目模块名不一致加载时会报 “module header mismatch”看起来像代码错误其实是配置文件的事。第二项path最直接Windows 下如果 agda 装在非默认目录这里没写对所有命令都会静默失败或一直转圈。第三项includeDirs影响加载 import 时的搜索路径写错的结果是明明库里文件存在却报 Not in scope 或 Failed to load interface。写配置时注意路径里的波浪号。JSON 里我遇到过不展开~的情况最稳妥的做法是写绝对路径比如/home/某开发者/agda-stdlib/src。为了少一次“路径本身写对了但扩展不认”的排查统一用绝对路径一劳永逸。4.2 用 .agda-lib 管理标准库和多个实验模块项目一多全局注册一堆库会互相污染。Agda 原生的库管理机制是.agda-lib文件agda-mode-vscode 也认它。你可以在每个项目根目录放一个这样命名的文件name: simulation-project depend: standard-library include: src然后在 VS Code 里打开src下的文件加载时 agda 会顺着这个.agda-lib找到它需要的库路径和 include 目录。这样做的好处是不同项目可以用不同版本的库互不干扰新同事拿到仓库只要 agda 装了改一下.agda-lib里库的相对路径就能跑很省事。如果项目不依赖任何库.agda-lib里只写name: xxx和include:也是可以的。我见过不少人把 include 写成绝对路径放在库里导致仓库一挪位置就全部失效。更稳的做法是.agda-lib里的路径尽量用相对路径配合项目根目录这一约定。4.3 绑定 VS Code 自己的快捷键摆脱 Emacs 肌肉记忆除了第 3 章那三个常用绑定我再补充一个和“写证明”强相关的键位建议把 case split 单独绑一个顺手的位置。在 Emacs 里是 CtrlC CtrlC但在 VS Code 里我长期被 CtrlC 与终端复制的冲突折磨。后来我把 case split 改成CtrlAltCLoad 改成CtrlAltLGive 改成CtrlAltG冲突小记忆也容易。我把这份绑定放在keybindings.json里适合大多数人的默认配置{ key: ctrlaltc, command: agda-mode-vscode.caseSplit, when: editorLangId agda agdaMode.active }, { key: ctrlaltg, command: agda-mode-vscode.give, when: editorLangId agda agdaMode.active }, { key: ctrlalta, command: agda-mode-vscode.autoProofSearch, when: editorLangId agda agdaMode.active }这样设置后你不需要记住几十个组合键只需要记住三个操作加载、给解、搜证明。其余操作一律在命令面板里搜。快捷键太多反而会掩盖“你根本没搞懂当前洞是什么状态”这个核心问题——先看上下文再决定按哪个键。4.4 用 latex 输入法写 λ、≡、∀VS Code 里的两个方案Agda 的源码里全是 unicode 符号。没有方便输入方式写两三行就开始烦躁。在 VS Code 里我用的方案有两个一是 VS Code 内置的 unicode 输入增强插件二是系统级输入法。前者更推荐因为它和语言绑定只在.agda文件里生效。以常见的输入映射为例输入\to自动变成→\lambda变成λ\equiv变成≡\forall变成∀。关键是别用中文输入法直接打这些符号否则标点会被吃掉后面写类型时经常出莫名其妙的解析错误。我遇到最典型的现象是同一行代码中文字符和 Agda 符号混在一起Agda 报解析错误只提示某个 token 位置实际却是输入法引入了一个不可见字符。如果输入法方案一直没有稳定可以退一步先写 ASCII 版本的类型签名等主体写完了再批量替换成 unicode。这个习惯不优雅但能保证你的注意力始终在证明逻辑上而不是和输入法搏斗。5. agda-mode-vscode 常见问题排查5 个我踩过的坑5.1 加载一直转圈状态栏没有任何报错现象按 CtrlC CtrlL 后界面没有反应状态栏要么没有加载完成的提示要么一直显示加载中。输出面板里也看不到明确报错。原因扩展往 agda 进程发加载命令后agda 进程根本没启动或启动后立即退出。最常见是agda-mode.path配置指错了可执行文件或 PATH 里没有 agda。解决先在终端里手动执行agda --version确认返回正常再打开设置检查agda-mode.path是否指向该可执行文件最后重启 VS Code让扩展重新读取环境变量。这三步能解决绝大多数的“转圈”问题。5.2 命令面板里搜不到任何 agda 相关命令现象CtrlShiftP 里搜 “Agda Mode”什么都出不来或者只有几个英文命令。原因扩展没有激活。agda-mode-vscode 一般按语言激活打开的文件如果不是.agda后缀或扩展在agda语言尚未注册时启动命令列表里就不会出现。解决先创建一个.agda文件确认 VS Code 右下角语言模式变成 Agda如果语言模式还是纯文本需要手动点一下右下角改成 Agda。改完再搜一次命令面板就有了。这个坑最隐蔽因为它不是“扩展坏了”而是 VS Code 的语言识别没触发。5.3 Hole 能显示但命令对它没反应现象代码里有?已经高亮显示为目标但按 CtrlC CtrlC 或 CtrlC CtrlS 都没有弹出任何交互。原因扩展不知道“当前光标在这个洞里”。agda-mode-vscode 对洞的识别依赖加载后的位置映射如果文件加载后又被外部修改比如 git 切换分支highlighter 的位置和实际文件错位交互命令就找不到洞。解决重新按 CtrlC CtrlL 让文件重新加载然后只改动洞的内容不要大规模移动代码。如果还不行关闭该文件再打开重新加载。这类问题不是逻辑错误是编辑器状态和文件状态没同步。5.4 import Data.Nat 报 “Failed to load interface”现象文件加载时报无法加载接口但标准库目录里明明有对应的.agda文件。原因标准库接口文件.agdai没生成或~/.agda/libraries里没有注册对应的.agda-lib。解决回到第 2 章的方法确认libraries和defaults文件内容正确。另一个办法是在项目里手动加.agda-lib并指定depend。如果接口文件缺失可以先进项目目录手动跑一次agda --interaction加载文件让 agda 生成缓存。注意这里不要用普通编译命令因为接口生成是加载过程的一部分。5.5 CtrlC 与终端复制冲突组合键老被吞现象按下 CtrlC CtrlL却只触发了一次复制或者焦点跳到终端面板。原因VS Code 的 CtrlC 默认是复制如果集成终端正在被使用这个键位会被终端面板捕获。agda-mode-vscode 依赖 CtrlC 系列键位但它对键位冲突没有任何提示冲突时你的命令就静默失效。解决最省事的方案是像我第 4 章那样全局改绑核心操作或者把集成终端的 send keybindings 改成不允许 CtrlC 系列透传。使用终端的频率如果很高我会直接把 agda 操作全部改到 CtrlAlt 组合键上彻底避开冲突。6. 进阶验证用加法的两个小性质检查整条链路是否真的可用6.1 一个验证路径从定义到补全证明理论知识再多都不如实际跑一个证明。我用加法结合律里的两个最小引理来验证整条链路一个能直接 refl 通过一个需要递归加 cong。把下面内容存成verify.agdamodule verify where open import Agda.Builtin.Nat __ : Nat → Nat → Nat zero n n suc m n suc (m n) plus-zero : (n : Nat) → zero n ≡ n plus-zero n refl plus-suc : (m n : Nat) → m suc n ≡ suc (m n) plus-suc zero n refl plus-suc (suc m) n cong suc (plus-suc m n)先加载整个文件。如果状态栏提示 loaded说明定义和两个证明都通过了。此时再做实验把plus-suc的第二个分支右边的cong suc (plus-suc m n)删掉留下一个洞然后试三种操作。第一种按 CtrlC CtrlA 自动搜索你会看到 Agda 靠自己找出了cong suc (plus-suc m n)这个项第二种先用 case split 展开m再逐个补洞第三种什么都不做直接写refl你会看到类型错误提示这能帮你理解为什么这里必须递归。6.2 日常最顺手的一套验证习惯我现在写新证明文件时的固定流程是先写模块头和全部 type signature不写任何 body加载一次确认签名被接受然后把 body 全部写成洞再一个一个补。每一轮都先用refl或者auto试解决不了才用 case split。这套流程帮我省掉了大量“证明写完了才发现类型签名不对”的返工。前面花大篇幅讲的配置和排错都是为了这个流程能顺畅地跑起来。等你形成了肌肉记忆手指就知道当前这个洞该按哪个命令整个过程非常自然。最后再分享一个个人习惯每次新开项目或换电脑第一天一定跑一次上面这个小验证文件确认链路、目录、缓存都是好的再开始写正式内容。这套流程已经帮我拦下了无数次“环境没配好就开始写证明”的返工希望也能帮到你。本文还有配套的精品资源点击获取