Unverified Commit 0a965144 authored by Mathew Polzin's avatar Mathew Polzin Committed by GitHub
Browse files

idris2: Move to by-name, clean-up, add `withPackages` helper, make unwrapped compiler (#445120)

parents 5c29bfa0 159c2cb8
Loading
Loading
Loading
Loading
+69 −0
Original line number Diff line number Diff line
# Idris2 {#sec-idris2}

When developing using Idris2, by default the Idris compiler only has the minimal support libraries in its environment. This means that it will not attempt to read any libraries installed
globally, for example in the `$HOME` directory. The recommended way to use Idris2 is to wrap the compiler in an environment that provides these packages per-project, for example in a
devShell.

```nix
{
  pkgs ? import <nixpkgs> { },
}:
pkgs.mkShell {
  packages = [ (idris2.withPackages (p: [ p.idris2Api ])) ];
}
```
or, alternatively if Nix is used to build the Idris2 project:

```nix
{
  pkgs ? import <nixpkgs> { },
}:
pkgs.mkShell {
  inputsFrom = [ (pkgs.callPackage ./package.nix { }) ];
}
```

By default, the Idris2 compiler provided by Nixpkgs does not read globally installed packages, nor can install them. Running `idris2 --install` will fail because the Nix store is
a read-only file-system. If globally-installed packages are desired rather than the above strategy, one can set `IDRIS2_PREFIX`, or additional `IDRIS2_PACKAGE_PATH` entries
for the compiler to read from. The following snippet will append `$HOME/.idris2` to `$IDRIS2_PACKAGE_PATH`, and if such a variable does not exist, create it. The Nixpkg's Idris2
compiler append a few required libraries to this path variable, but any paths in the user's environment will be prefixed to those libraries.

```nix
{
  pkgs ? import <nixpkgs> { },
}:
pkgs.mkShell {
  packages = [ (idris2.withPackages (p: [ p.idris2Api ])) ];
  shellHook = ''
    IDRIS2_PACKAGE_PATH="''${IDRIS2_PACKAGE_PATH:+$IDRIS2_PACKAGE_PATH}$HOME/.idris2"
  '';
}
```
The following snippet will allow the Idris2 to run `idris2 --install` successfully:
```nix
{
  pkgs ? import <nixpkgs> { },
}:
pkgs.mkShell {
  packages = [ (idris2.withPackages (p: [ p.idris2Api ])) ];
  shellHook = ''
    IDRIS2_PREFIX="$HOME/.idris2"
  '';
}
```

In 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.

The `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.
@@ -56,3 +108,20 @@ lspPkg.executable
```

The 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.

The compiler package can be instantiated with packages on its `IDRIS2_PACKAGES` path from the `idris2Packages` set.

```nix
{
  idris2,
  devShell,
}:
let
  myIdris = idris2.withPackages (p: [ p.idris2Api ]);
in
devShell {
  packages = [ myIdris ];
}
```

This search path is extended from the path already in the user's environment.
+2 −0
Original line number Diff line number Diff line
@@ -269,6 +269,8 @@

- `installShellCompletion`: now supports Nushell completion files

- `idris2` supports being instantiated with a package environment with `idris.withPackages (p: [ ])`

- New hardening flags, `strictflexarrays1` and `strictflexarrays3` were made available, corresponding to the gcc/clang options `-fstrict-flex-arrays=1` and `-fstrict-flex-arrays=3` respectively.

- `gramps` has been updated to 6.0.0
+5 −0
Original line number Diff line number Diff line
{ mkPrelude, prelude }:
mkPrelude {
  name = "base";
  dependencies = [ prelude ];
}
+12 −0
Original line number Diff line number Diff line
{
  mkPrelude,
  prelude,
  base,
}:
mkPrelude {
  name = "contrib";
  dependencies = [
    prelude
    base
  ];
}
+33 −0
Original line number Diff line number Diff line
{
  stdenv,
  lib,
  gmp,
  idris2-src,
  idris2-version,
}:
stdenv.mkDerivation (finalAttrs: {
  pname = "libidris2_support";
  version = idris2-version;
  src = idris2-src;

  strictDeps = true;
  buildInputs = [ gmp ];

  enableParallelBuilding = true;
  makeFlags = [
    "PREFIX=${placeholder "out"}"
  ]
  ++ lib.optional stdenv.isDarwin "OS=";

  buildFlags = [ "support" ];

  installTargets = "install-support";

  postInstall = ''
    mv "$out/idris2-${finalAttrs.version}/lib" "$out/lib"
    mv "$out/idris2-${finalAttrs.version}/support" "$out/share"
    rm -rf $out/idris2-${finalAttrs.version}
  '';

  meta.description = "Runtime library for Idris2";
})
Loading