pyrox.dev
1# Agda {#agda}
2
3## How to use Agda {#how-to-use-agda}
4
5Agda is available as the [agda](https://search.nixos.org/packages?channel=unstable&show=agda&from=0&size=30&sort=relevance&query=agda)
6package.
7
8The `agda` package installs an Agda-wrapper, which calls `agda` with `--library-file`
9set to a generated library-file within the nix store, this means your library-file in
10`$HOME/.agda/libraries` will be ignored. By default the agda package installs Agda
11with no libraries, i.e. the generated library-file is empty. To use Agda with libraries,
12the `agda.withPackages` function can be used. This function either takes:
13
14* A list of packages,
15* or a function which returns a list of packages when given the `agdaPackages` attribute set,
16* or an attribute set containing a list of packages and a GHC derivation for compilation (see below).
17* 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).
18
19For example, suppose we wanted a version of Agda which has access to the standard library. This can be obtained with the expressions:
20
21```nix
22agda.withPackages [ agdaPackages.standard-library ]
23```
24
25or
26
27```nix
28agda.withPackages (p: [ p.standard-library ])
29```
30
31or can be called as in the [Compiling Agda](#compiling-agda) section.
32
33If you want to use a different version of a library (for instance a development version)
34override the `src` attribute of the package to point to your local repository
35
36```nix
37agda.withPackages (p: [
38 (p.standard-library.overrideAttrs (oldAttrs: {
39 version = "local version";
40 src = /path/to/local/repo/agda-stdlib;
41 }))
42])
43```
44
45You can also reference a GitHub repository
46
47```nix
48agda.withPackages (p: [
49 (p.standard-library.overrideAttrs (oldAttrs: {
50 version = "1.5";
51 src = fetchFromGitHub {
52 repo = "agda-stdlib";
53 owner = "agda";
54 rev = "v1.5";
55 hash = "sha256-nEyxYGSWIDNJqBfGpRDLiOAnlHJKEKAOMnIaqfVZzJk=";
56 };
57 }))
58])
59```
60
61If you want to use a library not added to Nixpkgs, you can add a
62dependency to a local library by calling `agdaPackages.mkDerivation`.
63
64```nix
65agda.withPackages (p: [
66 (p.mkDerivation {
67 pname = "your-agda-lib";
68 version = "1.0.0";
69 src = /path/to/your-agda-lib;
70 })
71])
72```
73
74Again you can reference GitHub
75
76```nix
77agda.withPackages (p: [
78 (p.mkDerivation {
79 pname = "your-agda-lib";
80 version = "1.0.0";
81 src = fetchFromGitHub {
82 repo = "repo";
83 owner = "owner";
84 version = "...";
85 rev = "...";
86 hash = "...";
87 };
88 })
89])
90```
91
92See [Building Agda Packages](#building-agda-packages) for more information on `mkDerivation`.
93
94Agda will not by default use these libraries. To tell Agda to use a library we have some options:
95
96* Call `agda` with the library flag:
97 ```ShellSession
98 $ agda -l standard-library -i . MyFile.agda
99 ```
100* Write a `my-library.agda-lib` file for the project you are working on which may look like:
101 ```
102 name: my-library
103 include: .
104 depend: standard-library
105 ```
106* Create the file `~/.agda/defaults` and add any libraries you want to use by default.
107
108More information can be found in the [official Agda documentation on library management](https://agda.readthedocs.io/en/v2.6.1/tools/package-system.html).
109
110## Compiling Agda {#compiling-agda}
111
112Agda 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.
113This can be overridden by a different version of `ghc` as follows:
114
115```nix
116agda.withPackages {
117 pkgs = [
118 # ...
119 ];
120 ghc = haskell.compiler.ghcHEAD;
121}
122```
123
124To install Agda without GHC, use `ghc = null;`.
125
126## Writing Agda packages {#writing-agda-packages}
127
128To write a nix derivation for an Agda library, first check that the library has a (single) `*.agda-lib` file.
129
130A derivation can then be written using `agdaPackages.mkDerivation`. This has similar arguments to `stdenv.mkDerivation` with the following additions:
131
132* `libraryName` should be the name that appears in the `*.agda-lib` file, defaulting to `pname`.
133* `libraryFile` should be the file name of the `*.agda-lib` file, defaulting to `${libraryName}.agda-lib`.
134
135Here is an example `default.nix`
136
137```nix
138{
139 nixpkgs ? <nixpkgs>,
140}:
141with (import nixpkgs { });
142agdaPackages.mkDerivation {
143 version = "1.0";
144 pname = "my-agda-lib";
145 src = ./.;
146 buildInputs = [ agdaPackages.standard-library ];
147}
148```
149
150### Building Agda packages {#building-agda-packages}
151
152The default build phase for `agdaPackages.mkDerivation` runs `agda --build-library`.
153If something else is needed to build the package (e.g. `make`) then the `buildPhase` should be overridden.
154Additionally, a `preBuild` or `configurePhase` can be used if there are steps that need to be done prior to checking the library.
155`agda` and the Agda libraries contained in `buildInputs` are made available during the build phase.
156
157### Installing Agda packages {#installing-agda-packages}
158
159The default install phase copies Agda source files, Agda interface files (`*.agdai`) and `*.agda-lib` files to the output directory.
160This can be overridden.
161
162By 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.
163
164## Maintaining the Agda package set on Nixpkgs {#maintaining-the-agda-package-set-on-nixpkgs}
165
166We are aiming at providing all common Agda libraries as packages on `nixpkgs`,
167and keeping them up to date.
168Contributions and maintenance help is always appreciated,
169but the maintenance effort is typically low since the Agda ecosystem is quite small.
170
171The `nixpkgs` Agda package set tries to take up a role similar to that of [Stackage](https://www.stackage.org/) in the Haskell world.
172It is a curated set of libraries that:
173
1741. Always work together.
1752. Are as up-to-date as possible.
176
177While the Haskell ecosystem is huge, and Stackage is highly automated,
178the Agda package set is small and can (still) be maintained by hand.
179
180### Adding Agda packages to Nixpkgs {#adding-agda-packages-to-nixpkgs}
181
182To 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:
183
184```nix
185{
186 mkDerivation,
187 standard-library,
188 fetchFromGitHub,
189}:
190
191mkDerivation {
192 pname = "my-library";
193 version = "1.0";
194 src = <...>;
195 buildInputs = [ standard-library ];
196 meta = <...>;
197}
198```
199
200You can look at other files under `pkgs/development/libraries/agda/` for more inspiration.
201
202Note that the derivation function is called with `mkDerivation` set to `agdaPackages.mkDerivation`, therefore you
203could use a similar set as in your `default.nix` from [Writing Agda Packages](#writing-agda-packages) with
204`agdaPackages.mkDerivation` replaced with `mkDerivation`.
205
206Here is an example skeleton derivation for iowa-stdlib:
207
208```nix
209mkDerivation {
210 version = "1.5.0";
211 pname = "iowa-stdlib";
212
213 src = <...>;
214
215 libraryFile = "";
216 libraryName = "IAL-1.3";
217
218 buildPhase = ''
219 runHook preBuild
220
221 patchShebangs find-deps.sh
222 make
223
224 runHook postBuild
225 '';
226}
227```
228
229This 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`.
230
231When 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://githcub.com/agda/agda/issues/4613).
232
233In the pull request adding this library,
234you can test whether it builds correctly by writing in a comment:
235
236```
237@ofborg build agdaPackages.my-library
238```
239
240### Maintaining Agda packages {#agda-maintaining-packages}
241
242As mentioned before, the aim is to have a compatible, and up-to-date package set.
243These two conditions sometimes exclude each other:
244For example, if we update `agdaPackages.standard-library` because there was an upstream release,
245this will typically break many reverse dependencies,
246i.e. downstream Agda libraries that depend on the standard library.
247In `nixpkgs` we are typically among the first to notice this,
248since we have build tests in place to check this.
249
250In a pull request updating e.g. the standard library, you should write the following comment:
251
252```
253@ofborg build agdaPackages.standard-library.passthru.tests
254```
255
256This will build all reverse dependencies of the standard library,
257for example `agdaPackages.agda-categories`, or `agdaPackages.generic`.
258
259In some cases it is useful to build _all_ Agda packages.
260This can be done with the following Github comment:
261
262```
263@ofborg build agda.passthru.tests.allPackages
264```
265
266Sometimes, the builds of the reverse dependencies fail because they have not yet been updated and released.
267You should drop the maintainers a quick issue notifying them of the breakage,
268citing the build error (which you can get from the ofborg logs).
269If you are motivated, you might even send a pull request that fixes it.
270Usually, the maintainers will answer within a week or two with a new release.
271Bumping the version of that reverse dependency should be a further commit on your PR.
272
273In the rare case that a new release is not to be expected within an acceptable time,
274mark the broken package as broken by setting `meta.broken = true;`.
275This will exclude it from the build test.
276It can be added later when it is fixed,
277and does not hinder the advancement of the whole package set in the meantime.