简介这份资源是面向 Agda 依赖类型语言使用者的 VS Code 扩展帮助习惯 Emacs 的开发者把 agda-mode 的交互体验迁移到 VS Code 中解决在编辑器里加载、类型检查与规范化 Agda 文件的问题。包内共 179 个文件以 67 个 js 与 64 个 res 源码为主另有 out/in 编译与测试用例、json 配置、md 文档、agda 示例及 less/css 样式等压缩包约 457KB结构紧凑。扩展支持通过 Cc Cl 等组合键加载文件并针对 VS Code 无法使用 Cu 前缀的限制改用 Cu 与 Cy 替代 Emacs 中的归一化级别前缀同时提供 Agda 语言服务器LSP实验支持可在面板右上角看到 LSP 标识。已有 238 人学习适合想用 VS Code 编写 Agda、需要键位映射参考与排错思路的读者。1. 装 agda-mode-vscode 之前先把 Agda 本体和版本对齐Agda 在 VS Code 里的体验八成取决于一件很多人忽略的事agda-mode-vscode只是编辑器前端真正干活的是你系统里的 Agda 可执行文件。前端和本体版本错位轻则高亮失灵重则每次保存都卡在Checking不动。我见过最典型的翻车是有人用包管理器装了 Agda 2.6.3又随手从扩展市场拉了最新版 agda-mode结果C-c C-l加载文件直接报协议不匹配折腾一下午以为是扩展坏了其实是两边版本没对齐。这套环境适合两类人一类是刚开始学依赖类型、想用 Agda 写证明的开发者另一类是原来在 Emacs 里用 agda-mode、现在想迁到 VS Code 的人。装之前先确认三件事——系统里有没有 Agda、版本是多少、VS Code 是不是较新的稳定版。这三样对齐了后面的配置基本是顺水推舟对不齐后面每一章你都会踩一遍。2. 环境准备Agda 本体、VS Code 与扩展的版本对照2.1 先装 Agda 本体别急着开 VS Codeagda-mode-vscode不附带 Agda 编译器所以第一步永远是让agda这个命令能在终端里跑起来。常见做法有三种系统包管理器、Haskell 工具链、预编译二进制。我一般推荐按平台选最省事的那条路别一上来就自己编译。Ubuntu / Debian 系# 更新索引后安装 Agda 本体 sudo apt update sudo apt install agda # 验证是否装好并记下版本号 agda --versionmacOS 用 Homebrewbrew install agda agda --versionWindows 上如果不想碰 Haskell 工具链直接去 Agda 官方发布页下预编译包解压后把bin目录加进PATH再在 PowerShell 里跑agda --version确认。这里的关键不是装哪个版本而是把版本号记下来。后面配扩展时要拿它对照。agda --version输出的形如Agda version 2.6.4这个2.6.4就是你的基准。提示如果你同时装了多个 Agda比如系统一个、cabal 一个用which agda看清楚 VS Code 会调用哪一个。扩展默认走PATH里的第一个。2.2 VS Code 与扩展的版本匹配VS Code 本身建议用当前稳定版即可这个扩展对编辑器版本不挑。真正要挑的是扩展和 Agda 本体的搭配。装扩展有两条路图形界面扩展面板搜agda-mode认准发布者是banacorn的那个点安装。命令行# 列出已装扩展确认 agda-mode 是否在列 code --list-extensions | grep -i agda # 如果没装用扩展 ID 安装 code --install-extension banacorn.agda-mode装完先别写代码打开命令面板CtrlShiftP/CmdShiftP搜Agda能看到Agda: Load、Agda: Goal这类命令说明扩展激活了。如果一条都搜不到多半是扩展没装成功或者被禁用回扩展面板看状态。2.3 版本对照表与选择建议组件建议版本说明Agda 本体2.6.3 / 2.6.4稳定分支扩展兼容性最好agda-mode-vscode与本体同代的最新版装完用命令面板确认激活VS Code当前稳定版对扩展版本不敏感GHC若走 cabal与 Agda 发布说明一致自己编译时才需要关心选版本的原则很简单Agda 本体优先选稳定版扩展跟着本体走。如果你用的是 nightly 或自己从源码编的 Agda扩展可能识别不了它的交互协议这时候要么降回稳定版要么接受部分功能不可用。新手别碰 nightly这是血泪经验。3. 配置 agda-mode路径、交互协议与几个必改项3.1 让扩展找到你的 Agda 可执行文件扩展默认在PATH里找agda。如果你的 Agda 装在非标准位置比如 cabal 的~/.cabal/bin或者 Windows 上某个自定义目录就得在 VS Code 设置里显式告诉它。打开settings.json{ // 指向 agda 可执行文件的绝对路径 agdaMode.connection.agdaPath: /home/user/.cabal/bin/agda, // 交互命令的超时单位毫秒大项目加载慢可以调大 agdaMode.connection.commandTimeout: 30000 }agdaPath是最容易写错的一项Windows 上路径要用双反斜杠或正斜杠macOS / Linux 上别写成~/开头的相对路径扩展不一定会展开波浪号。我一般直接写绝对路径省得猜。commandTimeout默认值对中小项目够用但如果你加载的文件依赖多、类型检查慢Checking阶段超时会被中断表现就是加载到一半停住。调到 30000 或更高通常能缓解。3.2 交互协议与编码设置Agda 和编辑器之间靠标准输入输出通信扩展负责把 Agda 的输出解析成高亮、目标、错误信息。这套机制对编码敏感尤其是文件里有 Unicode 数学符号Agda 大量使用∀、→、≡这类字符。{ // 强制以 UTF-8 读写避免 Unicode 符号乱码 files.encoding: utf8, // 保存时不自动转换行尾防止 Agda 解析异常 files.eol: \n, // 关闭对 Agda 文件的自动格式化交给 agda-mode 自己处理 [agda]: { editor.formatOnSave: false } }files.encoding这项在 Windows 上尤其重要默认可能是 GBK 或 UTF-16Agda 文件一存就乱码加载时报一堆看不懂的语法错误。formatOnSave关掉是因为 Agda 的对齐有语义别的格式化器一插手证明结构就散了。3.3 输入法与快捷键的取舍Agda 的 Unicode 符号靠输入法打扩展自带一套输入法默认用反斜杠触发比如\forall出∀。这套输入法在 VS Code 里和别的快捷键可能冲突我一般会检查两处{ // 输入法触发键默认是反斜杠冲突时可改 agdaMode.inputMethod.triggerKey: \\, // 是否启用输入法关掉就只能靠系统输入法打符号 agdaMode.inputMethod.enabled: true }如果你系统里已经有一套顺手的 Unicode 输入方案可以把enabled设成false避免两套输入法打架。但新手建议先留着扩展自带的这套和 Agda 符号集是对齐的打\to出→、\bn出ℕ比记系统输入法省事。4. 避坑与排查agda-mode 装完不工作的五种情况4.1 现象命令面板搜不到 Agda 命令原因通常是扩展没装成功或者被 VS Code 的扩展宿主禁用了。先跑code --list-extensions | grep -i agda确认在不在列表里。在列表里但搜不到命令多半是扩展激活失败打开「输出」面板切到Agda频道看有没有报错。解决方式是卸载重装或者检查 VS Code 版本是不是太旧。4.2 现象加载文件一直停在 Checking原因有两个常见来源一是agdaPath指错了扩展调的根本不是你想的那个 Agda二是commandTimeout太小大文件没检查完就被掐断。先在终端手动跑agda 你的文件.agda看本体能不能正常检查。本体没问题再回头核对agdaPath和超时设置。4.3 现象Unicode 符号显示成方块或乱码原因是文件编码不是 UTF-8。检查files.encoding是不是utf8以及文件本身是不是被别的编辑器用 GBK 存过。解决方式是统一改成 UTF-8 重存必要时用iconv转一遍。这类问题在跨平台协作时特别常见一个人 Windows 一个人 macOS编码不统一就互相踩。4.4 现象输入法触发键没反应原因是触发键和 VS Code 或系统快捷键冲突。先看agdaMode.inputMethod.triggerKey设的是什么再检查有没有别的扩展占用了同一个键。换个不常用的触发键比如;或§通常能绕开。改完记得重启 VS Code 让设置生效。4.5 现象保存后高亮全丢原因是formatOnSave被别的格式化扩展接管了把 Agda 的对齐改乱了。确认[agda]段里editor.formatOnSave是false并且没有全局的格式化扩展对.agda文件生效。Agda 的缩进和对齐是有语义的任何自动格式化都可能破坏证明结构。5. 验证跑通用一个最小证明确认整条链路装完配完别急着开大项目先用一个最小文件把「编辑器 → Agda 本体 → 高亮回显」这条链路走通。新建Hello.agda-- 最小可加载模块用来验证 agda-mode 是否工作 module Hello where -- 定义一个最简单的类型 data Bool : Set where true : Bool false : Bool -- 定义一个恒等函数检查类型检查是否通过 id : Bool → Bool id x x保存后按C-c C-lVS Code 里对应命令面板的Agda: Load。预期结果是文件里的Set、Bool、→变成高亮色底部状态栏显示加载成功没有红色错误波浪线。如果高亮出来了、没有报错说明整条链路通了。再进一步把光标放在id x x的x上按C-c C-,Agda: Goal type and context底部应该弹出当前目标的类型和上下文。这一步能验证交互协议是双向通的不只是单向高亮。验证项操作通过标准本体可调用终端agda --version输出版本号扩展已激活命令面板搜Agda出现 Agda 命令加载链路C-c C-l高亮出现、无报错交互协议C-c C-,弹出目标类型与上下文编码正确文件含→∀显示正常不乱码我自己的习惯是每换一台机器、每升一次 Agda 版本都拿这个最小文件先跑一遍这五项。有一次升级后高亮正常但C-c C-,没反应就是交互协议那项挂了靠这个清单两分钟定位到是扩展版本没跟上本体。从那以后我每次配完 agda-mode 都强制走一遍这个最小验证不省这一步。希望帮到你。本文还有配套的精品资源点击获取
