| layout | title | permalink | translators | |
|---|---|---|---|---|
page |
使用说明 |
/GettingStarted/ |
|
《编程语言基础：Agda 语言描述》的使用方法和《Programming Language Foundations in Agda》一致。
本书可访问 PLFA-zh 在线阅读。
要参与翻译，请先阅读翻译规范
为使用 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。
为了让 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 文件中。
如果你在 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
你会在迷你缓冲区中看到输入该字符所需的按键序列。
? 洞
{!...!} 有内容的洞
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 的错误消息将会在代码右侧显示，而非被压缩在底部的狭小空间里。
推荐安装 mononoki 字体，并将以下内容添加到位于
~/.emacs 的 Emacs 配置文件的末尾：
;; default to mononoki
(set-face-attribute 'default nil
:family "mononoki"
:height 120
:weight 'normal
:width 'normal)另外带有连体符号的 FiraCode 也是个不错的选择。
要在本地构建并部署本书，在前文所列工具的基础之上，你还需要：
大部分工具的安装遵循其对应的网页提供的说明即可。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
本书使用 Kramdown Markdown 编写。
你可以在 https://travis-ci.org/ 查看 PLFA 的构建历史（原书 / 中文版）。