title | permalink | translators | ||
---|---|---|---|---|
使用说明 |
/GettingStarted/ |
|
《编程语言基础:Agda 语言描述》的使用方法与《Programming Language Foundations in Agda》一致。
本书可访问 PLFA-zh 在线阅读。
要参与翻译,请先阅读翻译规范。
你可以在线阅读 PLFA,无需安装任何东西。 然而,如果你想要交互式编写代码或完成习题,那么就需要几样东西:
- macOS 上:XCode 命令行工具
- Git
- GHC and Cabal
- Agda
- Agda 标准库
- PLFA
PLFA 只针对特定的 Agda 和 标准库版本进行了测试,相应版本已在前面的徽章中指明。 Agda 和标准库变化得十分迅速,而这些改变经常搞坏 PLFA,因此使用旧版或新版通常会出现问题。
Agda 和 Agda 标准库有多个版本。如果你使用了包管理器(如 Homebrew 或者 Debian apt),Agda 的版本可能不是最新的。除此之外,Agda 仍然在活跃的开发之中,如果你从 GitHub 上安装了开发版本,开发者的新变更也可能让这里的代码出现问题。 因此,使用上述版本的 Agda 和 Agda 标准库很重要。
在 macOS 平台,你需要安装 XCode 命令行工具。 在大多数 macOS 系统版本上,你可以用下面的命令安装它们:
xcode-select --install
你可以使用下面的命令来检查你是否安装了 Git。
git --version
如果你没有 Git,请参阅 Git 下载页面。
Agda 是用 Haskell 写成的,所以为了安装它我们需要 Glorious Haskell Compiler
和它的包管理器 Cabal。PLFA 应该在任何 >=8.10 的 GHC 版本下运行,在 8.10 到 9.8 版本下完成测试。我们建议使用 ghcup 来安装两者。
在 ghcup
安装好之后,输入下列命令:
ghcup install ghc 9.4.8
ghcup install cabal recommended
ghcup set ghc 9.4.8
ghcup set cabal recommended
或使用 ghcup tui
来『设置』合适的工具。
安装 Agda 最简单的方法是通过 Cabal。PLFA 使用 Agda 版本 2.7.0。运行下面的命令:
cabal update
cabal install Agda-2.7.0
这一步会消耗很长时间和很多内存来完成。
如果你遇到了问题,或者想参考替代的方法,可参阅 Agda 安装指引。
如果你愿意,你可以测试 Agda 是否已正确安装。
我们建议您使用下面的命令把 PLFA 安装至你的家目录:
git clone --depth 1 https://github.com/plfa/plfa.github.io plfa
PLFA 包括了所需的 Agda 标准库版本,你可以在安装 PLFA 的目录下运行以下命令来下载它。
git submodule update --init
最后,我们需要让 Agda 知道如何找到标准库。 你需要两个配置文件,一个用于指定库的路径,一个用于指定默认载入的库。
在 macOS 和 Unix 上,如果 PLFA 已经安装至 Home 目录,且你没有希望保存的配置文件,运行下面的命令:
mkdir -p ~/.agda
cp ~/plfa/data/dotagda/* ~/.agda
这条命令提供了 Agda 标准库,也让 PLFA 可以当作一个 Agda 库来使用。
否则,你需要手动编辑相关的配置文件。两者都位于 AGDA_DIR
目录下。
在 UNIX 和 macOS 平台,AGDA_DIR
默认为
~/.agda
。在 Windows 平台,AGDA_DIR
一般默认为 %AppData%\agda
,而
%AppData%
默认为 C:\Users\USERNAME\AppData\Roaming
。
- 如果
AGDA_DIR
文件夹不存在,创建它。 - 在
AGDA_DIR
中,创建一个纯文本文件libraries
,内容为/path/to/standard-library.agda-lib
(即上文中记录的路径)。 这个文件让 Agda 知道有一个名为standard-library
的库可用。 - 在
AGDA_DIR
中,创建一个纯文本文件defaults
,内容__仅__为standard-library
这一行。 - 如果你想导入书中的模块,那么需要将 PLFA 设置为 Agda 库。假设
PLFA
是 PLFA 的根目录,完成此设置需要将PLFA/src/plfa.agda-lib
作为单独的一行添加到AGDA_DIR/libraries
,并将plfa
作为单独的一行添加到AGDA_DIR/defaults
。
关于放置标准库的更多信息可以参阅 Agda 文档中的库管理。
推荐的 Agda 编辑器是 Emacs。安装 Emacs 可以用下面的方法:
- UNIX:包管理器中的 Emacs 应该可以使用(只要它的版本比较新),GNU Emacs 下载页面也有最近发布版本的链接。
- MacOS:推荐的 Emacs 是 Aquamacs,但是 GNU Emacs 也可以通过 Homebrew 或者 MacPorts 安装。参阅 GNU Emacs 下载页面中的指示。
- Windows:参阅 GNU Emacs 下载页面中的指示。
确保你可以用你安装的版本打开、编辑、保存文件。GNU Emacs 网站上的 Emacs 向导描述了如果打开 Emacs 安装中的教程。
Agda 自带了 Emacs 编辑器支持,如果你安装了 Agda,运行下面的命令来配置 Emacs:
agda-mode setup
agda-mode compile
如果你已经是 Emacs 用户,并有自己的设置,你会发现 setup
命令向你的 .emacs
文件中追加了配置,来配合你已有的设置。
从版本 2.6.0 开始,Agda 支持 Markdown 风格的文学编程,文件使用 .lagda.md
扩展名。
该扩展名的一个问题就是 Emacs 默认会进入 Markdown 编辑模式。
而为了让 agda-mode
在你打开 .agda
或 .lagda.md
文件时自动加载,
请将以下内容放到你的 Emacs 配置文件中:
;; auto-load agda-mode for .agda and .lagda.md
(setq auto-mode-alist
(append
'(("\\.agda\\'" . agda2-mode)
("\\.lagda.md\\'" . agda2-mode))
auto-mode-alist))
如果你的配置中已有了改变 auto-mode-alist
的设置,将上述内容放置在已有的设置__之后__,或者将其与已有设置合并(如果你对
Emacs Lisp 足够了解)。
Emacs 的配置文件通常位于 ~/.emacs
或 ~/.emacs.d/init.el
,然而
Aquamacs 用户需要将启动设置放到位于 ~/Library/Preferences/Aquamacs Emacs/Preferences
的 Preferences.el
文件中。
对于 Windows 平台,请参阅 GNU Emacs 文档 来寻找配置文件的位置。
Agda 中的很多重要符号是用 Unicode 来表示的,因此用来显示和编辑 Agda 的字体需要正确地显示这些符号。最重要的是你使用的字体需要有好的 Unicode 字符支持。我们推荐 Mononoki, 其他的备选字体有 Source Code Pro、 DejaVu Sans Mono 和 FreeMono。
你可以直接从此网站 下载并安装
Mononoki。对于大多数系统来说,安装字体只是简单的下载 .otf
或者 .ttf
文件。
如果你的包管理器提供了 Mononoki 的包,那样可能更加简单。
例如,macOS 的 Homebrew 提供了
font-mononiki
包;Debian 的 APT 提供了 fonts-mononoki
包。
将下面的内容加入 Emacs 配置文件,可以把 Mononoki 设置为 Emacs 的默认字体:
;; default to mononoki
(set-face-attribute 'default nil
:family "mononoki"
:height 120
:weight 'normal
:width 'normal)
在 Emacs 中打开本书的第一章 (plfa/src/plfa/part1/Naturals.lagda.md
),输入
C-c C-l
来载入和类型检查这个文件。
要加载文件并对其执行类型检查,请使用 C-c C-l
。
Agda 的编辑是通过使用「洞」来交互的,它表示程序中尚未填充的片段。
如果用问号作为表达式,并用 C-c C-l
加载缓冲区,Agda 会将问号替换为一个「洞」。
当光标在洞中时,你可以做以下这些事情:
C-c C-c
: 分项(询问变量名,case)C-c C-空格
:填洞C-c C-r
:用构造子精化(refine)C-c C-a
:自动填洞(automatic)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 的错误消息将会在代码右侧显示,而非被挤压在底部的狭小空间里。
当你书写 Agda 代码时,你需要输入标准键盘上没有的字符。Emacs 的「Agda-mode」定义了字符翻译来让这件事更容易:当你输入特定普通字符的序列时,Emacs 会在 Agda 文件中使用对应的特殊字符来替换。
例如,我们可以在之前的 .agda
测试文件中加入一条注释。
比如说,我们想要加入下面的注释:
{- I am excited to type ∀ and → and ≤ and ≡ !! -}
前几个字符都是普通字符,我们可以如往常的方式输入它们……
{- I am excited to type
在最后一个空格之后,我们无法在键盘上找到 ∀ 这个键。这个字符的输入序列是四个字符
\all
,所以我们输入这四个字符,当我们完成时,Emacs 会把它们替换成我们想要的……
{- I am excited to type ∀
我们继续输入其他字符。有时字符会在输入时发生变化,因为一个字符的输入序列是另一个字符输入序列的前缀。
在我们输入箭头时会出现这样的情况,它的输入序列是 \->
。在输入 \-
之后我们会看到……
{- I am excited to type ∀ and -
……因为输入序列 \-
对应了一定长度的短横。当我们输入 >
时,
变成了 →
!
≤
的输入序列是 \<=
,≡
的是 \==
。
{- I am excited to type ∀ and → and ≤ and ≡
最后几个字符又回归了普通字符……
{- I am excited to type ∀ and → and ≤ and ≡ !! -}
如果你在 Emacs 中输入 Unicode 时遇到了问题,可以在每章的最后找到当前章节中用到的 Unicode 字符。
带有 agda-mode
的 Emacs 提供了很多有用的命令,其中有两个对处理 Unicode
字符时特别有用。
支持的字符的完整列表可使用 agda-input-show-translations
命令查看:
M-x agda-input-show-translations
agda-mode
支持的所有字符都会列出来。
如果你想知道如何在 agda 文件输入一个特定的 Unicode 字符,请将光标移动到该字符上并输入以下命令:
M-x quail-show-key
你会在迷你缓冲区中看到该字符对应的按键序列。
Spacemacs 是一个「社区引领的 Emacs 版本」,对 Emacs 和 Vim
的编辑方式都有很好的支持。它自带集成了
agda-mode
,所需的只是将 .spacemacs
中启用 Agda 支持。
Visual Studio Code 是一个微软开发的开源代码编辑器。 Visual Studio 市场中有 Agda 插件。
If you plan to build PLFA locally, please refer to Contributing for additional instructions.