简介：这份资源是面向 Agda 语言开发者与函数式编程学习者的 VS Code 扩展包，用于在 VS Code 中提供 agda-mode 支持，解决 Agda 代码编辑、加载与类型推断等交互需求。包内共 179 个文件，以 67 个 js 与 64 个 res 源码文件为主体，辅以 13 个 out 与 13 个 in 测试用例、5 个 json 配置、4 个 md 说明文档及 4 个 agda 示例文件，另有 less、yml、ttf 字体等资源，压缩包约 457KB，结构紧凑。扩展支持通过 Cc Cl 等快捷键加载 Agda 文件，并可在语言服务器模式下于面板右上角显示 LSP 标识；针对类型相关命令，还提供了归一化级别与 Cu、Cy 前缀的按键映射方案，方便从 Emacs 迁移的用户快速上手。目前已有 238 人学习关注，适合希望在日常编辑器中获得 Agda 交互体验、并愿意参与反馈与改进的开发者参考使用。
1. 在 VS Code 里写证明：agda-mode-vscode 到底解决了什么
如果你写过 Agda，大概率经历过这种分裂：一边是终端里agda --interactive的 REPL，一边是编辑器里满屏的黄色高亮和看不懂的?。Agda 的交互式证明开发极度依赖编辑器反馈——归一化、类型检查、case split、自动填充，这些操作在终端里敲命令能把自己敲崩溃。agda-mode-vscode 就是把这个交互层搬进 VS Code 的扩展，让你在写.agda文件时直接调用 Agda 的交互命令，不用在编辑器和终端之间反复横跳。
这个扩展适合两类人：一是从 Emacs 的 agda-mode 迁移过来、但不想继续折腾 Emacs 配置的开发者；二是用 VS Code 做主力编辑器、想在一个窗口里完成 Agda 证明开发的从业者。它本质上是一个语言客户端，把 VS Code 的编辑器能力（补全、跳转、诊断）和 Agda 的交互命令（C-c C-l加载、C-c C-ccase split、C-c C-rrefine）对接起来。关键词里的 vscode-extension、agda-mode 是它的身份标签，而 reasonml、ReScript 出现在热词里，多半是因为它们同属「编辑器语言工具链」这个检索语境，实际和 Agda 没有直接关系，后面不再展开。
2. 环境搭建：从 Agda 可执行文件到扩展激活
2.1 先确认 Agda 本体能跑起来
扩展只是壳，真正做类型检查和归一化的是 Agda 本体。所以第一步不是装扩展，而是确认agda命令在终端里可用。常见做法是用包管理器装，比如在 macOS 上brew install agda，在 Linux 上用cabal install agda或发行版仓库。装完先跑一条命令验证：
# 查看 Agda 版本，确认可执行文件在 PATH 里 agda --version # 预期输出类似：Agda version 2.6.4 # 如果报 command not found，说明 PATH 没配好，先解决这个再往下走这一步的逻辑很简单：扩展启动时会去调agda这个可执行文件，如果系统找不到它，扩展会报「Agda executable not found」。参数上没什么可调的，关键是版本——Agda 2.6.x 和 2.7.x 在标准库接口上有差异，扩展本身对版本不敏感，但你的项目代码会敏感。我一般会先确认项目用的标准库版本，再决定装哪个 Agda。
2.2 安装扩展并配置可执行文件路径
在 VS Code 扩展市场搜agda-mode或agda，找到对应扩展安装。装完后如果agda不在默认 PATH 里（比如用 cabal 装在~/.cabal/bin），需要在 VS Code 设置里指定路径。打开settings.json：
{ // 指向 Agda 可执行文件的绝对路径 "agdaMode.agdaPath": "/Users/yourname/.cabal/bin/agda", // 传给 Agda 的额外参数，比如指定标准库路径 "agdaMode.agdaArgs": ["-i", "/path/to/agda-stdlib/src"], // 是否在打开 .agda 文件时自动加载 "agdaMode.autoLoad": true }agdaPath是最容易翻车的地方：路径里带空格、用了~而不是绝对路径、或者指向了一个 shell 脚本而不是二进制，都会导致扩展启动失败。agdaArgs里的-i是 include 路径，Agda 找import的模块时按这个顺序搜。如果你项目里用了--cubical之类的 flag，也要在这里加上，否则扩展加载时用的编译选项和命令行不一致，会出现「命令行能过、编辑器报错」的玄学问题。
2.3 验证交互命令是否生效
打开一个.agda文件，按C-c C-l（Ctrl+C 然后 Ctrl+L）触发加载。如果配置正确，底部状态栏会显示 Agda 的加载进度，文件里的?会变成 goal 编号，类型检查错误会以诊断形式标红。这一步是分水岭：能加载说明扩展和 Agda 本体已经握手成功，剩下的就是交互命令的使用问题。
3. 核心交互命令：把证明开发拆成可复现的操作
3.1 加载、归一化与类型检查
Agda 的开发循环是「写洞 → 加载 → 看目标类型 → 填充 → 再加载」。C-c C-l是加载，等价于命令行的agda --interactive里敲load。加载后光标停在?上，底部会显示当前 goal 的类型和上下文。归一化用C-c C-n，输入一个表达式，Agda 会算出它的范式——这在调试refl为什么过不了的时候特别有用，因为你能看到 Agda 眼里的表达式到底长什么样。
-- 一个典型的开发中间态 add-zero : (n : ℕ) → n + zero ≡ n add-zero n = ? -- 光标放在 ? 上按 C-c C-l，底部显示 Goal: n + zero ≡ n -- 再按 C-c C-c（case split）对 n 做分类讨论C-c C-c是 case split，对变量做模式匹配。它的参数是变量名，Agda 会根据数据类型自动展开所有构造子。这里有个坑：如果变量在上下文里被依赖类型约束过，case split 可能生成一堆看起来重复的分支，需要手动合并。C-c C-r是 refine，用当前上下文里类型匹配的构造子或函数去填充 goal，能省掉大量手敲。
3.2 用 Emacs 风格的键位在 VS Code 里操作
扩展默认沿用 Emacs agda-mode 的键位，这对从 Emacs 迁移的人是好事，对纯 VS Code 用户是门槛。C-c前缀意味着你要先按 Ctrl+C，松开，再按下一个键。VS Code 的键位绑定里可以改，但我不建议大改——Agda 社区的文档和教程全是这套键位，改了之后看文档会对不上。常见做法是保留默认，只把最常用的几个映射到更顺手的位置：
// keybindings.json 里覆盖个别命令 [ { "key": "ctrl+alt+l", "command": "agdaMode.load", "when": "editorLangId == agda" }, { "key": "ctrl+alt+c", "command": "agdaMode.caseSplit", "when": "editorLangId == agda" } ]when条件是必须的，否则这些键位会污染其他语言的编辑体验。agdaMode.load和agdaMode.caseSplit是扩展注册的命令 ID，可以在命令面板里搜到。改键位之后要重新加载窗口才生效，这是 VS Code 扩展的通用行为，不是这个扩展的 bug。
3.3 处理 goal 与上下文信息
Agda 的 goal 信息显示在底部面板，但 VS Code 的面板空间有限，长上下文会被截断。我一般会把agdaMode.goalDisplay设成hover或both，这样鼠标悬停在?上也能看到类型。如果上下文变量太多，可以用C-c C-,（Ctrl+C 然后逗号）单独查看 goal 和上下文，这个命令会把信息输出到一个临时窗口，比底部面板完整。
{ // goal 信息显示方式：panel / hover / both "agdaMode.goalDisplay": "both", // 是否在 goal 里显示归一化后的类型 "agdaMode.normalizeGoal": true }normalizeGoal打开后，goal 类型会先归一化再显示，好处是能看到n + zero被算成n，坏处是某些情况下归一化会卡住（比如涉及大量计算的项），这时候关掉它反而更快。这是个权衡参数，没有标准答案。
4. 避坑与排查：那些让扩展「看起来坏了」的瞬间
4.1 扩展报「Agda executable not found」
现象是打开.agda文件后状态栏一直显示未连接，命令面板里执行加载没反应。原因通常是agdaPath没配、配错，或者 VS Code 启动时的环境变量和终端不一致——macOS 上从 Dock 启动的 VS Code 不继承 shell 的 PATH，这是血泪经验。解决办法是在settings.json里写绝对路径，或者用launchctl setenv把 PATH 注入到 GUI 环境。验证方法是打开 VS Code 的集成终端跑which agda，如果这里能找到但扩展找不到，就是环境变量继承问题。
4.2 加载成功但 goal 不显示
现象是C-c C-l后文件变绿（无错误），但?没有变成 goal 编号，底部也没有类型信息。原因多半是文件里没有?或者?在注释里。Agda 只把真正的 hole 当作 goal，字符串或注释里的问号不算。另一个可能是扩展的 goal 显示被关了，检查agdaMode.goalDisplay是不是设成了none。解决方法是确认 hole 语法正确，然后重启扩展（命令面板执行Developer: Reload Window）。
4.3 case split 生成的分支无法通过类型检查
现象是C-c C-c对变量做 split 后，某些分支报类型错误，但手动写同样的模式匹配却能过。原因是 case split 生成的分支顺序和依赖类型的具体化方式可能和手写不同，尤其是涉及Vec、Fin这类索引类型时。解决办法是不要盲目信任自动生成的分支，逐个检查 goal 类型，必要时手动调整分支顺序或加rewrite。我一般会在 split 之后立刻C-c C-l重新加载，看哪些分支还有洞，而不是直接往下写。
4.4 标准库 import 报错但命令行能过
现象是编辑器里import Data.Nat标红，但终端里agda编译同一个文件没问题。原因是扩展用的 include 路径和命令行不一致。命令行的agda可能读了~/.agda/libraries和~/.agda/defaults，而扩展启动时的工作目录不同，导致相对路径解析失败。解决办法是在agdaMode.agdaArgs里显式加-i指向标准库的src目录，或者确保 VS Code 打开的是项目根目录而不是单个文件。
4.5 大文件加载慢到怀疑人生
现象是几千行的.agda文件每次C-c C-l都要等十几秒甚至更久。原因是 Agda 的类型检查是全局的，改一个洞可能触发大量重新检查。这不是扩展的锅，是 Agda 本身的工作方式。缓解办法是把大文件拆成多个模块，用import隔离；或者在开发时用--no-termination-check之类的 flag 跳过部分检查（仅限调试，别提交）。扩展层面能做的有限，agdaMode.autoLoad设成false可以避免每次打开文件都自动加载。
5. 进阶技巧：把交互命令串成肌肉记忆
用熟之后，Agda 开发的速度瓶颈不在打字，而在「想清楚下一步做什么」。扩展提供的命令本质上是一组对证明状态的查询和变换，真正高效的做法是把它们串成固定节奏。我自己的循环是：C-c C-l加载看所有 goal → 对第一个 goal 按C-c C-c或C-c C-r→ 立刻C-c C-l确认没引入新错误 → 移到下一个 goal。这个循环里C-c C-l出现的频率极高，所以我把加载键位改到了左手小指能碰到的地方，减少手部移动。
另一个技巧是用C-c C-n做「表达式探针」。当你不确定某个项归一化后长什么样，不要靠脑补，直接归一化它。比如证明Vec的map和++的分配律时，归一化map f (xs ++ ys)和map f xs ++ map f ys能立刻看出它们是否 definitionally equal。如果是，refl就够；如果不是，你需要引理。这个判断用眼睛看比用脑子想快得多。
验证扩展是否正常工作，我一般会准备一个最小.agda文件作为冒烟测试：
module SmokeTest where open import Data.Nat using (ℕ; zero; suc; _+_) open import Relation.Binary.PropositionalEquality using (_≡_; refl) -- 这个证明应该能通过 C-c C-c 和 C-c C-r 自动完成 +-identity : (n : ℕ) → n + zero ≡ n +-identity zero = refl +-identity (suc n) = cong suc (+-identity n)如果这个文件能加载、能 case split、能 refine，说明扩展的核心链路是通的。剩下的就是 Agda 本身的证明问题了。
从那以后我每次配新环境，都强制先跑一遍这个冒烟测试，确认扩展和 Agda 本体握手成功再开始写真正的证明。希望帮到你。
本文还有配套的精品资源，点击获取
