tjh.dev
1# Idris2 {#sec-idris2}
2
3In addition to exposing the Idris2 compiler itself, Nixpkgs exposes an `idris2Packages.buildIdris` helper to make it a bit more ergonomic to build Idris2 executables or libraries.
4
5The `buildIdris` function takes an attribute set that defines at a minimum the `src` and `ipkgName` of the package to be built and any `idrisLibraries` required to build it. The `src` is the same source you're familiar with and the `ipkgName` must be the name of the `ipkg` file for the project (omitting the `.ipkg` extension). The `idrisLibraries` is a list of other library derivations created with `buildIdris`. You can optionally specify other derivation properties as needed but sensible defaults for `configurePhase`, `buildPhase`, and `installPhase` are provided.
6
7Importantly, `buildIdris` does not create a single derivation but rather an attribute set with two properties: `executable` and `library`. The `executable` property is a derivation and the `library` property is a function that will return a derivation for the library with or without source code included. Source code need not be included unless you are aiming to use IDE or LSP features that are able to jump to definitions within an editor.
8
9A simple example of a fully packaged library would be the [`LSP-lib`](https://github.com/idris-community/LSP-lib) found in the `idris-community` GitHub organization.
10```nix
11{ fetchFromGitHub, idris2Packages }:
12let
13 lspLibPkg = idris2Packages.buildIdris {
14 ipkgName = "lsp-lib";
15 src = fetchFromGitHub {
16 owner = "idris-community";
17 repo = "LSP-lib";
18 rev = "main";
19 hash = "sha256-EvSyMCVyiy9jDZMkXQmtwwMoLaem1GsKVFqSGNNHHmY=";
20 };
21 idrisLibraries = [ ];
22 };
23in
24lspLibPkg.library { withSource = true; }
25```
26
27The above results in a derivation with the installed library results (with sourcecode).
28
29A slightly more involved example of a fully packaged executable would be the [`idris2-lsp`](https://github.com/idris-community/idris2-lsp) which is an Idris2 language server that uses the `LSP-lib` found above.
30```nix
31{
32 callPackage,
33 fetchFromGitHub,
34 idris2Packages,
35}:
36
37# Assuming the previous example lives in `lsp-lib.nix`:
38let
39 lspLib = callPackage ./lsp-lib.nix { };
40 inherit (idris2Packages) idris2Api;
41 lspPkg = idris2Packages.buildIdris {
42 ipkgName = "idris2-lsp";
43 src = fetchFromGitHub {
44 owner = "idris-community";
45 repo = "idris2-lsp";
46 rev = "main";
47 hash = "sha256-vQTzEltkx7uelDtXOHc6QRWZ4cSlhhm5ziOqWA+aujk=";
48 };
49 idrisLibraries = [
50 idris2Api
51 lspLib
52 ];
53 };
54in
55lspPkg.executable
56```
57
58The above uses the default value of `withSource = false` for the `idris2Api` but could be modified to include that library's source by passing `(idris2Api { withSource = true; })` to `idrisLibraries` instead. `idris2Api` in the above derivation comes built in with `idris2Packages`. This library exposes many of the otherwise internal APIs of the Idris2 compiler.