Anderson Torres e671d3bbbd 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:40:09 -03:00

3.6 KiB

Raw Blame History

Idris

Installing Idris

The easiest way to get a working idris version is to install the idris attribute:

$ nix-env -f "<nixpkgs>" -iA idris

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:

self: super: {
  myIdris = with self.idrisPackages; with-packages [ contrib pruviloj ];
}

And then:

$ # On NixOS
$ nix-env -iA nixos.myIdris
$ # On non-NixOS
$ nix-env -iA nixpkgs.myIdris

To see all available Idris packages:

$ # On NixOS
$ nix-env -qaPA nixos.idrisPackages
$ # On non-NixOS
$ nix-env -qaPA nixpkgs.idrisPackages

Similarly, entering a nix-shell:

$ nix-shell -p 'idrisPackages.with-packages (with idrisPackages; [ contrib pruviloj ])'

Starting Idris with library support

To have access to these libraries in idris, call it with an argument -p <library name> for each library:

$ nix-shell -p 'idrisPackages.with-packages (with idrisPackages; [ contrib pruviloj ])'
[nix-shell:~]$ idris -p contrib -p pruviloj

A listing of all available packages the Idris binary has access to is available via --listlibs:

$ idris --listlibs
00prelude-idx.ibc
pruviloj
base
contrib
prelude
00pruviloj-idx.ibc
00base-idx.ibc
00contrib-idx.ibc

Building an Idris project with Nix

As an example of how a Nix expression for an Idris package can be created, here is the one for idrisPackages.yaml:

{ lib
, build-idris-package
, 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";
    hash = "sha256-h28F9EEPuvab6zrfeE+0k1XGQJGwINnsJEG8yjWIl7w=";
  };

  meta = {
    description = "Idris YAML lib";
    homepage = "https://github.com/Heather/Idris.Yaml";
    license = lib.licenses.mit;
    maintainers = [ lib.maintainers.brainrape ];
  };
}

Assuming this file is saved as yaml.nix, it's buildable using

$ nix-build -E '(import <nixpkgs> {}).idrisPackages.callPackage ./yaml.nix {}'

Or it's possible to use

with import <nixpkgs> {};

{
  yaml = idrisPackages.callPackage ./yaml.nix {};
}

in another file (say default.nix) to be able to build it with

$ nix-build -A yaml

Passing options to `idris` commands

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

build-idris-package {
  idrisBuildOptions = [ "--log" "1" "--verbose" ]

  ...
}

to require verbose output during idris build phase.

3.6 KiB Raw Blame History