Installation

To get started with Agda, follow these three steps:

In case of installation problems, check the section on troubleshooting.

Hint

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

Step 1: Install Agda

There are at least three options for installing Agda:

Option 2: Install the Development Version of Agda from Source (for advanced users)

If you want to work on the Agda compiler itself, or you want to work with the very latest version of Agda, then you can compile it from source from the Github repository.

You should have GHC and Cabal installed (if not see the instructions in Option 1: Install Agda as a Haskell Package (recommended)).

Note

For the development version enable-cluster-counting is on by default, so unless you turn it off (see Installation Flags, below), you also need to install the ICU library.

Install alex and happy dependencies

Agda depends on the alex and happy tools, but depending on your system and version of Cabal these might not be installed automatically. You can use Cabal to install them manually:

cabal update
cabal install alex happy

Build Agda using Cabal

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

cabal update
make install

Build Agda using Stack

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:

cp stack-8.10.7.yaml stack.yaml
make install

Option 3: Install Agda as a Prebuilt Package

Packaged Agda binaries and the Agda standard library are provided by various package managers. Installing Agda binaries can be faster than installing Agda from source, but installation problems might be harder to work around.

An OS-independent binary installation of Agda is provided by the python installer.

Warning

Depending on the system, prebuilt packages may not contain the latest release of Agda. See repology for a list of Agda versions available on various package managers.

See Prebuilt Packages and System-Specific Instructions for a list of known systems and their system-specific instructions.

Step 2: Install the Agda Standard Library (agda-stdlib)

Most users will want to install the standard library. You can install this as any other Agda library (see Library Management). See the agda-stdlib project’s installation instructions for the steps to take to install the latest version.

Step 3: Install and Configure a Text Editor for Agda

Your choice of text editor matters more in Agda than it does in most other programming languages. This is because Agda code typically uses a lot of unicode symbols, and because you will typically interact with Agda through the text editor while writing your program.

The most common choice is Emacs. Other editors with interactive support for Agda include

Emacs

Emacs has good support for unicode input, and the agda-mode for emacs is maintained by the Agda developers in the main Agda repository and offers many advanced features.

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:

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:

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

Installation Reference

Troubleshooting

A Common Issue on Windows: Invalid Byte Sequence

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

hGetContents: invalid argument (invalid byte sequence)

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

CHCP 65001

A Common Issue: Missing ieee754 Dependency

You may get the following error when compiling with the GHC backend:

Compilation error:

MAlonzo/RTE/Float.hs:6:1: error:
    Failed to load interface for ‘Numeric.IEEE’
    Use -v to see a list of the files searched for.

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

cabal install --lib Agda ieee754

This will register ieee754 in the GHC default environment.

Cabal install fails due to dynamic linking issues

If you have setting executable-dynamic: True in your cabal configuration then installation might fail on Linux and Windows.

Cure: change to default executable-dynamic: False.

Further information:

Agda and Haskell

Tested GHC Versions

Agda has been tested with GHC 8.6.5, 8.8.4, 8.10.7, 9.0.2, 9.2.8, 9.4.8, 9.6.6, 9.8.2, and GHC 9.10.1.

Installation Flags

When installing Agda the following flags can be used:

debug

Enable debug printing. This makes Agda slightly slower, and building Agda slower as well. The --verbose={N} option only has an effect when Agda was installed with this flag. Default: off.

debug-serialisation

Enable debug mode in serialisation. This makes serialisation slower. Default: off.

debug-parsing

Enable debug mode in the parser. This makes parsing slower. Default: off.

enable-cluster-counting

Enable cluster counting. This will require the text-icu Haskell library, which in turn requires that ICU be installed. Note that if enable-cluster-counting is False, then option --count-clusters triggers an error message when given to Agda. Default: off, but on for development version.

optimise-heavily

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

Hint

During cabal install you can add build flags using the -f argument: cabal install -fenable-cluster-counting. Whereas stack uses --flag and an Agda: prefix, like this: stack install --flag Agda:enable-cluster-counting.

Installing ICU

If cluster counting is enabled (see the enable-cluster-counting flag above, enabled by default), then you will need the ICU library to be installed. See the text-icu Prerequisites documentation for how to install ICU on your system.

Keeping the Default Environment Clean

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:

cabal install --package-env agda --lib Agda ieee754

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

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.

Installing Multiple Versions of Agda

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

cabal install Agda-2.6.4.3 --program-suffix=-2.6.4.3

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

C-c C-x C-s 2.6.4.3 RETURN

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

C-c C-x C-s RETURN

Prebuilt Packages and System-Specific Instructions

The recommended way to install Agda is through cabal, but in some cases you may want to use your system’s package manager instead:

Arch Linux

The following prebuilt packages are available:

In case of installation problems, please consult the issue tracker <https://gitlab.archlinux.org/archlinux/packaging/packages/agda/-/issues>_.

Debian / Ubuntu

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

apt install agda

This should install Agda and the Emacs mode.

The standard library is available in Debian 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 / EPEL (Centos)

Agda is packaged for Fedora Linux and EPEL. Agda-stdlib is available for Fedora.

dnf install Agda Agda-stdlib

will install Agda with the emacs mode and also agda-stdlib.

FreeBSD

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

GNU Guix

GNU Guix provides packages for both agda and agda-stdlib. You can install the latest versions by running:

guix install agda agda-stdlib

You can also install a specific version by running:

guix install agda@ver agda-stdlib@ver

where ver is a specific version number.

Packages Sources:

Nix or NixOS

Agda is part of the Nixpkgs collection that is used by https://nixos.org/nixos. Install Agda (and the standard library) via:

nix-env -f "<nixpkgs>" -iE "nixpkgs: (nixpkgs {}).agda.withPackages (p: [ p.standard-library ])"
agda-mode setup
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:

nix-env -f "<nixpkgs>" -iA agda
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.

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:

brew install agda
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:

mkdir -p ~/.agda
echo $(brew --prefix)/lib/agda/standard-library.agda-lib >> ~/.agda/libraries
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.

Python Installer (pip)

An OS-independent binary install of Agda is provided via the Python Installer:

pip install agda

Further information: https://pypi.org/project/agda/

Windows

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

  • Agda 2.6.0.1 bundled with Emacs 26.1

  • Agda 2.6.2.2 …

Warning

These are old versions of Agda. It would be much better to use the Agda as installed by cabal instead.