Installation¶
There are several ways to install Agda:
- Using a released source package from Hackage
- Using a binary package prepared for your platform
- Using the development version from the Git repository
Agda can be installed using different flags (see Installation Flags).
Installation from Hackage¶
After installing the prerequisites you can install the latest released version of Agda from Hackage.
Installing the agda
and the agda-mode
programs¶
Using cabal
¶
For installing the agda
and the agda-mode
programs using
cabal
run the following commands:
cabal update
cabal install Agda
If you use Nix-style Local Builds,
by using Cabal 3.0.0.0 or by running cabal v2-install
, you’ll get the
following error when compiling with the GHC backend:
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:
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:
cabal v2-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.
Using stack
¶
For installing the agda
and the agda-mode
programs using
stack
run the following commands:
cabal get Agda-X.Y.Z
cd Agda-X.Y.Z
stack --stack-yaml stack-a.b.c.yaml install
replacing X.Y.Z and a.b.c for the Agda version on Hackage and your GHC version, respectively.
Running the agda-mode
program¶
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.
Prebuilt Packages and System-Specific Instructions¶
Arch Linux¶
The following prebuilt packages are available:
However, due to significant packaging bugs [such as this](https://bugs.archlinux.org/task/61904?project=5&string=agda), you might want to use alternative installation methods.
Debian / Ubuntu¶
Prebuilt packages are available for Debian 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 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 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 command:
brew install agda
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 /usr/local/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 keywords
--without-stdlib
, --without-ghc
, or from --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.
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 ofcabal install Agda
) orYou 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:
-
debug
¶
Enable debugging features that may slow Agda down. Default: off.
-
enable-cluster-counting
¶
Enable the
--count-clusters
flag. Note that ifenable-cluster-counting
isFalse
, then the--count-clusters
flag triggers an error message. Default: off.