《编程语言基础：Agda 描述》的使用方法和《Programming Language Foundations in Agda》一致。

要参与翻译请先阅读翻译规范

开始使用 PLFA

为使用 PLFA，你需要以下工具：

大部分工具的安装方式遵循其对应网页提供的说明即可。本页顶部的徽章列出了 PLFA 使用的依赖版本。

你可以执行下方的命令克隆仓库或者下载 zip 包（原书 / 中文版）以从 GitHub 获取最新版的 PLFA。

原书：

git clone https://github.com/plfa/plfa.github.io

中文版：

git clone https://github.com/Agda-zh/PLFA-zh

最后，我们需要让 Agda 知道标准库位于何处。此处的说明可供参考。

如果你想完成位于 tspl 目录内的习题，或者想导入书中的模块，PLFA 也可以被设置为一个 Agda 库。完成此设置需要将 plfa.agda-lib 所处的路径作为单独的一行添加到 ~/.agda/libraries，并将 plfa 作为单独的一行添加到 ~/.agda/defaults。

构建本书

要在本地构建并部署本书，在前文所列工具的基础之上，你还需要：

大部分工具的安装遵循其对应的网页提供的说明即可。Ruby 的较新版本应该都可以使用。

我们建议使用 Stack 安装 agda2html：

git clone https://github.com/wenkokke/agda2html.git
cd agda2html
stack install

安装完所有的工具后，我们就可以从源码构建本书了：

make build

运行如下命令可以在本地部署本书：

make serve

Makefile 提供了更多可选的命令：

make                      （见 make test）
make build                （将 lagda 构建至 markdown 并构建网站）
make build-offline        （将 lagda 构建至 markdown 并离线构建网站）
make build-incremental    （将 lagda 构建至 markdown 并增量式构建网站）
make test                 （检查所有链接的有效性）
make test-offline         （离线检查所有链接的有效性）
make serve                （启动服务）
make server-start         （以分离模式启动服务）
make server-stop          （使用 pkill 停止服务）
make clean                （移除所有~非必要的~生成的文件）
make clobber              （移除所有生成的文件）

如果你只想获取本书的副本以供离线阅读，而并不关心如何编辑并构建本书，那么你可以下载由 Travis 自动构建的 master 分支（原书 / 中文版）。若要在本地部署本书，你需要 Ruby 和 Bundler（见上文）。请下载 master 分支的压缩包，并在解压后的目录中运行：

bundle install
bundle exec jekyll serve

GNU sed 和 macOS

macOS 预装的 sed 版本和 GNU sed 并不完全兼容。因此，你可能会遇到类似这样的错误：

sed: 1: "out/plfa/Bisimulation.md": invalid command code o

你可以通过安装 GNU 兼容版 sed 来修复此错误，如执行以下 Homebrew 命令：

brew install gnu-sed --with-default-names

更新 `agda2html`

有时我们需要更新 agda2html。要更新你的本地副本，可以在你克隆的 agda2html 仓库中运行如下命令。更简单的方法是按照前文所述的方法重新安装 agda2html。

git pull
stack install

Unicode 字符

如果你在 Emacs 中输入 Unicode 字符时遇到困难，每一章的结尾都列出了该章引入的 Unicode 字符。所支持字符的完整列表请参阅 agda-input.el。

使用 `agda-mode`

?            坑
{!...!}      有内容的坑
C-c C-l      加载缓冲区

在洞上可用的命令：

C-c C-c x    在变量 x 上分项（自动模式匹配）
C-c C-空格   填坑
C-c C-r      用构造器精化
C-c C-a      自动填坑
C-c C-,      目标类型和上下文
C-c C-.      目标类型，上下文，以及推断的类型

更多细节请见 emacs-mode 文档

如果你希望在 Agda 代码侧边而非底部查看消息，可以参考如下操作：

载入 Agda 文件并按 C-c C-l；
按 C-x 1 以仅显示当前 Agda 文件；
按 C-x 3 以垂直分割窗口；
将光标移动到右侧窗口；
按 C-x b 并输入 “Agda information” 以切换到该缓冲区。

现在，来自 Agda 的错误消息将会在代码右侧显示，而非被压缩在底部的狭小空间里。

Emacs 中的字体

如果你有以下代码中提及的字体，推荐将这些代码添加到 Emacs 配置文件 ~/.emacs 的末尾。

;; Setting up Fonts for use with Agda/PLFA
;;
;; default to DejaVu Sans Mono,
(set-face-attribute 'default nil
		    :family "DejaVu Sans Mono"
		    :height 120
		    :weight 'normal
		    :width  'normal)

;; fix \:
(set-fontset-font "fontset-default"
		  (cons (decode-char 'ucs #x2982)
			(decode-char 'ucs #x2982))
		  "STIX")

Markdown

本书使用 Kramdown Markdown 编写。

Travis 持续集成

你可以在 https://travis-ci.org/ 查看 PLFA 的构建历史（原书 / 中文版）。