简介：这份资源是面向 Agda 语言开发者与函数式编程学习者的 VS Code 扩展包，用于在 VS Code 中提供 agda-mode 支持，解决 Agda 代码编辑、加载与类型推断等交互需求。包内共 179 个文件，以 67 个 js 与 64 个 res 文件为主，分别承担扩展逻辑与 ReScript 源码实现，另含 13 个 out、13 个 in 测试用例、5 个 json 配置、4 个 agda 示例文件及 less、yml、ttf 等样式与资源文件，压缩包约 457KB，结构紧凑。扩展支持通过 Cc Cl 等组合键加载 Agda 文件，并针对类型相关命令提供不同规范化级别，用 Cu、Cy 前缀替代 Emacs 中的 Cu、Cu Cu 操作；同时内置仍处开发阶段的 Agda 语言服务器，启用后可在面板右上角看到 LSP 标识。已有 238 人学习关注，适合希望脱离 Emacs、在 VS Code 中完成 Agda 日常开发与调试的读者参考使用。
1. 装 agda-mode-vscode 前，先把 Agda 本体和版本对齐
Agda 在 VS Code 里的体验，八成取决于一件跟插件本身无关的事：你机器上的 Agda 可执行文件是哪个版本、装在哪、VS Code 能不能找到它。我见过太多人插件装完，打开.agda文件一片红，第一反应是插件坏了，其实是agda命令压根没进 PATH，或者版本和插件要求的语言协议对不上。agda-mode-vscode 这个扩展本质是个前端，它负责把 Agda 的交互式会话翻译成 VS Code 里的高亮、目标显示、case 拆分这些操作，真正的类型检查和求值全在 Agda 本体里跑。所以这套环境适合两类人：一类是刚接触依赖类型、想用 Agda 写证明的开发者，另一类是原来在 Emacs 里用 agda-mode、想换到 VS Code 但被配置卡住的人。装不好不会报一个漂亮的错，而是各种「命令无响应」「文件类型不识别」「目标窗口空白」，排查起来很玄学。这一篇就按我实际装机的顺序，从版本选择一路写到跑通第一个交互命令。
2. 环境准备：Agda 本体、VS Code 与扩展的版本取舍
2.1 先定 Agda 版本，再谈插件
agda-mode-vscode 对 Agda 本体有版本要求，这不是插件挑剔，而是 Agda 的交互协议（内部叫 IOTCM 那套）在不同大版本间会变。我一般会先确认要用的 Agda 版本，再回头装插件，顺序反了容易白折腾。
常见做法是用包管理器装 Agda，而不是自己从源码编译。原因很直接：Agda 依赖 GHC 和一堆 Haskell 库，源码编译一次少则十几分钟多则半小时，出错了还得清缓存重来。用包管理器能省掉依赖地狱。
# 以常见的 Haskell 工具链为例，先确认 GHC 和 cabal 可用 ghc --version cabal --version # 用 cabal 安装指定版本的 Agda（版本号按你项目需要改） cabal update cabal install Agda-2.6.4 # 装完确认可执行文件位置 which agda agda --version这里几个点要说清楚。cabal update是刷新包索引，不刷新可能装到旧版本。cabal install Agda-2.6.4里的版本号是硬约束，写Agda不带版本会拿最新版，最新版未必和你的插件兼容。which agda用来确认它进了 PATH，如果这条命令没输出，后面 VS Code 一定找不到它。agda --version是最终确认，输出里会带版本号和编译用的 GHC 版本。
如果你用的是系统包管理器（比如某些 Linux 发行版的包源），版本往往偏旧，可能低到插件不支持。这种情况我建议还是走 cabal 或 stack，别图省事。
2.2 VS Code 与扩展的安装
VS Code 本身版本不用太新，近一两年的稳定版都行。扩展安装有两条路：图形界面里搜agda-mode-vscode，或者命令行装。
# 命令行安装扩展，扩展 ID 以市场实际为准 code --install-extension banacorn.agda-mode # 列出已装扩展，确认装上了 code --list-extensions | grep -i agdacode --install-extension后面跟的是扩展的完整 ID，格式是发布者.扩展名。装完用--list-extensions过滤一下，能看到就说明扩展本体到位了。这一步和 Agda 本体是两回事，扩展装上了不代表 Agda 能用，别混淆。
2.3 让 VS Code 找到 Agda 可执行文件
这是翻车率最高的一环。VS Code 从图形界面启动时，继承的环境变量和你终端里的可能不一样，终端里which agda有输出，VS Code 里就是找不到。
我一般会在 VS Code 的设置里显式指定 Agda 路径。打开settings.json，加一行：
{ // 指向 agda 可执行文件的绝对路径，按你机器实际位置改 "agdaMode.connection.agdaPath": "/home/yourname/.cabal/bin/agda" }agdaMode.connection.agdaPath这个键就是告诉扩展去哪找 Agda。值必须是绝对路径，写agda这种相对命令在部分环境下不生效。Windows 上路径要写成C:\\Users\\...\\agda.exe这种转义形式。改完重启 VS Code，让设置生效。
提示：不确定 Agda 装哪了，在终端跑
which agda（Linux/macOS）或where agda（Windows），把输出原样填进去。
3. 配置 agda-mode-vscode：语言识别、交互命令与参数
3.1 确认文件类型被正确识别
Agda 源文件后缀是.agda，但 VS Code 默认不一定把它关联到这个扩展。打开一个.agda文件，看右下角语言模式是不是Agda。如果不是，点一下手动选，或者直接在设置里绑死：
{ // 把 .agda 后缀强制关联到 agda 语言 "files.associations": { "*.agda": "agda" } }files.associations是 VS Code 通用的文件关联配置，键是 glob 模式，值是语言 ID。这里语言 ID 必须是agda，写错了扩展不会接管，高亮和命令都不会出现。这一步做完，重新打开文件，语法高亮应该就正常了。
3.2 交互命令怎么触发
agda-mode-vscode 的核心价值是把 Agda 的交互式开发搬进编辑器。常用命令包括加载文件、显示目标、case 拆分、求值等。这些命令默认绑了快捷键，也可以从命令面板调。
{ // 自定义快捷键示例：Ctrl+Alt+L 加载当前文件 "keybindings": [ { "key": "ctrl+alt+l", "command": "agdaMode.load", "when": "editorLangId == agda" } ] }command字段对应扩展注册的命令 ID，agdaMode.load是加载文件。when条件是关键，editorLangId == agda保证只在 Agda 文件里生效，不然会污染其他语言的快捷键。命令 ID 以扩展实际注册的为准，不同版本可能有差异，拿不准就去命令面板搜Agda看真实名字。
3.3 关键参数：连接方式与超时
扩展和 Agda 之间是进程通信，有几个参数影响稳定性。
{ // Agda 交互进程的启动参数 "agdaMode.connection.agdaArgs": ["--interaction"], // 命令超时时间，单位毫秒，大项目加载慢可以调大 "agdaMode.connection.timeout": 30000 }agdaArgs是传给 Agda 本体的启动参数，--interaction表示进入交互模式，这是扩展正常工作的前提，一般不用改。timeout控制单条命令等待多久算超时，默认值对中小项目够用，但如果你在跑一个依赖很多、类型检查很重的文件，加载可能超过默认时间，表现就是「命令一直转圈然后失败」。这种情况把值调到 60000 甚至更大，比反复重装插件有用。
注意：改完这些设置一定要重启 VS Code 窗口（不是只关文件），进程通信参数在窗口启动时读取。
4. 避坑与排查：agda-mode-vscode 装完不工作的常见原因
4.1 现象：打开 .agda 文件没有任何高亮，命令面板搜不到 Agda 命令
原因基本是文件没被识别成 agda 语言，或者扩展没启用。先看右下角语言模式，再去看扩展面板里 agda-mode-vscode 是不是被禁用了。解决就是按 3.1 配files.associations，并在扩展面板确认它是启用状态。有时候是工作区级别禁用了扩展，检查一下工作区的.vscode/settings.json有没有覆盖。
4.2 现象：命令能触发，但报「Agda not found」或类似找不到可执行文件
这是 PATH 问题，不是插件问题。原因在 2.3 说过，VS Code 的启动环境和终端不一致。解决就是在设置里显式写agdaMode.connection.agdaPath绝对路径。写完重启窗口。如果还不行，在 VS Code 内置终端里跑一次agda --version，内置终端继承的是 VS Code 的环境，它要是也找不到，说明路径确实没配对。
4.3 现象：加载文件卡住，最后超时失败
两种可能。一是文件本身类型检查就慢，依赖多、证明复杂，这种调大timeout。二是 Agda 版本和插件协议不匹配，表现是进程起来了但握手失败。确认方法是在终端手动跑agda --interaction，看它能不能正常启动并等待输入。如果手动跑也异常，问题在 Agda 本体，回去检查版本。
4.4 现象：目标显示窗口空白，或者 case 拆分结果不对
这类问题多半是 Agda 版本和插件版本组合不匹配。Agda 的交互输出格式在小版本间也可能微调，插件解析不了就显示空白。我一般会去扩展的说明里看它声明支持的 Agda 版本范围，把本体降到范围内。别硬扛最新版，稳定组合比追新重要。
4.5 现象：改了设置没生效
VS Code 的设置分用户级和工作区级，工作区级会覆盖用户级。如果你在用户设置里改了agdaPath但工作区里有另一份设置，以工作区为准。排查时打开命令面板搜Open Workspace Settings，看看有没有冲突项。另外进程类设置必须重启窗口，只重载文件不够。
5. 验证跑通：用一个最小文件确认整条链路
装完不验证，等于没装。我习惯用一个最小 Agda 文件把「加载 → 类型检查 → 交互」这条链路走一遍，任何一环断了都能立刻定位。
新建一个Hello.agda：
-- 最小验证文件：定义一个简单类型和一个值 module Hello where -- 声明一个自然数类型的数据定义 data Nat : Set where zero : Nat suc : Nat → Nat -- 定义一个加法函数，用来触发类型检查 _+_ : Nat → Nat → Nat zero + m = m suc n + m = suc (n + m) -- 一个具体表达式，方便在编辑器里求值 two : Nat two = suc (suc zero)保存后，用 3.2 里配的加载命令（或命令面板搜Agda: Load）加载这个文件。判断跑通看三个信号：第一，文件没有红色错误波浪线，说明类型检查通过；第二，把光标放在two上触发「显示目标」类命令，能看到它的类型是Nat；第三，在文件里选中two + two这样的表达式触发求值，能得到suc (suc (suc (suc zero)))这种规范化结果。
如果这三步都过，说明 Agda 本体、扩展、路径配置、交互协议整条链路是通的。任何一步不过，回到第 4 章按现象对号入座，比盲目重装高效得多。
我还会额外确认一件事：关掉 VS Code 再重新打开，重复一次加载。因为有些路径问题只在冷启动时暴露，热重载看不出来。这一步能过滤掉「当前会话能用、下次打开又坏」的假成功。
从那以后我每次装完 agda-mode-vscode，都强制走一遍这个最小文件的加载和求值，不看到two + two算出结果不算装完。希望帮到你。
本文还有配套的精品资源，点击获取
