Installation

Hint

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

Hint

This documentation is for first-time Agda users. More advanced “do it yourself” instructions can be found in the Agda repo’s HACKING.md file.

Step 1: Install Agda

You can get the Agda type-checker in at least 4 ways:

Option 1: From GitHub releases

Pre-built agda binaries are available for the following platforms:

  • Windows (x86-64)

  • Linux (x86-64, statically linked)

  • macOS (x86-64)

  • macOS (arm64, i.e. Apple M-series)

They can be downloaded from the Agda GitHub releases page (under “Assets”).

To install, download the appropriate archive, extract the binary, and place it in a directory listed in your PATH environment variable.

Option 2: From source

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.

Both cabal install-based and nix build-based developer builds are maintained.

Miscellaneous developer information is available in the repository’s HACKING.md.

Option 3: From package manager

agda binaries are distributed by various package managers, but are often out of date. Repology.org maintains a list:

As well as the repositories tracked by repology, an OS-independent binary installation of Agda is provided by the python installer.

Option 4: From text editor

Some text editor extensions (e.g. banacorn.agda-mode for VSCode) can install Agda on their own.

Step 2: Configure a text editor

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.

Editors with interactive support for Agda include:

Step 3: Install agda-stdlib (optional)

You may want to install Agda’s standard library, although Agda will work without it.

You can install this like 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 4: Install ghc (optional)

To compile your Agda code to an executable, agda calls the Haskell compiler ghc, which is not bundled with most Agda distributions. You can install ghc spearately with e.g. GHCUp.

No separate programs are called by Agda’s JavaScript backend.