Installation

There are several ways to install Agda:

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

Hint

If you want a sneak peek of Agda without installing it, try the Agda Pad

Installation from source

Step 1 : Prerequisites

You need recent versions of the following programs to compile Agda:

You should also make sure that programs installed by cabal-install are on your shell’s search path. The installation location is described by field installdir in the cabal configuration (check ~/.cabal/config; it defaults to ~/.cabal/bin). So, e.g. under Ubuntu or macOS, you may need to add

  1. export PATH=~/.cabal/bin:$PATH

to your .profile or .bash_profile.

Non-Windows users need to ensure that the development files for the C libraries zlib and ncurses are installed (see http://zlib.net and http://www.gnu.org/software/ncurses/). Your package manager may be able to install these files for you. For instance, on Debian or Ubuntu it should suffice to run

  1. apt-get install zlib1g-dev libncurses5-dev

as root to get the correct files installed.

ICU and cluster counting

Optionally one can also install the ICU library, which is used to implement the --count-clusters option. Once the ICU library is installed and configured, one can enable the --count-clusters option by giving the enable-cluster-counting flag to cabal install:

  1. cabal install -f enable-cluster-counting

Information on installing the ICU prerequisite on various OSs is available at https://github.com/haskell/text-icu/blob/master/README.markdown#prerequisites (retrieved 2022-02-09).

  • Under Debian or Ubuntu it may suffice to install libicu-dev.

  • Under macOS, try brew install icu4c. Note that this installs ICU in a non-standard location. You may need to set

    1. export PKG_CONFIG_PATH="$(brew --prefix)/opt/icu4c/lib/pkgconfig"

    See brew info icu4c for details.

Step 2 : Installing the agda and the agda-mode programs

After installing the prerequisites you can install the latest released version of Agda from Hackage.

Using cabal

For installing the agda and the agda-mode programs using cabal run the following commands:

  1. cabal update
  2. cabal install Agda

If you use Nix-style Local Builds, by using Cabal ≥ 3.0 or by running cabal v2-install, you’ll get the following error when compiling with the GHC backend:

  1. Compilation error:
  3. MAlonzo/RTE.hs:13:1: error:
  4.     Failed to load interface for ‘Numeric.IEEE’
  5.     Use -v to see a list of the files searched for.

This is because packages are sandboxed in $HOME/.cabal/store and you have to explicitly register required packaged in a GHC environment. This can be done by running the following command:

  1. cabal v2-install --lib Agda ieee754

This will register ieee754 in the GHC default environment.

You may want to keep the default environment clean, e.g. to avoid conflicts with other installed packages. In this case you can a create separate Agda environment by running:

  1. cabal v2-install --package-env agda --lib Agda ieee754

You then have to set the GHC_ENVIRONMENT when you invoke Agda:

  1. GHC_ENVIRONMENT=agda agda -c hello-world.agda

Note

Actually it is not necessary to register the Agda library, but doing so forces Cabal to install the same version of ieee754 as used by Agda.

Warning

If you are installing Agda using Cabal on Windows, depending on your system locale setting, cabal install Agda may fail with an error message:

  1. hGetContents: invalid argument (invalid byte sequence)

If this happens, you can try changing the console code page to UTF-8 using the command:

  1. CHCP 65001

Using stack

For installing the agda and the agda-mode programs using stack run the following commands:

  1. cabal get Agda-X.Y.Z
  2. cd Agda-X.Y.Z
  3. stack --stack-yaml stack-x.y.z.yaml install

replacing X.Y.Z by the Agda version on Hackage and x.y.z by your GHC version, respectively.

Step 3 : Running the agda-mode program

Warning: Installing agda-mode via melpa is discouraged. It is strongly advised to install agda-mode for emacs as described below:

After installing the agda-mode program using cabal or stack run the following command:

  1. agda-mode setup

The above 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:

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

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

  1. 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.

Step 4 : Installing the standard library

Installing the standard library, should you choose to use it, is an additional step using a separate repository.

Prebuilt Packages and System-Specific Instructions

Warning : Depending on the system, prebuild packages may not be the last release. See https://repology.org/project/agda/versions.

Arch Linux

The following prebuilt packages are available:

However, due to significant packaging bugs such as this, you might want to use alternative installation methods.

Debian / Ubuntu

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

  1. apt-get install agda agda-mode

This should install Agda and the Emacs mode.

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

  1. apt-get install agda-stdlib

More information:

Reporting bugs:

Please report any bugs to Debian, using:

  1. reportbug -B debian agda
  2. reportbug -B debian agda-stdlib

Fedora

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

  1. 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.

Nix or NixOS

Agda is part of the Nixpkgs collection that is used by https://nixos.org/nixos. There are two ways to install Agda from nix:

  • The new way: If you are tracking nixos-unstable or nixpkgs-unstable (the default on MacOS) or you are using NixOS version 20.09 or above then you should be able to install Agda (and the standard library) via:

    1. nix-env -f "<nixpkgs>" -iE "nixpkgs: (nixpkgs {}).agda.withPackages (p: [ p.standard-library ])"
    2. agda-mode setup
    3. echo "standard-library" > ~/.agda/defaults

    The second command tries to set up the Agda emacs mode. Skip this if you don’t want to set up the emacs mode. See Installation from source above for more details about agda-mode setup. The third command sets the standard-library as a default library so it is always available to Agda. If you don’t want to do this you can omit this step and control library imports on a per project basis using an .agda-lib file in each project root.

    If you don’t want to install the standard library via nix then you can just run:

    1. nix-env -f "<nixpkgs>" -iA agda
    2. agda-mode setup

    For more information on the Agda infrastructure in nix, and how to manage and develop Agda libraries with nix, see https://nixos.org/manual/nixpkgs/unstable/#agda. In particular, the agda.withPackages function can install more libraries than just the standard library. Alternatively, see Library Management for how to manage libraries manually.

  • The old way (deprecated): As Agda is a Haskell package available from Hackage you can install it like any other Haskell package:

    1. nix-env -f "<nixpkgs>" -iA haskellPackages.Agda
    2. agda-mode setup

    This approach does not provide any additional support for working with Agda libraries. See Library Management for how to manage libraries manually. It also suffers from this open issue which the ‘new way’ does not.

Nix is extremely flexible and we have only described how to install Agda globally using nix-env. One can also declare which packages to install globally in a configuration file or pull in Agda and some relevant libraries for a particular project using nix-shell.

The Agda git repository is a Nix flake to allow using a development version with Nix. The flake has the following outputs:

  • overlay: A nixpkgs overlay which makes haskellPackages.Agda (which the top-level agda package depends on) be the build of the relevant checkout.

  • haskellOverlay: An overlay for haskellPackages which overrides the Agda attribute to point to the build of the relevant checkout. This can be used to make the development version available at a different attribute name, or to override Agda for an alternative haskell package set.

OS X

Homebrew is a free and open-source software package management system that provides prebuilt packages for OS X. Once it is installed in your system, you are ready to install agda. Open the Terminal app and run the following commands:

  1. brew install agda
  2. agda-mode setup

This process should take less than a minute, and it installs Agda together with its Emacs mode and its standard library. For more information about the brew command, please refer to the Homebrew documentation and Homebrew FAQ.

By default, the standard library is installed in the folder /usr/local/lib/agda/. To use the standard library, it is convenient to add the location of the agda-lib file /usr/local/lib/agda/standard-library.agda-lib to the ~/.agda/libraries file, and write the line standard-library in the ~/.agda/defaults file. To do this, run the following commands:

  1. mkdir -p ~/.agda
  2. echo $(brew --prefix)/lib/agda/standard-library.agda-lib >>~/.agda/libraries
  3. echo standard-library >>~/.agda/defaults

Please note that this configuration is not performed automatically. You can learn more about using the standard library or using a library in general.

It is also possible to install with the command-line option keyword --HEAD. This requires building Agda from source.

To configure the way of editing agda files, follow the section Emacs mode.

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 the line (exec-path-from-shell-initialize) to your .emacs file.

Windows

A precompiled version of Agda 2.6.0.1 bundled with Emacs 26.1 with the necessary mathematical fonts, is available at http://www.cs.uiowa.edu/~astump/agda.

Installation of the Development Version

After getting the development version from the Git repository

  • Install the prerequisites. Note that for the development version enable-cluster-counting is on by default, so unless you manage to turn it off, you also need to install the ICU library.

  • In the top-level directory of the Agda source tree, run:

    1. cabal update
    2. make install

    To install via stack instead of cabal, copy one of the stack-x.y.z.yaml files of your choice to a stack.yaml file before running make. For example:

    1. cp stack-8.10.7.yaml stack.yaml
    2. make install

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.

enable-cluster-counting

Enable the Agda option --count-clusters. Note that if enable-cluster-counting is False, then option --count-clusters triggers an error message when given to Agda. Default: off.

optimise-heavily

Optimise Agda heavily. (In this case it might make sense to limit GHC’s memory usage.) Default: off.

Installing multiple versions of Agda

Multiple versions of Agda can be installed concurrently by using the –program-suffix flag. For example:

  1. cabal install Agda-2.6.1 --program-suffix=-2.6.1

will install version 2.6.1 under the name agda-2.6.1. You can then switch to this version of Agda in Emacs via

  1. C-c C-x C-s 2.6.1 RETURN

Switching back to the standard version of Agda is then done by:

  1. C-c C-x C-s RETURN