简介VS Code 上的 Agda 模式扩展面向在 VS Code 中编写 Agda 证明、函数式程序和类型驱动开发的用户尤其适合希望从 Emacs 快捷键习惯平滑迁移到现代图形界面的开发者。扩展移植了 Agda 的核心交互命令并支持语言服务器LSP可完成类型检查、加载、Goal 查看、自动补全、规范化等常见操作让 VS Code 中的 Agda 开发体验更贴近 Emacs 模式。包内共 179 个文件压缩包约 457KB文件类型涵盖 js、res、out、in、json、md、agda 等js/res 为扩展实现与 UI 资源out/in 为构建产物与输入测试数据json 存配置md 为说明文档agda 为示例源码。这些示例覆盖拆分大小写、引用标记、输入法、Issue 复现等场景可直观看出扩展如何处理不同语法与交互特性。当前已有 236 人浏览学习适合想了解 Agda 模式在 VS Code 上的实现细节、或需要定制自身 Agda 工具的开发者参考、复用并回馈改进。为什么我推荐在 VS Code 里用 agda-mode 写 AgdaAgda 这门语言对大多数写惯了 TypeScript、Python 的人来说第一眼观感就是“满屏奇怪符号”——箭头不是-而是→自然数不是decimal而是ℕ函数的输入输出之间还带一团类型定义看起来像论文草稿多于像程序。但真正上手之后就会发现Agda 的乐趣并不是“证明定理”本身而是那种“跟编译器对话、一步步把程序逼出来”的过程。这种体验极度依赖编辑器的交互能力。过去说到 Agda 编辑器大家默认就是 Emacs因为官方的主力工具 agda-mode 就是绑定在 Emacs 里的。但现在情况已经变了VS Code 上的 agda-mode 扩展已经能做到相当完整的交互式编辑、Goal 查看、case 分裂、自动补全证明而且整个 UI 对于习惯了现代编辑器的人来说上手门槛要低得多。这篇文章不打算讲深奥的类型论也不打算推销“函数式编程比命令式好”这种立场。我只想从一个日常使用者的角度把 agda-mode-vscode 的环境搭建过程以及它背后那套“交互式做证明”的工作流拆清楚、讲明白把我踩过的坑、验证过的配置、以及各种快捷键对应到 Emacs agda-mode 的哪些功能全部整理出来。如果你是第一次听说 Agda但已经装了 VS Code看完这篇应该能直接照着把环境跑起来如果你已经在 Emacs 里写 Agda想换到 VS Code 也完全没问题下面是整个迁移过程的核心操作。1. 为什么要专门给 Agda 配一个编辑器1.1 Agda 的“编程方式”和普通语言完全不同先看一段最简单的 Agda 代码module hello where data Bool : Set where true : Bool false : Bool not : Bool → Bool not true false not false true如果你只是编译运行那这段代码跟普通语言也没太大区别。但 Agda 真正的核心能力是“依赖类型 交互式证明”。也就是说你的代码里经常会出现这样的东西__ : ℕ → ℕ → ℕ zero m m suc n m suc (n m) -assoc : (a b c : ℕ) → (a b) c ≡ a (b c) -assoc zero b c ? -assoc (suc a) b c ?这里出现了一个问号?在 agda-mode 里叫hole洞。它不是注释而是“这个位置需要填代码但还没填”的意思。当你把光标放到 hole 里编辑器会告诉你当前需要证明的目标类型是什么、上下文里有哪些变量可用。这个过程跟“写业务代码”完全不同——你更像是用编译器做解题助手先在编辑器里写下类型然后逐步填充实现每填一步都检查一下。正因为这样Agda 的日常开发极度依赖编辑器与编译器的双向通信。你要么在 Emacs 里体验官方原生支持要么在 VS Code 里用社区维护的 agda-mode-vscode。二者核心机制一致本质上都是启动一个 Agda 交互进程然后编辑器向它发送请求、接收结果。1.2 对比 Emacs 和 VS Code 的 agda 工作环境我身边很多长期写 Agda 的人仍然坚持 Emacs理由也很充分官方 agda-mode 功能永远最全、支持最早、各种符号输入法比如输入\to变成→集成得最顺滑。但 Emacs 的问题同样明显配置成本高很多年轻开发者没接触过 Emacs 的操作逻辑光是学会最基本的 C-x C-s 存盘就要适应一阵子。VS Code 上的 agda-mode-vscode 是把 Emacs 里的交互协议移植到了 VS Code 的 Language Server 体系里。虽然它并不是严格意义上的 LSPLanguage Server Protocol实现而是扩展与 Agda 进程直接通信但使用体验已经很接近。优点是安装简单扩展市场搜agda-mode就能装编辑器外观现代字体、主题、Git 集成、文件树都是现成的快捷键虽然源自 Emacs但 VS Code 的命令面板可以随时查、随时改和终端、Git、Markdown 预览等工具无缝配合写证明思路也能直接在同一个窗口做笔记。当然它也有短板。最大的问题是复杂项目体积一大VS Code 版加载速度有时会明显慢于 Emacs 版还有某些 Emacs 里存在的高级命令VS Code 版还没完全覆盖。不过对大多数学习、论文复现、小规模验证项目来说功能已经够用。2. 从零开始搭建 agda-mode-vscode 环境2.1 安装 Agda 编译器本体VS Code 扩展本质上只是一个编辑器外壳真正干活的还是 Agda 编译器。编译器装不上后面一切免谈。不同平台安装方式不太一样我把常用方法列出来。macOS 下最简单的方式是 Homebrewbrew install agda装完顺手验证一下版本agda --versionLinux 下如果你的包管理器里有 Agda直接装就行比如 Ubuntusudo apt install agda如果包管理器版本太老或者想装最新版可以考虑用 Haskell Tool Stack 编译安装这条路比较“重”耗时二十分钟到一小时不等新手不建议一开始就走git clone https://github.com/agda/agda.git cd agda stack install --stack-yaml stack-8.10.7.yamlWindows 下稍微复杂一点。官方不直接分发 Windows 二进制包通用做法是先用winget install HaskellStack或从 haskellstack.org 下载 Stack然后在 MSYS2 / Git Bash 环境里通过 stack 编译安装。不过我自己在 Windows 上的经验是如果你只是现学现用优先考虑 WSL 方案在 WSL 的 Ubuntu 里跑apt install agdaVS Code 用 Remote-WSL 连接体验要稳定得多。无论哪个平台装完之后建议顺手把 Agda 标准库也装上。因为很多入门示例会用到Data.Nat、Relation.Binary.PropositionalEquality等模块。macOS 下 Homebrew 会自动顺带装标准库Linux 下需要额外装agda-stdlib包WSL 里就是sudo apt install agda-stdlib标准库装好后要给 Agda 注册库位置在用户目录下创建或编辑~/.agda/libraries ~/.agda/defaultslibraries文件里写入标准库.agda-lib文件的绝对路径defaults文件里写standard-library。两个文件都要。这一步漏了的话你的文件里import Data.Nat就会报找不到模块。2.2 安装并配置 VS Code 扩展打开 VS Code扩展面板搜索agda-mode认准发布者banacorn的扩展并安装。装完之后扩展会自动去 PATH 里找agda可执行文件。万一找不到你需要手动指定路径。在 VS Code 的 settings.json 里加{ agda-mode.executable: /path/to/agda }注意这个配置项名字在不同版本里可能略有差异老版本叫agda.executable新版本叫agda-mode.executable。改完重启 VS Code 即可。另外强烈建议把下面这两个配置也做了{ agda-mode.loadOnOpen: true, agda-mode.unicodeInputMethod: true }loadOnOpen会在你打开.agda文件时自动加载省去每次手动按快捷键的麻烦。unicodeInputMethod提供了 Emacs agda-mode 经典的 Unicode 输入支持——输入\to会提示转换为→输入\bN得到ℕ。如果你经常写 Agda这个功能能省掉大量复制粘贴特殊字符的时间。2.3 验证环境是否跑通新建一个文件hello.agda输入我开头那段 Bool 定义的代码然后按下CtrlC CtrlL加载文件。如果一切正常VS Code 底部或右侧会弹出 Agda 的信息提示代码里的 Unicode 符号会正常渲染文件路径旁边不会出现红色错误标记。如果快捷键按下没反应先用命令面板CtrlShiftP输入Agda看看相关命令是否出现确认扩展确实被激活了。加载成功之后再把光标放到not true false这行上按CtrlC CtrlT可以查看当前表达式的类型按CtrlC Ctrl,可以查看上下文信息。能看到这些反馈就说明 vs code 和 agda 编译器之间的通道已经打通可以开始真正的交互式开发了。3. 快速上手 agda-mode 的五个核心操作3.1 C-c C-l加载文件与查看 Goal加载文件是所有操作的起点。无论你改了什么都要先加载一遍让 Agda 重新检查。加载之后如果存在 hole即?位置编辑器会突出显示并将光标移到对应位置。把光标放到 hole 里面按CtrlC Ctrl,可以看到当前 Goal 的类型也就是“此处需要的表达式应该长成什么样”。加载这个动作看起来简单但背后做的事情其实不少。Agda 会解析整个文件进行类型检查并根据你当前光标的位置维护一份交互状态。文件越大、依赖的库越多加载时间越长。我建议在写文件头部时就把所有import先写全否则后面每次加载都要因为新增 import 重来一遍。VS Code 版有个小优势窗口下方的输出区会显示 Agda 加载过程的日志。如果文件加载出错你能直接看到是哪个模块找不到还是哪个类型不匹配不用像在 Emacs 里那样弹个独立 buffer来回切比较费眼。3.2 C-c C-c对变量做 case split这是 Agda 日常开发里最高频的操作缩写来自 Emacs 的case。假设你写了一个函数plus : ℕ → ℕ → ℕ plus n m ?光标放在 hole 里按下CtrlC CtrlC扩展会问你“split on which variable?”输入n回车整个定义会变成plus : ℕ → ℕ → ℕ plus zero m ? plus (suc n) m ?也就是说case split 会自动帮你按变量的构造函数展开分情况讨论变量名也被统一重命名。这一步的意义在于在写依赖类型的代码时模式匹配的“分情况讨论”往往是证明的关键步骤手工写很容易因为变量顺序、重名等细节出错而编辑器帮你生成能减少大量无谓的报错。如果你是第一接触可能会觉得“这不就是自动补全吗”。但它在 Agda 里真正的威力是当你对suc n展开后Agda 会自动在上下文里把n变成可用的归纳假设后续证明可以直接引用。3.3 C-c C-rrefine 自动填充初步结构refine 操作也经常用。它的作用是当前 Goal 是一个函数类型或者归纳类型你按CtrlC CtrlRAgda 会帮你把外层构造器或函数应用先填出来剩下的子表达式继续留成 hole。举一个具体例子。你要证明加法结合律-assoc : (a b c : ℕ) → (a b) c ≡ a (b c) -assoc zero b c ?光标放在 hole 上按CtrlC CtrlRAgda 会把右边的?替换成某种“显然由定义出发可以化简”的形式实际上往往直接变成refl而在-assoc (suc a) b c那个分支里refine 会识别出目标是一个suc开头的等式自动帮你写成cong suc ?把suc提取到外面剩下一个更小的 Goal。这种“剥洋葱”式的证明体验只有在交互式编辑器里才能感受到。3.4 C-c C-a自动搜索证明最后是最省事的操作CtrlC CtrlA让 Agda 自动在上下文中搜索是否有符合当前 Goal 类型的表达式。如果找到了可能是已有的函数、引理、公理它会把表达式填到 hole 里并继续检查剩余的子目标。自动搜索的能力有限它不会做复杂推导只能根据类型签名做匹配所以不要指望它能证明一切。但在简单情形下它真的能一步完成比如加法结合律的zero分支按完C-c C-a直接出refl。我通常的流程是先 case split再 refine最后用 auto 处理那些机械的、显然成立的子目标剩下的难啃的骨头才手写证明项。3.5 C-c C-Spacegive把 hole 内容提交这个操作在 Emacs agda-mode 里的名字叫 “Give”。你手动在 hole 里填了表达式之后用CtrlC CtrlSpace提交并检查当前 hole 是否通过类型检查。如果通过了?会被正式替换成你填的内容如果类型不对扩展会给出错误提示。很多人新手阶段容易犯一个错误直接在 hole 里写上一大串证明项然后按加载C-c C-l发现报错又不知道具体错在哪儿。我建议养成一个习惯在 hole 里写完一小步就C-c C-Space验证一次不要一次性憋一大段。特别是证明代码一个括号位置不对就让人抓狂分步提交能把问题定位到最小范围。4. 实战从零写一个可运行的证明文件4.1 准备项目与引入标准库为了演示一整套工作流我们做一个最小但完整的项目。目标是证明a 0 ≡ a在 Peano 自然数体系里zero m的定义可以直接化简但suc n 0需要递归论证。新建一个文件比如plus-zero.agda输入以下内容module plus-zero where open import Data.Nat using (ℕ; zero; suc) open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong) 0 : (a : ℕ) → a 0 ≡ a 0 zero ? 0 (suc a) ?这里Data.Nat提供ℕ与__的定义_≡_是相等类型refl对应自反性。如果你已经按前面步骤配置好了标准库加载这个文件应该是没有报错的只会在两个?处出现 Goal 提示。4.2 用 hole、refine 和 auto 完成证明先把光标放到第一个 hole0 zero ?上按CtrlC Ctrl,看到 GoalGoal: zero 0 ≡ zero这个式子为什么正确因为__的第一个参数是zero定义就是zero m m所以zero 0会化简成0即zero。这就意味着整个等式左右两边定义相等可以直接用refl。对着 hole 按CtrlC CtrlAAgda 搜索到refl自动填入。第二个分支光标放到?上先按CtrlC CtrlC要求 case split此时因为变量已经单参数扩展会自动按suc a拆分得到0 zero refl 0 (suc a) ?再看 GoalGoal: suc a 0 ≡ suc a__的定义是suc n m suc (n m)所以suc a 0展开成suc (a 0)。此时 Goal 的形状是suc (a 0) ≡ suc a说明只要证明a 0 ≡ a再用cong suc套一层就能完成。按CtrlC CtrlRAgda 会识别出右侧是一个以suc构造器开头的等式自动把代码补成0 zero refl 0 (suc a) cong suc (0 a)等一下第二步 refine 后就剩一个 hole即0 a这个位置你可能会想继续按但这里其实已经可以直接交掉。因为0 a : a 0 ≡ a的类型恰好就是我们的归纳假设也就是说 Agda 在上下文里能看到0 a而你刚刚用 refine 生成的表达式里已经自动引用了它。所以直接按CtrlC CtrlSpace提交整个文件检查通过。最终代码module plus-zero where open import Data.Nat using (ℕ; zero; suc) open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong) 0 : (a : ℕ) → a 0 ≡ a 0 zero refl 0 (suc a) cong suc (0 a)这整段过程不会超过两三分钟但你已经体验到了 agda-mode 的核心循环模式加载 - 查看 Goal - case split - refine - auto - give。所有复杂证明本质上都是把目标不断拆小直到每个子目标都能用refl或已有引理结束。4.3 保存加载与常见输出解读写完后按CtrlC CtrlL重新加载。如果代码正确左下角会显示类似 “All Done” 的提示且输出面板没有错误日志。如果某一步类型不匹配VS Code 会在打开的文件中用波浪线标出错误位置鼠标悬停能看到完整错误信息。最常见的错误有两类一是 “a ! b” 类型不匹配通常意味着你填的表达式 Church 化不对二是 “variable not in scope”通常来自 import 没写全或拼写错误。遇到后按错误提示、回到对应 hole重新 refine 或手写补齐即可。5. 六个高频问题与对应的排查方案5.1 扩展提示找不到 agda 可执行文件这是最常遇见的安装问题。现象是加载文件时报 “Cannot find Agda executable” 或者直接没反应。排查顺序记住三步在终端手动跑agda --version看能不能输出版本号如果不能说明编译器没装好或不在 PATH 里先解决 Agda 安装如果终端能跑但扩展还是找不到说明 VS Code 的 PATH 环境与终端不一致。这时候打开 settings.json设置绝对路径agda-mode.executable。macOS 下特别容易踩这个坑因为 VS Code 在 Finder 里启动时不会加载 shell 的 PATH 配置Homebrew 安装路径又在/opt/homebrew/bin需要在设置里显式写出来。这个坑我帮同事排查过至少三次。5.2 加载成功但 Unicode 符号显示为方框如果代码里的→、ℕ、≡等在编辑器中显示成方框、问号或者豆腐块通常是字体不支持这些字符。需要在 VS Code 设置里配置一个支持广泛 Unicode 的字体。我个人推荐在editor.fontFamily里把Source Code Pro或JetBrains Mono放前面同时加上Segoe UI Symbol、Noto Sans Symbols2作为 fallback{ editor.fontFamily: JetBrains Mono, Noto Sans Symbols2, Segoe UI Symbol, monospace }如果设置了还是显示不正常可以安装专门的 Agda 字体把 Agda 源码仓库里的Agda.ttf安装到系统字体目录再用 VS Code 手动选择。5.3 C-c 快捷键与中文输入法冲突Windows 下如果你使用微软拼音等中文输入法CtrlC CtrlL这类组合键有时会被输入法拦截导致 Agda 命令不生效。我实测有效的解法是在输入法设置里取消“使用 Ctrl 键切换中英文”或“Shift 切换”相关的快捷键绑定或者索性在写 Agda 时切换到英文输入状态。macOS 下一般没有这个问题但如果你用第三方输入法比如搜狗同样可以在输入法设置里关闭 Ctrl 组合键。另一个思路是把 agda-mode 的常用命令绑定到 VS Code 的其他按键上。比如在 keybindings.json 里把加载文件绑定为CtrlShiftLcase split 绑定为CtrlI等。命令名可以在命令面板里搜 “Agda” 查到改完之后就不需要依赖原始的 Emacs 风格快捷键了。5.4 大文件加载卡顿、CPU 飙高Agda 的类型检查严格且计算开销大项目一大加载慢是正常的不一定是扩展问题。我个人的优化经验是尽量把大项目拆成多个小模块按依赖关系分层不要一个几千行的单文件写完用{-# OPTIONS --no-positivity-check #-}之类的编译选项要慎用并不是说禁用检查会对而是它可能掩盖问题加载时不要频繁连续按C-c C-l等一次加载完成再改下一处否则会让 Agda 进程排队多个检查请求反而更慢如果确需修改多处可以考虑先把文件里所有 hole 临时替换成postulate加载速度会快很多最后再逐个填证明。5.5 打开多个 .agda 文件导致状态混乱Agda 交互进程按文件维护状态。如果你在同一个窗口同时打开多个.agda文件切换加载不同文件时偶尔会出现加载了 A 文件却反馈 B 文件错误的情况。我的习惯是一个窗口只保留一个在进行中的 Agda 项目其他参考文件要么放另一个窗口要么只读打开。了避免状态污染改完一个文件加载通过后再打开下一个文件前可以按一下CtrlShiftP执行 “Agda: Clear” 清空久状态。5.6 需要输入特殊符号但不知道写法这是新手最容易卡住的地方。Emacs 的 agda-mode 里输入\to会出现→\bN会出现ℕ。VS Code 版同样内置了这个输入法前提是你开启了agda-mode.unicodeInputMethod。你可以在某个.agda文件里直接输入\开头的命令块扩展会弹出补全菜单列出所有可用的符号与对应输入写法。如果你开着这个功能但没反应请检查是否和其他扩展的补全冲突极端情况下可以禁用其他补全类扩展再试。6. 写在最后的一点经验用 agda-mode-vscode 写了一个学期的 Agda 之后我最大的感受是编辑器选型真的会影响你愿意不愿意继续学这门语言。Emacs 很好但如果你本来就是 VS Code 用户完全没必要为了 Agda 去重复学习一套全新的编辑器。VS Code 上的 agda-mode 虽然还没到 100% 还原 Emacs 版的程度日常做练习、读论文代码、验证算法性质已经绰绰有余了。几个实用的小建议放在最后。把CtrlC CtrlL和CtrlC CtrlSpace这两个快捷键先练到肌肉记忆它们是你和 Agda 编译器之间最频繁的交互。再就是写 Agda 文件时尽量每段证明都配一个注释说明自己在证什么因为点缀在定理代码里的 Unicode 符号很容易让人三天之后就看不懂自己当初的意图。最后随时打开命令面板搜 “Agda”你能看到全部功能的入口——很多时候不是扩展没有某个功能而是你还没找到那个命令叫什么名字。本文还有配套的精品资源点击获取