2021-01-01 17:45:43 +00:00
# Idris {#idris}
2018-03-24 14:47:41 +00:00
2021-06-05 19:22:45 +00:00
## Installing Idris {#installing-idris}
2018-03-24 14:47:41 +00:00
2018-11-10 14:58:25 +00:00
The easiest way to get a working idris version is to install the `idris` attribute:
2018-03-24 14:47:41 +00:00
2021-06-05 19:22:45 +00:00
```ShellSession
2021-11-08 12:00:00 +00:00
$ nix-env -f "< nixpkgs > " -iA idris
2018-11-10 14:58:25 +00:00
```
2018-03-24 14:47:41 +00:00
2019-06-15 15:11:24 +00:00
This however only provides the `prelude` and `base` libraries. To install idris with additional libraries, you can use the `idrisPackages.with-packages` function, e.g. in an overlay in `~/.config/nixpkgs/overlays/my-idris.nix` :
2018-03-24 14:47:41 +00:00
2019-06-15 15:11:24 +00:00
```nix
self: super: {
myIdris = with self.idrisPackages; with-packages [ contrib pruviloj ];
}
2018-11-10 14:58:25 +00:00
```
2019-06-15 15:11:24 +00:00
And then:
2021-06-05 19:22:45 +00:00
```ShellSession
2019-06-15 15:11:24 +00:00
$ # On NixOS
$ nix-env -iA nixos.myIdris
$ # On non-NixOS
$ nix-env -iA nixpkgs.myIdris
2018-11-10 14:58:25 +00:00
```
2018-03-24 14:47:41 +00:00
2018-11-10 14:58:25 +00:00
To see all available Idris packages:
2021-06-05 19:22:45 +00:00
```ShellSession
2018-11-10 14:58:25 +00:00
$ # On NixOS
$ nix-env -qaPA nixos.idrisPackages
$ # On non-NixOS
$ nix-env -qaPA nixpkgs.idrisPackages
```
2018-03-24 14:47:41 +00:00
2018-11-10 14:58:25 +00:00
Similarly, entering a `nix-shell` :
2021-06-05 19:22:45 +00:00
```ShellSession
2018-11-10 14:58:25 +00:00
$ nix-shell -p 'idrisPackages.with-packages (with idrisPackages; [ contrib pruviloj ])'
```
2018-03-24 14:47:41 +00:00
2021-06-05 19:22:45 +00:00
## Starting Idris with library support {#starting-idris-with-library-support}
2018-03-24 14:47:41 +00:00
2018-11-10 14:58:25 +00:00
To have access to these libraries in idris, call it with an argument `-p <library name>` for each library:
2018-03-24 14:47:41 +00:00
2021-06-05 19:22:45 +00:00
```ShellSession
2018-11-10 14:58:25 +00:00
$ nix-shell -p 'idrisPackages.with-packages (with idrisPackages; [ contrib pruviloj ])'
[nix-shell:~]$ idris -p contrib -p pruviloj
```
2018-03-24 14:47:41 +00:00
2018-11-10 14:58:25 +00:00
A listing of all available packages the Idris binary has access to is available via `--listlibs` :
2021-06-05 19:22:45 +00:00
```ShellSession
2018-11-10 14:58:25 +00:00
$ idris --listlibs
00prelude-idx.ibc
pruviloj
base
contrib
prelude
00pruviloj-idx.ibc
00base-idx.ibc
00contrib-idx.ibc
```
2021-06-05 19:22:45 +00:00
## Building an Idris project with Nix {#building-an-idris-project-with-nix}
2018-11-10 14:58:25 +00:00
As an example of how a Nix expression for an Idris package can be created, here is the one for `idrisPackages.yaml` :
```nix
2021-01-21 00:07:16 +00:00
{ lib
, build-idris-package
2018-11-10 14:58:25 +00:00
, fetchFromGitHub
, contrib
, lightyear
}:
build-idris-package {
name = "yaml";
version = "2018-01-25";
# This is the .ipkg file that should be built, defaults to the package name
# In this case it should build `Yaml.ipkg` instead of `yaml.ipkg`
# This is only necessary because the yaml packages ipkg file is
# different from its package name here.
ipkgName = "Yaml";
# Idris dependencies to provide for the build
idrisDeps = [ contrib lightyear ];
src = fetchFromGitHub {
owner = "Heather";
repo = "Idris.Yaml";
rev = "5afa51ffc839844862b8316faba3bafa15656db4";
doc: use sri hash syntax
The nixpkgs manual contains references to both sri hash and explicit
sha256 attributes. This is at best confusing to new users. Since the
final destination is exclusive use of sri hashes, see nixos/rfcs#131,
might as well push new users in that direction gently.
Notable exceptions to sri hash support are builtins.fetchTarball,
cataclysm-dda, coq, dockerTools.pullimage, elixir.override, and
fetchCrate. None, other than builtins.fetchTarball, are fundamentally
incompatible, but all currently accept explicit sha256 attributes as
input. Because adding backwards compatibility is out of scope for this
change, they have been left intact, but migration to sri format has been
made for any using old hash formats.
All hashes have been manually tested to be accurate, and updates were
only made for missing upstream artefacts or bugs.
2022-12-03 19:49:00 +00:00
hash = "sha256-h28F9EEPuvab6zrfeE+0k1XGQJGwINnsJEG8yjWIl7w=";
2018-11-10 14:58:25 +00:00
};
Nix docs: remove `with lib;` from example code
Following [Best Practices](https://nix.dev/guides/best-practices#with-scopes),
`with` is a problematic language construction and should be avoided.
Usually it is employed like a "factorization": `[ X.A X.B X.C X.D ]` is written
`with X; [ A B C D ]`.
However, as shown in the link above, the syntatical rules of `with` are not so
intuitive, and this "distributive rule" is very selective, in the sense that
`with X; [ A B C D ]` is not equivalent to `[ X.A X.B X.C X.D ]`.
However, this factorization is still useful to "squeeze" some code, especially
in lists like `meta.maintainers`.
On the other hand, it becomes less justifiable in bigger scopes. This is
especially true in cases like `with lib;` in the top of expression and in sets
like `meta = with lib; { . . . }`.
That being said, this patch removes most of example code in the current
documentation.
The exceptions are, for now
- doc/functions/generators.section.md
- doc/languages-frameworks/coq.section.md
because, well, they are way more complicated, and I couldn't parse them
mentally - yet another reason why `with` should be avoided!
2024-03-06 11:51:54 +00:00
meta = {
2018-11-10 14:58:25 +00:00
description = "Idris YAML lib";
2020-02-16 16:31:03 +00:00
homepage = "https://github.com/Heather/Idris.Yaml";
Nix docs: remove `with lib;` from example code
Following [Best Practices](https://nix.dev/guides/best-practices#with-scopes),
`with` is a problematic language construction and should be avoided.
Usually it is employed like a "factorization": `[ X.A X.B X.C X.D ]` is written
`with X; [ A B C D ]`.
However, as shown in the link above, the syntatical rules of `with` are not so
intuitive, and this "distributive rule" is very selective, in the sense that
`with X; [ A B C D ]` is not equivalent to `[ X.A X.B X.C X.D ]`.
However, this factorization is still useful to "squeeze" some code, especially
in lists like `meta.maintainers`.
On the other hand, it becomes less justifiable in bigger scopes. This is
especially true in cases like `with lib;` in the top of expression and in sets
like `meta = with lib; { . . . }`.
That being said, this patch removes most of example code in the current
documentation.
The exceptions are, for now
- doc/functions/generators.section.md
- doc/languages-frameworks/coq.section.md
because, well, they are way more complicated, and I couldn't parse them
mentally - yet another reason why `with` should be avoided!
2024-03-06 11:51:54 +00:00
license = lib.licenses.mit;
maintainers = [ lib.maintainers.brainrape ];
2018-11-10 14:58:25 +00:00
};
}
```
Assuming this file is saved as `yaml.nix` , it's buildable using
2021-06-05 19:22:45 +00:00
```ShellSession
2018-11-10 14:58:25 +00:00
$ nix-build -E '(import < nixpkgs > {}).idrisPackages.callPackage ./yaml.nix {}'
```
Or it's possible to use
```nix
with import < nixpkgs > {};
{
yaml = idrisPackages.callPackage ./yaml.nix {};
}
```
in another file (say `default.nix` ) to be able to build it with
2021-06-05 19:22:45 +00:00
```ShellSession
2018-11-10 14:58:25 +00:00
$ nix-build -A yaml
```
2019-07-31 15:15:06 +00:00
2021-06-05 19:22:45 +00:00
## Passing options to `idris` commands {#passing-options-to-idris-commands}
2019-07-31 15:15:06 +00:00
The `build-idris-package` function provides also optional input values to set additional options for the used `idris` commands.
Specifically, you can set `idrisBuildOptions` , `idrisTestOptions` , `idrisInstallOptions` and `idrisDocOptions` to provide additional options to the `idris` command respectively when building, testing, installing and generating docs for your package.
For example you could set
2021-03-13 23:30:36 +00:00
```nix
2019-07-31 15:15:06 +00:00
build-idris-package {
2024-03-27 18:10:27 +00:00
idrisBuildOptions = [ "--log" "1" "--verbose" ];
2019-07-31 15:15:06 +00:00
2024-03-27 18:10:27 +00:00
# ...
2019-07-31 15:15:06 +00:00
}
```
to require verbose output during `idris` build phase.