pyrox.dev
Merge pull request #110491 from neosimsim/agda-doc-fix-install-command
agda: fix code snippet for installing Agda
authored by
Domen Kožar
and committed by
GitHub
ba6f0e8f
c75166fb
+90
-9
doc/languages-frameworks/agda.section.md
+90
-9
doc/languages-frameworks/agda.section.md
···
2
2
3
3
## How to use Agda
4
4
5
-
Agda can be installed from `agda`:
6
-
```ShellSession
7
-
$ nix-env -iA agda
8
-
```
5
+
Agda is available as the [agda](https://search.nixos.org/packages?channel=unstable&show=agda&from=0&size=30&sort=relevance&query=agda)
6
+
package.
9
7
10
-
To use Agda with libraries, the `agda.withPackages` function can be used. This function either takes:
8
+
The `agda` package installs an Agda-wrapper, which calls `agda` with `--library-file`
9
+
set 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
11
+
with no libraries, i.e. the generated library-file is empty. To use Agda with libraries,
12
+
the `agda.withPackages` function can be used. This function either takes:
11
13
12
14
* A list of packages,
13
15
* or a function which returns a list of packages when given the `agdaPackages` attribute set,
14
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).
15
18
16
19
For example, suppose we wanted a version of Agda which has access to the standard library. This can be obtained with the expressions:
17
20
···
27
30
28
31
or can be called as in the [Compiling Agda](#compiling-agda) section.
29
32
30
-
If you want to use a library in your home directory (for instance if it is a development version) then typecheck it manually (using `agda.withPackages` if necessary) and then override the `src` attribute of the package to point to your local repository.
33
+
If you want to use a different version of a library (for instance a development version)
34
+
override the `src` attribute of the package to point to your local repository
35
+
36
+
```nix
37
+
agda.withPackages (p: [
38
+
(p.standard-library.overrideAttrs (oldAttrs: {
39
+
version = "local version";
40
+
src = /path/to/local/repo/agda-stdlib;
41
+
}))
42
+
])
43
+
```
44
+
45
+
You can also reference a GitHub repository
46
+
```nix
47
+
agda.withPackages (p: [
48
+
(p.standard-library.overrideAttrs (oldAttrs: {
49
+
version = "1.5";
50
+
src = fetchFromGitHub {
51
+
repo = "agda-stdlib";
52
+
owner = "agda";
53
+
rev = "v1.5";
54
+
sha256 = "16fcb7ssj6kj687a042afaa2gq48rc8abihpm14k684ncihb2k4w";
55
+
};
56
+
}))
57
+
])
58
+
```
59
+
60
+
If you want to use a library not added to Nixpkgs, you can add a
61
+
dependency to a local library by calling `agdaPackages.mkDerivation`.
62
+
```nix
63
+
agda.withPackages (p: [
64
+
(p.mkDerivation {
65
+
pname = "your-agda-lib";
66
+
version = "1.0.0";
67
+
src = /path/to/your-agda-lib;
68
+
})
69
+
])
70
+
```
71
+
72
+
Again you can reference GitHub
73
+
74
+
```nix
75
+
agda.withPackages (p: [
76
+
(p.mkDerivation {
77
+
pname = "your-agda-lib";
78
+
version = "1.0.0";
79
+
src = fetchFromGitHub {
80
+
repo = "repo";
81
+
owner = "owner";
82
+
version = "...";
83
+
rev = "...";
84
+
sha256 = "...";
85
+
};
86
+
})
87
+
])
88
+
```
89
+
90
+
See [Building Agda Packages](#building-agda-packages) for more information on `mkDerivation`.
31
91
32
-
Agda will not by default use these libraries. To tell Agda to use the library we have some options:
92
+
Agda will not by default use these libraries. To tell Agda to use a library we have some options:
33
93
34
94
* Call `agda` with the library flag:
35
95
```ShellSession
···
46
106
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).
47
107
48
108
## Compiling Agda
49
-
Agda modules can be compiled with the `--compile` flag. A version of `ghc` with `ieee754` is made available to the Agda program via the `--with-compiler` flag.
109
+
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.
50
110
This can be overridden by a different version of `ghc` as follows:
51
111
52
112
```nix
···
65
125
* `libraryName` should be the name that appears in the `*.agda-lib` file, defaulting to `pname`.
66
126
* `libraryFile` should be the file name of the `*.agda-lib` file, defaulting to `${libraryName}.agda-lib`.
67
127
128
+
Here is an example `default.nix`
129
+
130
+
```nix
131
+
{ nixpkgs ? <nixpkgs> }:
132
+
with (import nixpkgs {});
133
+
agdaPackages.mkDerivation {
134
+
version = "1.0";
135
+
pname = "my-agda-lib";
136
+
src = ./.;
137
+
buildInputs = [
138
+
agdaPackages.standard-library
139
+
];
140
+
}
141
+
```
142
+
68
143
### Building Agda packages
69
144
The default build phase for `agdaPackages.mkDerivation` simply runs `agda` on the `Everything.agda` file.
70
145
If something else is needed to build the package (e.g. `make`) then the `buildPhase` should be overridden.
···
80
155
## Adding Agda packages to Nixpkgs
81
156
82
157
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:
158
+
83
159
```nix
84
160
{ mkDerivation, standard-library, fetchFromGitHub }:
85
161
```
86
-
and `mkDerivation` should be called instead of `agdaPackages.mkDerivation`. Here is an example skeleton derivation for iowa-stdlib:
162
+
163
+
Note that the derivation function is called with `mkDerivation` set to `agdaPackages.mkDerivation`, therefore you
164
+
could use a similar set as in your `default.nix` from [Writing Agda Packages](#writing-agda-packages) with
165
+
`agdaPackages.mkDerivation` replaced with `mkDerivation`.
166
+
167
+
Here is an example skeleton derivation for iowa-stdlib:
87
168
88
169
```nix
89
170
mkDerivation {