Home Explore Blog Models CI



nixpkgs

2nd chunk of `doc/languages-frameworks/agda.section.md`
d8b105a40974e850c184f1c8e6f7c1035a9dbd3b60a2fe4e0000000100000df2
  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:

* `libraryName` should be the name that appears in the `*.agda-lib` file, defaulting to `pname`.
* `libraryFile` should be the file name of the `*.agda-lib` file, defaulting to `${libraryName}.agda-lib`.

Here is an example `default.nix`

```nix
{
  nixpkgs ? <nixpkgs>,
}:
with (import nixpkgs { });
agdaPackages.mkDerivation {
  version = "1.0";
  pname = "my-agda-lib";
  src = ./.;
  buildInputs = [ agdaPackages.standard-library ];
}
```

### Building Agda packages {#building-agda-packages}

The default build phase for `agdaPackages.mkDerivation` runs `agda --build-library`.
If something else is needed to build the package (e.g. `make`) then the `buildPhase` should be overridden.
Additionally, a `preBuild` or `configurePhase` can be used if there are steps that need to be done prior to checking the library.
`agda` and the Agda libraries contained in `buildInputs` are made available during the build phase.

### Installing Agda packages {#installing-agda-packages}

The default install phase copies Agda source files, Agda interface files (`*.agdai`) and `*.agda-lib` files to the output directory.
This can be overridden.

By default, Agda sources are files ending on `.agda`, or literate Agda files ending on `.lagda`, `.lagda.tex`, `.lagda.org`, `.lagda.md`, `.lagda.rst`. The list of recognised Agda source extensions can be extended by setting the `extraExtensions` config variable.

## Maintaining the Agda package set on Nixpkgs {#maintaining-the-agda-package-set-on-nixpkgs}

We are aiming at providing all common Agda libraries as packages on `nixpkgs`,
and keeping them up to date.
Contributions and maintenance help is always appreciated,
but the maintenance effort is typically low since the Agda ecosystem is quite small.

The `nixpkgs` Agda package set tries to take up a role similar to that of [Stackage](https://www.stackage.org/) in the Haskell world.
It is a curated set of libraries that:

1. Always work together.
2. Are as up-to-date as possible.

While the Haskell ecosystem is huge, and Stackage is highly automated,
the Agda package set is small and can (still) be maintained by hand.

### Adding Agda packages to Nixpkgs {#adding-agda-packages-to-nixpkgs}

To add an Agda package to `nixpkgs`, the derivation should be written to `pkgs/development/libraries/agda/${library-name}/default.nix` and an entry should be added to `pkgs/top-level/agda-packages.nix`. Here it is called in a scope with access to all other Agda libraries, so the derivation could look like:

```nix
{
  mkDerivation,
  standard-library,

Title: Agda Library Management, Compilation, and Nixpkgs Contributions
Summary
This section details how to manage Agda libraries, compile Agda modules, and contribute Agda packages to Nixpkgs. It begins by concluding the methods for Agda to recognize libraries (CLI flags, `*.agda-lib` files, or `~/.agda/defaults`). It then explains how to compile Agda modules using the GHC backend, including options to specify a GHC version or install Agda without GHC. For creating Nix derivations for Agda libraries, the document describes `agdaPackages.mkDerivation`, its arguments (`libraryName`, `libraryFile`), and provides an example. It covers default build/install phases, how to override them, and how Agda source files are recognized. Finally, it discusses maintaining the Agda package set on Nixpkgs, comparing it to Haskell's Stackage, and provides instructions for adding new Agda packages to Nixpkgs, specifying file locations and derivation structure.