Home Explore Blog CI



nixpkgs

4th chunk of `doc/languages-frameworks/agda.section.md`
e25f4a03b44e1f91ecb0359102972c0ca986e6be0ed433260000000100000b86
mkDerivation {
  version = "1.5.0";
  pname = "iowa-stdlib";

  src = <...>;

  libraryFile = "";
  libraryName = "IAL-1.3";

  buildPhase = ''
    runHook preBuild

    patchShebangs find-deps.sh
    make

    runHook postBuild
  '';
}
```

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

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).

In the pull request adding this library,
you can test whether it builds correctly by writing in a comment:

```
@ofborg build agdaPackages.iowa-stdlib
```

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

As mentioned before, the aim is to have a compatible, and up-to-date package set.
These two conditions sometimes exclude each other:
For example, if we update `agdaPackages.standard-library` because there was an upstream release,
this will typically break many reverse dependencies,
i.e. downstream Agda libraries that depend on the standard library.
In `nixpkgs` we are typically among the first to notice this,
since we have build tests in place to check this.

In a pull request updating e.g. the standard library, you should write the following comment:

```
@ofborg build agdaPackages.standard-library.passthru.tests
```

This will build all reverse dependencies of the standard library,
for example `agdaPackages.agda-categories`, or `agdaPackages.generic`.

In some cases it is useful to build _all_ Agda packages.
This can be done with the following Github comment:

```
@ofborg build agda.passthru.tests.allPackages
```

Sometimes, the builds of the reverse dependencies fail because they have not yet been updated and released.
You should drop the maintainers a quick issue notifying them of the breakage,
citing the build error (which you can get from the ofborg logs).
If you are motivated, you might even send a pull request that fixes it.
Usually, the maintainers will answer within a week or two with a new release.
Bumping the version of that reverse dependency should be a further commit on your PR.

In the rare case that a new release is not to be expected within an acceptable time,
mark the broken package as broken by setting `meta.broken = true;`.
This will exclude it from the build test.
It can be added later when it is fixed,
and does not hinder the advancement of the whole package set in the meantime.

Title: Testing, Building, and Maintaining Agda Packages in Nixpkgs
Summary
This section details how to test and maintain Agda packages within Nixpkgs. It includes commands to test specific packages or their reverse dependencies using `@ofborg`, and how to handle breakages caused by updates, such as notifying maintainers of broken reverse dependencies. In cases where timely fixes are not available, the section advises marking broken packages as `meta.broken = true` to exclude them from build tests until they are fixed.