安装

有多种可以安装 Agda 的方式:

Agda 可使用不同的选项安装(见 安装选项)。

从 Hackage 安装

你可以从 Hackage 安装 Agda 的最新发行版。 请先安装 前提需求 所述软件,然后运行以下命令:

cabal update
cabal install Agda
agda-mode setup

最后一条命令会尝试设置 Emacs,使其可以通过 Emacs 模式 使用 Agda。还有一种方法,即将以下文本复制到你的 .emacs 文件中:

(load-file (let ((coding-system-for-read 'utf-8))
                (shell-command-to-string "agda-mode locate")))

你还可以编译 Emacs 模式的文件(非必须):

agda-mode compile

有时这样可以显著提高速度。

警告:如果你重新安装了 Agda 模式但没有重新编译 Emacs Lisp 文件,那么 Emacs 可能会继续使用原来编译的文件。

预构建包与特定系统的指南

Arch Linux

以下预构建包可直接获取:

Debian / Ubuntu

预构建包可在 Debian 的测试/不稳定版和 Ubuntu Karmic 之后的版本上使用。请执行以下命令:

apt-get install agda-mode

这样会安装 Agda 及其 Emacs 模式。

标准库可在 Debian 的测试/不稳定版和 Ubuntu Lucid 之后的版本上使用。请执行以下命令安装:

apt-get install agda-stdlib

更多信息:

问题报告:

请报告任何在 Debian 上出现的问题,可使用以下命令:

reportbug -B debian agda
reportbug -B debian agda-stdlib

Fedora

Agda 已在 Fedora 上打包(从 Fedora 18 开始)。执行

yum install Agda

会安装 emacs-agda-mode 和 ghc-Agda-devel。

FreeBSD

Agda 及其标准库可从 FreshPorts 获取。

NixOS

Agda 为 https://nixos.org/nixos 使用的 Nixpkgs 合集的一部分,要为 Emacs 安装 Agda 和 agda-mode,请执行:

nix-env -f "<nixpkgs>" -iA haskellPackages.Agda

如果你只关心标准库,那么也可以只安装不带可执行程序的库。Agda 标准库当前不会自动安装。

OS X

Homebrew 为 OS X 提供了预构建的包。请执行以下命令安装:

brew install agda

应该不到一分钟就能安装好 Agda 以及 Emacs 模式和标准库。

默认情况下,标准库会被安装到 /usr/local/lib/agda/。要使用标准库, 将 /usr/local/lib/agda/standard-library.agda-lib 添加到 ~/.agda/libraries,并在 ~/.agda/defaults 中指定 standard-library 会十分方便。注意这些并不会继续执行。

当然,也可以指定 --without-stdlib--without-ghc--HEAD 选项来安装。 注意,这需要从源码构建 Agda。

更多信息请参阅 Homebrew 文档

注解

如果 Emacs 找不到 agda-mode 可执行程序,那么可以通过 M-x package-install RET exec-path-from-shell RET 来安装 exec-path-from-shell 包, 之后在你的 .emacs 文件中添加

(exec-path-from-shell-initialize)

安装开发版

请访问 Agda wiki 获得开发版, 之后执行以下步骤:

  • 安装前提需求中列出的软件

  • 在 Agda 源码树的顶层目录中

    • 按照说明从 Hackage 安装 Agda (请执行 cabal install 而非 cabal install Agda),或者

    • 你可以运行以下命令来安装 Agda(包括编译版的 Emacs 模式):

      make install
      

      注意在 Mac 上,由于 ICU 安装在了非标准目录中,因此你需要在命令行中指定它的位置:

      make install-bin CABAL_OPTS='--extra-lib-dirs=/usr/local/opt/icu4c/lib --extra-include-dirs=/usr/local/opt/icu4c/include'
      

安装选项

在安装 Agda 时可指定以下命令行选项:

cpphs
使用 cpphs 代替 cpp。默认关闭。
debug
开启调试特性可能会减慢 Agda 的速度。默认关闭。
flag enable-cluster-counting
开启 --count-clusters 选项(见 Counting Extended Grapheme Clusters)。注意若 enable-cluster-countingFalse,那么 --count-clusters 选项会触发一条错误信息。 默认关闭。