文件列表:

PLFA-zh-dev/ (0, 2023-04-13)
PLFA-zh-dev/.dir-locals.el (391, 2023-04-13)
PLFA-zh-dev/.epubcheck.tsv (64, 2023-04-13)
PLFA-zh-dev/.htmlvalidate.json (359, 2023-04-13)
PLFA-zh-dev/.htmlvalidateignore (86, 2023-04-13)
PLFA-zh-dev/.node-version (3, 2023-04-13)
PLFA-zh-dev/.nojekyll (0, 2023-04-13)
PLFA-zh-dev/.pre-commit-config.yaml (738, 2023-04-13)
PLFA-zh-dev/.python-version (7, 2023-04-13)
PLFA-zh-dev/.ruby-version (6, 2023-04-13)
PLFA-zh-dev/.vscode/ (0, 2023-04-13)
PLFA-zh-dev/.vscode/tasks.json (794, 2023-04-13)
PLFA-zh-dev/CONTRIBUTING.md (9421, 2023-04-13)
PLFA-zh-dev/Gemfile (116, 2023-04-13)
PLFA-zh-dev/LICENSE (18664, 2023-04-13)
PLFA-zh-dev/Makefile (3819, 2023-04-13)
... ...

--- title : 使用说明 permalink: /GettingStarted/ translators : ["Rongxiao Fu", "Oling Cat"] --- [![Build Status][plfa-badge-status-svg]][plfa-badge-status-url] [![pre-commit.ci status][pre-commit-status-svg]][pre-commit-status-url] [![Release Version][plfa-badge-version-svg]][plfa-badge-version-url] [![agda][agda-badge-version-svg]][agda-badge-version-url] [![standard-library][agda-stdlib-version-svg]][agda-stdlib-version-url] ## 读者指南 {#getting-started-for-readers} 《编程语言基础：Agda 语言描述》的使用方法与《Programming Language Foundations in Agda》一致。 **本书可访问 [PLFA-zh][plfa-zh] 在线阅读。** **要参与翻译，请先阅读[翻译规范][trans-spec]。** 你可以[在线阅读][plfa-zh] PLFA，无需安装任何东西。 然而，如果你想要交互式编写代码或完成习题，那么就需要几样东西： - macOS 上：[XCode 命令行工具](https://github.com/Agda-zh/PLFA-zh/blob/master/#on-macos-install-the-xcode-command-line-tools) - [Git](https://github.com/Agda-zh/PLFA-zh/blob/master/#install-git) - [GHC and Cabal](https://github.com/Agda-zh/PLFA-zh/blob/master/#install-ghc-and-cabal) - [Agda](https://github.com/Agda-zh/PLFA-zh/blob/master/#install-agda) - [Agda 标准库](https://github.com/Agda-zh/PLFA-zh/blob/master/#install-plfa-and-the-agda-standard-library) - [PLFA](https://github.com/Agda-zh/PLFA-zh/blob/master/#install-plfa-and-the-agda-standard-library) PLFA 只针对特定的 Agda 和 标准库版本进行了测试，相应版本已在前面的徽章中指明。 Agda 和标准库变化得十分迅速，而这些改变经常搞坏 PLFA，因此使用旧版或新版通常会出现问题。 Agda 和 Agda 标准库有多个版本。如果你使用了包管理器（如 Homebrew 或者 Debian apt），Agda 的版本可能不是最新的。除此之外，Agda 仍然在活跃的开发之中，如果你从 GitHub 上安装了开发版本，开发者的新变更也可能让这里的代码出现问题。 因此，使用上述版本的 Agda 和 Agda 标准库很重要。 ### macOS 平台：安装 XCode 命令行工具{#on-macos-install-the-xcode-command-line-tools} 在 macOS 平台，你需要安装 [XCode 命令行工具][xcode]。 在大多数 macOS 系统版本上，你可以用下面的命令安装它们： ```bash xcode-select --install ``` ### 安装 Git {#install-git} 你可以使用下面的命令来检查你是否安装了 Git。 ```bash git --version ``` 如果你没有 Git，请参阅 [Git 下载页面][git]。 ### 安装 GHC 和 Cabal {#install-ghc-and-cabal} Agda 是用 Haskell 写成的，所以为了安装它我们需要 _Glorious Haskell Compiler_ 和它的包管理器 _Cabal_。PLFA 应该在任何 >=8.10 的 GHC 版本下运行，在 8.10 和 9.2 版本下完成测试。我们建议使用 [ghcup][ghcup] 来安装两者。 在 `ghcup` 安装好之后，输入下列命令： ```bash ghcup install ghc 9.2.4 ghcup install cabal recommended ghcup set ghc 9.2.4 ghcup set cabal recommended ``` 或使用 `ghcup tui` 来『设置』合适的工具。 ### 安装 Agda {#install-agda} 安装 Agda 最简单的方法是通过 Cabal。PLFA 使用 Agda 版本 2.6.3。运行下面的命令： ```bash cabal update cabal install Agda-2.6.3 ``` 这一步会消耗很长时间和很多内存来完成。 如果你遇到了问题，或者想参考替代的方法，可参阅 [Agda 安装指引][agda-readthedocs-installation]。 如果你愿意，你可以[测试 Agda 是否已正确安装][agda-readthedocs-hello-world]。 ### 安装 PLFA 和 Agda 标准库 {#install-plfa-and-the-agda-standard-library} 我们建议您使用下面的命令把 PLFA 安装至你的家目录： ```bash git clone --depth 1 --recurse-submodules --shallow-submodules https://github.com/plfa/plfa.github.io plfa ``` PLFA 包括了所需要的 Agda 标准库版本，如果你在克隆时使用了 `--recurse-submodule` 选项，你在 `standard-library` 文件夹中已经有了 Agda 标准库！ 最后，我们需要让 Agda 知道如何找到标准库。 你需要两个配置文件，一个用于指定库的路径，一个用于指定默认载入的库。 在 macOS 和 Unix 上，如果 PLFA 已经安装至家目录，且你没有希望保存的配置文件，运行下面的命令： ```bash 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-readthedocs-package-system]。 ## 设置 Agda 的编辑器 ### Emacs 推荐的 Agda 编辑器是 Emacs。安装 Emacs 可以用下面的方法： - __UNIX 平台__：包管理器中的 Emacs 应该可以使用（只要它的版本比较新），[GNU Emacs 下载页面][emacs]也有最近发布版本的链接。 - __MacOS 平台__：推荐的 Emacs 是 [Aquamacs][aquamacs]，但是 GNU Emacs 也可以通过 Homebrew 或者 MacPorts 安装。参阅 [GNU Emacs 下载页面][emacs]中的指示。 - __Windows 平台__：参阅 [GNU Emacs 下载页面][emacs]中的指示。 确保你可以用你安装的版本打开、编辑、保存文件。GNU Emacs 网站上的 [Emacs 向导][emacs-tour]描述了如果打开 Emacs 安装中的教程。 Agda 自带了 Emacs 编辑器支持，如果你安装了 Agda，运行下面的命令来配置 Emacs： ```bash agda-mode setup agda-mode compile ``` 如果你已经是 Emacs 用户，并有自己的设置，你会注意到 `setup` 命令向你的 `.emacs` 文件中追加了配置，来配合你已有的设置。 加上 `agda-mode`。Agda 自带了 `agda-mode`， 因此如果你已经安装了 Agda，那么之需要运行以下命令就能配置好 `agda-mode` 了： #### 检查 `agda-mode` 是否正确安装 打开之前创建的 `nats.agda` 文件，使用 [`C-c C-l`][agda-readthedocs-emacs-notation] 来载入和类型检查这个文件。 #### 在 Emacs 中自动加载 `agda-mode` 从版本 2.6.0 开始，Agda 支持 Markdown 风格的文学编程，文件使用 `.lagda.md` 扩展名。 该扩展名的一个问题就是 Emacs 默认会进入 Markdown 编辑模式。 而为了让 `agda-mode` 在你打开 `.agda` 或 `.lagda.md` 文件时自动加载， 请将以下内容放到你的 Emacs 配置文件中： ```elisp ;; 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 文档][emacs-home] 来寻找配置文件的位置。 #### 可选：在 Emacs 中使用 Mononoki 字体 Agda 中的很多重要符号是用 Unicode 来表示的，因此用来显示和编辑 Agda 的字体需要正确地显示这些符号。最重要的是你使用的字体需要有好的 Unicode 字符支持。我们推荐 [Mononoki][font-mononoki]， 其他的备选字体有 [Source Code Pro][font-sourcecodepro]、 [DejaVu Sans Mono][font-dejavusansmono] 和 [FreeMono][font-freemono]。 你可以直接从[此网站][font-mononoki] 下载并安装 Mononoki。对于大多数系统来说，安装字体只是简单的下载 `.otf` 或者 `.ttf` 文件。 如果你的包管理器提供了 Mononoki 的包，那样可能更加简单。 例如，macOS 的 Homebrew 提供了 `font-mononiki` 包；Debian 的 APT 提供了 `fonts-mononoki` 包。 将下面的内容加入 Emacs 配置文件，可以把 Mononoki 设置为 Emacs 的默认字体： ```elisp ;; default to mononoki (set-face-attribute 'default nil :family "mononoki" :height 120 :weight 'normal :width 'normal) ``` #### 在 Emacs 中使用 `agda-mode` 要加载文件并对其执行类型检查，请使用 [`C-c C-l`][agda-readthedocs-emacs-notation]。 Agda 的编辑是通过使用「[洞][agda-readthedocs-holes]」来交互的，它表示程序中尚未填充的片段。 如果用问号作为表达式，并用 `C-c C-l` 加载缓冲区，Agda 会将问号替换为一个「洞」。 当光标在洞中时，你可以做以下这些事情： - `C-c C-c`: 分项（询问变量名，**c**ase） - `C-c C-空格`：填洞 - `C-c C-r`：用构造子精化（**r**efine） - `C-c C-a`：自动填洞（**a**utomatic） - `C-c C-,`：目标类型和上下文 - `C-c C-.`：目标类型，上下文，以及推断的类型 更多细节请见 [emacs-mode 文档][agda-readthedocs-emacs-mode]。 如果你想在 Agda 代码的侧边而非底栏查看信息，那么可以这样做： - 打开 Agda 文件并按 `C-c C-l`； - 按 `C-x 1` 来仅显示当前 Agda 文件； - 按 `C-x 3` 来垂直分割窗口； - 将光标移动到右侧窗口； - 按 `C-x b` 并输入「Agda information」切换到该缓冲区。 现在，Agda 的错误消息将会在代码右侧显示，而非被挤压在底部的狭小空间里。 #### 在 Emacs 中使用 `agda-mode` 输入 Unicode 字符 当你书写 Agda 代码时，你需要输入标准键盘上没有的字符。Emacs 的「Agda-mode」定义了字符翻译来让这件事更容易：当你输入特定普通字符的序列时，Emacs 会在 Agda 文件中使用对应的特殊字符来替换。 例如，我们可以在之前的 `.agda` 测试文件中加入一条注释。 比如说，我们想要加入下面的注释： ```agda {- I am excited to type and → and ≤ and ≡ !! -} ``` 前几个字符都是普通字符，我们可以如往常的方式输入它们…… ```agda {- I am excited to type ``` 在最后一个空格之后，我们无法在键盘上找到 这个键。这个字符的输入序列是四个字符 `\all`，所以我们输入这四个字符，当我们完成时，Emacs 会把它们替换成我们想要的…… ```agda {- I am excit ... ...

近期下载者：

相关文件：

评论：[我要评论] [举报此文件]

收藏者：