# Agda {#agda}

## How to use Agda {#how-to-use-agda}

Agda is available as the [agda](https://search.nixos.org/packages?channel=unstable&show=agda&from=0&size=30&sort=relevance&query=agda)
package.

The `agda` package installs an Agda-wrapper, which calls `agda` with `--library-file`
set to a generated library-file within the nix store, this means your library-file in
`$HOME/.agda/libraries` will be ignored. By default the agda package installs Agda
with no libraries, i.e. the generated library-file is empty. To use Agda with libraries,
the `agda.withPackages` function can be used. This function either takes:

* A list of packages,
* or a function which returns a list of packages when given the `agdaPackages` attribute set,
* or an attribute set containing a list of packages and a GHC derivation for compilation (see below).
* or an attribute set containing a function which returns a list of packages when given the `agdaPackages` attribute set and a GHC derivation for compilation (see below).

For example, suppose we wanted a version of Agda which has access to the standard library. This can be obtained with the expressions:

```nix
agda.withPackages [ agdaPackages.standard-library ]
```

or

```nix
agda.withPackages (p: [ p.standard-library ])
```

or can be called as in the [Compiling Agda](#compiling-agda) section.

If you want to use a different version of a library (for instance a development version)
override the `src` attribute of the package to point to your local repository

```nix
agda.withPackages (p: [
  (p.standard-library.overrideAttrs (oldAttrs: {
    version = "local version";
    src = /path/to/local/repo/agda-stdlib;
  }))
])
```

You can also reference a GitHub repository

```nix
agda.withPackages (p: [
  (p.standard-library.overrideAttrs (oldAttrs: {
    version = "1.5";
    src = fetchFromGitHub {
      repo = "agda-stdlib";
      owner = "agda";
      rev = "v1.5";
      hash = "sha256-nEyxYGSWIDNJqBfGpRDLiOAnlHJKEKAOMnIaqfVZzJk=";
    };
  }))
])
```

If you want to use a library not added to Nixpkgs, you can add a
dependency to a local library by calling `agdaPackages.mkDerivation`.

```nix
agda.withPackages (p: [
  (p.mkDerivation {
    pname = "your-agda-lib";
    version = "1.0.0";
    src = /path/to/your-agda-lib;
  })
])
```

Again you can reference GitHub

```nix
agda.withPackages (p: [
  (p.mkDerivation {
    pname = "your-agda-lib";
    version = "1.0.0";
    src = fetchFromGitHub {
      repo = "repo";
      owner = "owner";
      version = "...";
      rev = "...";
      hash = "...";
    };
  })
])
```

See [Building Agda Packages](#building-agda-packages) for more information on `mkDerivation`.

Agda will not by default use these libraries. To tell Agda to use a library we have some options:

* Call `agda` with the library flag:
  ```ShellSession
  $ agda -l standard-library -i . MyFile.agda
  ```
* Write a `my-library.agda-lib` file for the project you are working on which may look like:
  ```
  name: my-library
  include: .
  depend: standard-library
  ```
* Create the file `~/.agda/defaults` and add any libraries you want to use by default.

More information can be found in the [official Agda documentation on library management](https://agda.readthedocs.io/en/v2.6.1/tools/package-system.html).

## Compiling Agda {#compiling-agda}

Agda modules can be compiled using the GHC backend with the `--compile` flag. A version of `ghc` with `ieee754` is made available to the Agda program via the `--with-compiler` flag.
This can be overridden by a different version of `ghc` as follows:

```nix
agda.withPackages {
  pkgs = [
    # ...
  ];
  ghc = haskell.compiler.ghcHEAD;
}
```

To install Agda without GHC, use `ghc = null;`.

## Writing Agda packages {#writing-agda-packages}

To write a nix derivation for an Agda library, first check that the library has a (single) `*.agda-lib` file.

A derivation can then be written using `agdaPackages.mkDerivation`. This has similar arguments to `stdenv.mkDerivation` with the following additions: