Installation

There are several ways to install Agda:

Agda can be installed using different flags (see Installation Flags).

Installation from Hackage

You can install the latest released version of Agda from Hackage. Install the prerequisites and then run the following commands:

cabal update
cabal install Agda
agda-mode setup

The last command tries to set up Emacs for use with Agda via the Emacs mode. As an alternative you can copy the following text to your .emacs file:

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

It is also possible (but not necessary) to compile the Emacs mode’s files:

agda-mode compile

This can, in some cases, give a noticeable speedup.

Warning: If you reinstall the Agda mode without recompiling the Emacs Lisp files, then Emacs may continue using the old, compiled files.

Prebuilt Packages and System-Specific Instructions

Arch Linux

The following prebuilt packages are available:

Debian / Ubuntu

Prebuilt packages are available for Debian testing/unstable and Ubuntu from Karmic onwards. To install:

apt-get install agda-mode

This should install Agda and the Emacs mode.

The standard library is available in Debian testing/unstable and Ubuntu from Lucid onwards. To install:

apt-get install agda-stdlib

More information:

Reporting bugs:

Please report any bugs to Debian, using:

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

Fedora

Agda is packaged in Fedora (since before Fedora 18).

yum install Agda

will pull in emacs-agda-mode and ghc-Agda-devel.

FreeBSD

Packages are available from FreshPorts for Agda and Agda standard library.

NixOS

Agda is part of the Nixpkgs collection that is used by https://nixos.org/nixos. To install Agda and agda-mode for Emacs, type:

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

If you’re just interested in the library, you can also install the library without the executable. The Agda standard library is currently not installed automatically.

OS X

Homebrew provides prebuilt packages for OS X. To install:

brew install agda

This should take less than a minute, and install Agda together with the Emacs mode and the standard library.

By default, the standard library is installed in /usr/local/lib/agda/. To use the standard library, it is convenient to add /usr/local/lib/agda/standard-library.agda-lib to ~/.agda/libraries, and specify standard-library in ~/.agda/defaults. Note this is not performed automatically.

It is also possible to install --without-stdlib, --without-ghc, or from --HEAD. Note this will require building Agda from source.

For more information, refer to the Homebrew documentation.

Note

If Emacs cannot find the agda-mode executable, it might help to install the exec-path-from-shell package by doing M-x package-install RET exec-path-from-shell RET, and adding

(exec-path-from-shell-initialize)

to your .emacs file.

Installation of the Development Version

After getting the development version following the instructions in the Agda wiki:

  • Install the prerequisites

  • In the top-level directory of the Agda source tree

    • Follow the instructions for installing Agda from Hackage (except run cabal install instead of cabal install Agda) or

    • You can try to install Agda (including a compiled Emacs mode) by running the following command:

      make install
      

      Note that on a Mac, because ICU is installed in a non-standard location, you need to specify this location on the command line:

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

Installation Flags

When installing Agda the following flags can be used:

cpphs
Use cpphs instead of cpp. Default: off.
debug
Enable debugging features that may slow Agda down. Default: off.
flag enable-cluster-counting
Enable the --count-clusters flag (see Counting Extended Grapheme Clusters). Note that if enable-cluster-counting is False, then the --count-clusters flag triggers an error message. Default: off.