layout	title	permalink	translators
page	使用说明	/GettingStarted/	Rongxiao Fu

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

本书可访问 PLFA-zh 在线阅读。

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

开始使用 PLFA

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

• Agda
• Agda 标准库

大部分工具的安装方式遵循其对应网页提供的说明即可。 这里有篇安装配置的教程可供参考。 本页顶部的徽章列出了 PLFA 使用的依赖版本。我们已经用上面列出的版本测试过了， 其它更旧或更新的版本可能会出问题。

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

原书：

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

中文版：

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

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

如果你想完成 courses 目录中的习题，或者想导入书中的模块， 那么需要将 PLFA 设置为 Agda 库。完成此设置需要将 plfa.agda-lib 所在的路径作为单独的一行添加到 ~/.agda/libraries，并将 plfa 作为单独的一行添加到 ~/.agda/defaults。

在 Emacs 中自动加载 agda-mode

为了让 agda-mode 在你打开 .agda 或 .lagda.md 文件时自动加载， 请将以下内容放到你的 Emacs 配置文件中。

(setq auto-mode-alist
   (append
     '(("\\.agda\\'" . agda2-mode)
       ("\\.lagda.md\\'" . agda2-mode))
     auto-mode-alist))

Emacs 的配置文件通常位于 ~/.emacs 或 ~/.emacs.d/init.el，不过 Aquamacs 用户需要将启动设置放到位于 ~/Library/Preferences/Aquamacs Emacs/Preferences 的 Preferences.el 文件中。

Unicode 字符

如果你在 Emacs 中输入 Unicode 字符时遇到困难，每一章的结尾都列出了该章引入的 Unicode 字符。

agda-mode 和 Emacs 有很多有用的命令，其中的两个在你做练习时非常有用。

要查看所支持字符的完整列表，请使用 agda-input-show-translations：

M-x agda-input-show-translations

这样会显示出 agda-mode 中所有支持的字符。

如果你想知道如何在 agda 文件中输入一个特定的 Unicode 字符，请将光标移至该字符上， 然后输入以下命令：

M-x quail-show-key

你会在迷你缓冲区中看到输入该字符所需的按键序列。

使用 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 中的字体

推荐安装 mononoki 字体，并将以下内容添加到位于 ~/.emacs 的 Emacs 配置文件的末尾：

;; default to mononoki
(set-face-attribute 'default nil
		    :family "mononoki"
		    :height 120
		    :weight 'normal
		    :width  'normal)

另外带有连体符号的 FiraCode 也是个不错的选择。

构建本书

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

• Ruby
• Bundler

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

你需要用 Bundler 安装 Ruby 依赖：Jekyll、 html-proofer 等。

bundle install

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

make build

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

make serve

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

make                      （见 make test）
make build                （将 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

Markdown

本书使用 Kramdown Markdown 编写。

Travis 持续集成

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