安装¶
有多种可以安装 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 可能会继续使用原来编译的文件。
预构建包与特定系统的指南¶
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-counting
为False
,那么--count-clusters
选项会触发一条错误信息。 默认关闭。