Build Status Agda agda-stdlib

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

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

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

开始使用 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 知道标准库位于何处。 此处的说明可供参考。

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

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")

构建本书

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

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

你需要用 Bundler 安装 Ruby 依赖:Jekyllhtml-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 的构建历史(原书 / 中文版)。