macOS

Open the terminal.app.
Install Homebrew, take the defaults, in particular let it install in /usr/local.
Install agda. Run:
```
 $ brew install agda
```
This will install agda and all its dependencies. In particular:
1. It will install GHC, a Haskell compiler.
2. It will install emacs: let it do it, it is necessary to satisfy a dependency, but you will install a better version in a moment.
3. It will install and compile the standard library. It is not needed for the lectures, but it is useful, and mandatory for many other things.
This should take less than a couple of minutes, but if homebrew starts compiling everything–which will take hours–see their FAQ.
Now you will install a windowed version of emacs. Run:
```
 $ brew cask install emacs-mac
```
This will install emacs as an app you can launch by double-clicking.
Now we need to make emacs aware of the agda installation. Run:
```
 $ agda-mode setup
```

Optional: make the standard library readily available to agda. Run the following commands:

 $ mkdir ~/.agda
 $ echo "/usr/local/lib/agda/standard-library.agda-lib" > ~/.agda/libraries
 $ echo "standard-libary" > ~/.agda/defaults

An alternative is to use Stack. If you are so inclined, see instructions below.

Linux

Using the native package manager

These instructions are tested on Ubuntu 20.04.1 LTS (Focal Fossa). It will install Agda version 2.6.0.1, which is slightly behind, but totally fine for our purposes.

Install agda using your system’s package manager: This will install agda and all its dependencies. In particular:
1. It will install GHC, a Haskell compiler.
2. It will install emacs if not previously installed
3. It will install and compile the standard library. It is not needed for the lectures, but it is useful, and mandatory for many other things.
4. It will take care of agda-mode, which will be packaged inside the emacs installation.
To install, run:
```
sudo apt install agda
```
on the command line.
If installed this way, there is no need to make emacs aware of the agda installation. You are fine.
The standard library files are installed and the library is fully functional.

One file, namely /usr/share/agda-stdlib/standard-library.agda-lib, only seems to be missing. But if you import the library it just works.

We are not going to use the standard library in the course in any significant way.

Using `Stack`

Stack gives a predictable build. See instructions below

Windows

There may be several alternatives:

See the references for installation instructions.
If running Windows 10, one can:
1. install one of the Linux distributions using the Windows Subsystem for Linux.
2. Install Agda following the Linux installation instructions.
Check out the documentation.
Use Stack

Using Stack

Check the instructions from Philip Wadler’s book. Make sure you have git.

Install stack:
1. On macOS: brew install haskell-stack
2. On Linux: if you are on Ubuntu, sudo apt install haskell-stack
3. On Windows: https://docs.haskellstack.org/en/stable/install_and_upgrade/#windows
Add ~/.local/bin to your PATH:
```
 $ echo "export PATH=~/.local/bin:$PATH" >> ~/.bashrc
 $ . ~/.bashrc
```
You only have to this once. You must figure out how to set environmental variables.

Get the Agda sources: either download the Zip archive or use git clone as follows:

 $ git clone https://github.com/agda/agda.git
 $ cd agda
 $ git checkout v2.6.1

stack install --stack-yaml stack-8.8.3.yaml

It will compile Agda and some of its prerequisites, so you are going to wait some time…

… and it will be very long if you are doing this in a virtual machine.
Run
```
 $ agda-mode setup
```

Optional: for the standard library, either download the Zip archive, or

 git clone https://github.com/agda/agda-stdlib.git
 cd agda-stdlib
 git checkout v1.3

Do not do this inside the agda directory you used to install Agda!

Thus, if you have the standard library in ~/agda-stdlib, then do the following:

 $ test ! -d ~/.agda && mkdir ~/.agda
 $ echo "~/agda-stdlib/standard-libary.agda-lib" >> ~/.agda/libraries
 $ echo "standard-library" >> ~/.agda/defaults