layout | title | permalink | translators | ||
---|---|---|---|---|---|
page |
使用说明 |
/GettingStarted/ |
|
《编程语言基础:Agda 语言描述》的使用方法与《Programming Language Foundations in Agda》一致。
本书可访问 PLFA-zh 在线阅读。
要参与翻译,请先阅读翻译规范。
你可以在线阅读 PLFA,无需安装任何东西。 然而,如果你想要交互式编写代码或完成习题,那么就需要几样东西:
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 钩子:
-
fix-whitespace 程序用来检查错误的空格。
-
可运行的测试套件用来保证一切都能通过类型检查。
你可以运行 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 时那样。
本书的网站版本是通过三步来构建的:
-
.lagda.md
文件会使用 Agda 的高亮被编译到 Markdown。 (这需要几个 POSIX 工具,包括bash
、sed
和grep
。) -
Markdown 文件会通过 Jekyll 转换为 HTML,它是一个被广发使用的静态网站构建工具。 (这需要 Ruby 和 Jekyll。)
-
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
。