配置 Agda 与 Emacs 环境
由于我正在修读的 CSC3120: Principles of Programming Languages 课程使用 Agda 作为主要的编程语言，本文记录如何在 Apple Silicon Mac 上使用 Nix 搭建 Agda 开发环境，并配置 Emacs 的 Agda 模式。
前置准备
需要安装以下工具：
- Nix
- Emacs
Nix 可以创建可复现的开发环境，因此这里使用它来管理 Agda 及其标准库。
本文使用 Nix flakes，需要启用 nix-command 和 flakes。如果尚未启用，可以在 ~/.config/nix/nix.conf 中添加以下配置；如果已有 experimental-features 配置，请将这两个选项合并进去：
experimental-features = nix-command flakes创建 Nix 开发环境
在存放 Agda 代码的仓库根目录创建 flake.nix：
{
description = "Agda development environment";
inputs = {
nixpkgs.url = "github:NixOS/nixpkgs/nixpkgs-unstable";
};
outputs =
{ nixpkgs, ... }:
let
system = "aarch64-darwin";
pkgs = import nixpkgs { inherit system; };
agda-with-stdlib = pkgs.agda.withPackages (p: [
p.standard-library
]);
in
{
devShells.${system}.default = pkgs.mkShell {
packages = [
agda-with-stdlib
];
};
};
}这里的 aarch64-darwin 对应 Apple Silicon Mac。如果使用其他平台，需要修改 system，例如 x86-64 Linux 使用 x86_64-linux。
如果仓库由 Git 管理，先将 flake.nix 加入 Git 索引，确保 Nix 能读取它：
git add flake.nix然后在仓库根目录进入开发环境，并确认 Agda 可用：
nix develop
agda --version首次运行会生成 flake.lock。建议将它与 flake.nix 一起提交到仓库，以锁定依赖版本；仅使用 nixpkgs-unstable 分支名并不能保证不同时间创建的环境具有相同版本。
退出这个 shell 后，开发环境提供的 Agda 不再自动出现在当前 shell 的 PATH 中。下次开发时，需要重新运行 nix develop。
nix develop 默认会运行 bash，需要其他的 shell 可以使用 nix develop -c fish 等。
配置 Agda 项目
在仓库根目录创建 <NAME>.agda-lib，并写入以下内容：
name: <NAME>
include: .
depend: standard-library其中：
name是项目的库名，可以根据项目修改。include: .表示模块的搜索路径包含该配置文件所在的目录，也就是这里的仓库根目录。depend: standard-library声明项目依赖 Agda 标准库。上面的 Nix 配置通过agda.withPackages提供该依赖。
Agda 文件的顶层模块名需要与相对于搜索路径的文件路径对应，且大小写必须一致。例如：
-- <PROJECT_ROOT>/example.agda
module example where-- <PROJECT_ROOT>/foo/bar.agda
module foo.bar where配置 Emacs
我习惯将 Emacs 安装在开发环境之外，让不同项目共用同一个编辑器 （虽然我目前只用 Emacs 编写 Agda）。通过 Nix 安装的 Emacs 同样可以编辑配置文件。
将以下配置放入 Emacs 的初始化文件：
(require 'subr-x)
(when-let ((agda (executable-find "agda")))
(load-file
(string-trim
(shell-command-to-string
(concat
(shell-quote-argument agda)
" --emacs-mode locate"))))
(require 'agda2-mode))这段配置通过当前环境中的 agda 查找并加载对应版本的 Emacs 模式。只有当 Emacs 能找到 agda 时，配置才会生效。
因此，建议在 nix develop 创建的 shell 中启动一个新的 Emacs 进程。
从 macOS Dock 启动的 Emacs 通常不会继承 Nix 开发环境，因此可能找不到 Agda。已经运行的 Emacs daemon 也不会因为执行了 nix develop 就自动获得新环境；通过 emacsclient 连接已有 daemon 不等同于从开发环境启动新的 Emacs 进程。
验证环境
在仓库根目录创建 Example.agda：
module Example where
open import Data.Nat using (ℕ; zero)
example : ℕ
example = zero在开发环境中运行：
agda Example.agda
emacs Example.agda如果尚未进入开发环境，先在仓库根目录运行 nix develop。若 agda Example.agda 成功结束且没有报错，说明 Agda 能找到项目和标准库。
在 Emacs 中按 C-c C-l 加载并检查文件。文件成功加载后，便可以开始编写 Agda 代码。
Agda 模式还提供 Unicode 输入法。例如，在 Agda 文件中输入 \bN 可以得到 ℕ，输入 \to 可以得到 →。
常见问题
- Emacs 没有启用 Agda 模式：使用
M-:执行(executable-find "agda")。如果结果为nil，请确认是从nix develop的 shell 中启动了新的 Emacs 进程。 - 找不到标准库：先确认命令运行在开发环境中，再检查仓库根目录的
<NAME>.agda-lib是否包含depend: standard-library，以及flake.nix是否使用了包含p.standard-library的 Agda 包。 - 模块名与文件路径不匹配：检查顶层
module声明、文件名和目录名是否对应，尤其注意大小写。