staging-next 2025-08-10 (#432489)

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

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

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:

* `everythingFile` can be used to specify the location of the `Everything.agda` file, defaulting to `./Everything.agda`. If this file does not exist then either it should be patched in or the `buildPhase` should be overridden (see below).

* `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`.

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

The default build phase for `agdaPackages.mkDerivation` runs `agda` on the `Everything.agda` file.

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 `Everything.agda` file.

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}

### 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}/` 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 top line of the `default.nix` can look like:

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

{

  standard-library,

  fetchFromGitHub,

}:

{ }

```

Note that the derivation function is called with `mkDerivation` set to `agdaPackages.mkDerivation`, therefore you

could use a similar set as in your `default.nix` from [Writing Agda Packages](#writing-agda-packages) with

`agdaPackages.mkDerivation` replaced with `mkDerivation`.

Here is an example skeleton derivation for iowa-stdlib:

```nix

mkDerivation {

  version = "1.5.0";

  pname = "iowa-stdlib";

  pname = "my-library";

  version = "1.0";

  src = <...>;

  libraryFile = "";

  libraryName = "IAL-1.3";

  buildPhase = ''

    runHook preBuild

    patchShebangs find-deps.sh

    make

    runHook postBuild

  '';

  buildInputs = [ standard-library ];

  meta = <...>;

}

```

This library has a file called `.agda-lib`, and so we give an empty string to `libraryFile` as nothing precedes `.agda-lib` in the filename. This file contains `name: IAL-1.3`, and so we let `libraryName =  "IAL-1.3"`. This library does not use an `Everything.agda` file and instead has a Makefile, so there is no need to set `everythingFile` and we set a custom `buildPhase`.

You can look at other files under `pkgs/development/libraries/agda/` for more inspiration.

Note that the derivation function is called with `mkDerivation` set to `agdaPackages.mkDerivation`, therefore you

could use a similar set as in your `default.nix` from [Writing Agda Packages](#writing-agda-packages) with

`agdaPackages.mkDerivation` replaced with `mkDerivation`.

When writing an Agda package it is essential to make sure that no `.agda-lib` file gets added to the store as a single file (for example by using `writeText`). This causes Agda to think that the nix store is a Agda library and it will attempt to write to it whenever it typechecks something. See [https://github.com/agda/agda/issues/4613](https://github.com/agda/agda/issues/4613).

you can test whether it builds correctly by writing in a comment:

```

@ofborg build agdaPackages.iowa-stdlib

@ofborg build agdaPackages.my-library

```

### Maintaining Agda packages {#agda-maintaining-packages}

- `space-orbit` package has been removed due to lack of upstream maintenance. Debian upstream stopped tracking it in 2011.

- Derivations setting both `separateDebugInfo` and one of `allowedReferences`, `allowedRequistes`, `disallowedReferences` or `disallowedRequisites` must now set `__structuredAttrs` to `true`. The effect of reference whitelisting or blacklisting will be disabled on the `debug` output created by `separateDebugInfo`.

- `victoriametrics` no longer contains VictoriaLogs components. These have been separated into the new package `victorialogs`.

- `mx-puppet-discord` was removed from nixpkgs along with its NixOS module as it was unmaintained and was the only user of sha1 hashes in tree.

- `kbd` package's `outputs` now include a `man` and `scripts` outputs. The `unicode_start` and `unicode_stop` Bash scripts are now part of the `scripts` output, allowing most usages of the `kbd` package to not pull in `bash`.

- `conduwuit` was removed due to upstream ceasing development and deleting their repository. For existing data, a migration to `matrix-conduit`, `matrix-continuwuity` or `matrix-tuwunel` may be possible.

- `gnome-keyring` no longer ships with an SSH agent anymore because it has been deprecated upstream. You should use `gcr_4` instead, which provides the same features. More information on why this was done can be found on [the relevant GCR upstream PR](https://gitlab.gnome.org/GNOME/gcr/-/merge_requests/67).

- `meta.mainProgram`: Changing this `meta` entry can lead to a package rebuild due to being used to determine the `NIX_MAIN_PROGRAM` environment variable.

- `lisp-modules` were brought in sync with the [June 2025 Quicklisp release](http://blog.quicklisp.org/2025/07/june-2025-quicklisp-dist-now-available.html).

- `searx` was updated to use `envsubst` instead of `sed` for parsing secrets from environment variables.

  If your previous configuration included a secret reference like `server.secret_key = "@SEARX_SECRET_KEY@"`, you must migrate to the new envsubst syntax: `server.secret_key = "$SEARX_SECRET_KEY"`.

        init

        crossLists

        unique

        uniqueStrings

        allUnique

        intersectLists

        subtractLists

      spdxId = "HPND-sell-variant";

    };

    hpndDoc = {

      fullName = "Historical Permission Notice and Disclaimer - documentation variant";

      spdxId = "HPND-doc";

    };

    hpndDocSell = {

      fullName = "Historical Permission Notice and Disclaimer - documentation sell variant";

      spdxId = "HPND-doc-sell";

    };

    hpndUc = {

      spdxId = "HPND-UC";

      fullName = "Historical Permission Notice and Disclaimer - University of California variant";

      # Marc Weber (small nix contributor)

    };

    tekHvcLicense = {

      fullName = "TekHVC License";

      url = "https://gitlab.freedesktop.org/xorg/lib/libx11/-/blob/7f8305c779ac6948d7261764f5ffb8ae9aa975b1/COPYING#L138-171";

      # TODO: add spdxId when it gets accepted to spdx

      # https://tools.spdx.org/app/license_requests/458

      # https://github.com/spdx/license-list-XML/issues/2757

    };

    tsl = {

      shortName = "TSL";

      fullName = "Timescale License Agreegment";

    warn

    pipe

    ;

  inherit (lib.attrsets) mapAttrs attrNames;

  inherit (lib.attrsets) mapAttrs;

  inherit (lib) max;

in

rec {

  /**

    Remove duplicate elements from the `list`. O(n^2) complexity.

    :::{.note}

    If the list only contains strings and order is not important, the complexity can be reduced to O(n log n) by using [`lib.lists.uniqueStrings`](#function-library-lib.lists.uniqueStrings) instead.

    :::

    # Inputs

    `list`

  */

  unique = foldl' (acc: e: if elem e acc then acc else acc ++ [ e ]) [ ];

  /**

    Removes duplicate strings from the `list`. O(n log n) complexity.

    :::{.note}

    Order is not preserved.

    All elements of the list must be strings without context.

    This function fails when the list contains a non-string element or a [string with context](https://nix.dev/manual/nix/latest/language/string-context.html).

    In that case use [`lib.lists.unique`](#function-library-lib.lists.unique) instead.

    :::

    # Inputs

    `list`

    : List of strings

    # Type

    ```

    uniqueStrings :: [ String ] -> [ String ]

    ```

    # Examples

    :::{.example}

    ## `lib.lists.uniqueStrings` usage example

    ```nix

    uniqueStrings [ "foo" "bar" "foo" ]

    => [ "bar" "foo" ] # order is not preserved

    ```

    :::

  */

  uniqueStrings = list: attrNames (groupBy id list);

  /**

    Check if list contains only unique elements. O(n^2) complexity.