j0hn50n133 / plfa-zh Goto Github PK

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

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

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

你可以在线阅读 PLFA，无需安装任何东西。 然而，如果你想要交互式编写代码或完成习题，那么就需要几样东西：

• Agda
• Agda 标准库
• PLFA（英文版）
• PLFA-zh（中文版）

PLFA 只针对特定的 Agda 和 标准库版本进行了测试，相应版本已在前面的徽章中指明。 Agda 和标准库变化得十分迅速，而这些改变经常搞坏 PLFA，因此使用旧版或新版通常会出现问题。

安装特定 Agda 版本的最简方式是使用 Stack。你可以从 GitHub 上获取需要的版本， 可以通过克隆源码库并切换到合适的分支，也可以直接下载 Zip 包：

git clone https://github.com/agda/agda.git
cd agda
git checkout v2.6.1

要安装 Agda，请在其源码目录中运行 Stack：

stack install --stack-yaml stack-8.8.3.yaml

如果你想让 Stack 使用你系统上安装的 GHC 版本，可以传递 --system-ghc 选项并选择对应的 stack-*.yaml 文件。例如，若你安装了 GHC 8.2.2，请运行：

stack install --system-ghc --stack-yaml stack-8.2.2.yaml

你可以从 GitHub 上获取所需要的版本，可以通过克隆源码库并切换到合适的分支，也可以直接下载 Zip 包：

git clone https://github.com/agda/agda-stdlib.git
cd agda-stdlib
git checkout v1.3

你也可以从 GitHub 克隆源码库，或者下载 Zip 包来获取最新版的《编程语言基础：Agda 语言描述》：

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

最后，我们需要让 Agda 知道如何找到标准库。你可以按照这里给出的步骤来设置。

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

推荐的 Agda 编辑器是 Emacs 加上 agda-mode。Agda 自带了 agda-mode， 因此如果你已经安装了 Agda，那么之需要运行以下命令就能配置好 agda-mode 了：

agda-mode setup

要加载文件并对其执行类型检查，请使用 C-c C-l。

Agda 的编辑是通过使用「洞」来交互的，它表示程序中尚未填充的片段。 如果用问号作为表达式，并用 C-c C-l 加载缓冲区，Agda 会将问号替换为一个「洞」。 当光标在洞中时，你可以做以下这些事情：

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 的错误消息将会在代码右侧显示，而非被挤压在底部的狭小空间里。

从版本 2.6.0 开始，Agda 支持 Markdown 风格的文学编程，文件使用 .lagda.md 扩展名。 该扩展名的一个副作用就是大部分编辑器默认会进入 Markdown 编辑模式。

而为了让 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 文件中。

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

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

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

如果你在 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

你会在迷你缓冲区中看到该字符对应的按键序列。

PLFA 可同时在网站上和作为 EPUB 电子书来阅读，二者均可在 Linux 和 macOS 上构建。 PLFA 是以 Kramdown Markdown 格式的文学化 Agda 编写的。

本源码库包含了几个 Git 钩子：

1. fix-whitespace 程序用来检查错误的空格。

2. 可运行的测试套件用来保证一切都能通过类型检查。

你可以运行 make init 来安装这些 Git 钩子。 你可以运行以下命令来安装 fix-whitespace：

git clone https://github.com/agda/fix-whitespace
cd fix-whitespace/
stack install --stack-yaml stack-8.8.3.yaml

如果你想让 Stack 使用你系统中安装的 GHC，那么可以传入 --system-ghc 参数并选择对应的 stack-*.yaml 文件，就像在安装 Agda 时那样。

本书的网站版本是通过三步来构建的：

1. .lagda.md 文件会使用 Agda 的高亮被编译到 Markdown。 （这需要几个 POSIX 工具，包括 bash、sed 和 grep。）

2. Markdown 文件会通过 Jekyll 转换为 HTML，它是一个被广发使用的静态网站构建工具。 （这需要 Ruby 和 Jekyll。）

3. HTML 会使用 html-proofer 来检查。 （这需要 Ruby 和 html-proofer。）

最新版本的 Ruby 应该就可以了。安装 Jekyll 和 html-proofer 最简单的方式是使用 Bundler。 你可以通过运行以下命令来安装 Bundler：

gem install bundler

你也可以运行以下命令来安装 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 分支（原书 / 中文版）。 若要在本地部署本书，你同样需要 Jekyll 和 Bundler（见上文）。 请下载 master 分支的压缩包，并在解压后的目录中运行：

bundle install
bundle exec jekyll serve

本书的 EPUB 版本 使用 Pandoc 构建。

请安装最新版的 Pandoc，可从这里下载。安装 Pandoc 最简单的方式是用是它的官方安装包， 这样比通过 Haskell Stack 从源码构建安装要快上许多。

安装好 Pandoc 之后，你就可以运行以下命令来构建 EPUB 了：

make epub

EPUB 文件会输出到 out/epub/plfa.epub。