diff --git a/doc/languages-frameworks/idris2.section.md b/doc/languages-frameworks/idris2.section.md index 953222b9b315..a9b524250a37 100644 --- a/doc/languages-frameworks/idris2.section.md +++ b/doc/languages-frameworks/idris2.section.md @@ -1,5 +1,57 @@ # 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 { }, +}: +pkgs.mkShell { + packages = [ (idris2.withPackages (p: [ p.idris2Api ])) ]; +} +``` +or, alternatively if Nix is used to build the Idris2 project: + +```nix +{ + pkgs ? import { }, +}: +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 { }, +}: +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 { }, +}: +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. diff --git a/doc/release-notes/rl-2511.section.md b/doc/release-notes/rl-2511.section.md index 81389bf97a8b..4e42fcca7ec7 100644 --- a/doc/release-notes/rl-2511.section.md +++ b/doc/release-notes/rl-2511.section.md @@ -267,6 +267,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