dhall: Document language support in the Nixpkgs manual (#123051)
This commit is contained in:
parent
b065b36e86
commit
b23797e2c5
432
doc/languages-frameworks/dhall.section.md
Normal file
432
doc/languages-frameworks/dhall.section.md
Normal file
@ -0,0 +1,432 @@
|
||||
# Dhall {#sec-language-dhall}
|
||||
|
||||
The Nixpkgs support for Dhall assumes some familiarity with Dhall's language
|
||||
support for importing Dhall expressions, which is documented here:
|
||||
|
||||
* [`dhall-lang.org` - Installing packages](https://docs.dhall-lang.org/tutorials/Language-Tour.html#installing-packages)
|
||||
|
||||
## Remote imports
|
||||
|
||||
Nixpkgs bypasses Dhall's support for remote imports using Dhall's
|
||||
semantic integrity checks. Specifically, any Dhall import can be protected by
|
||||
an integrity check like:
|
||||
|
||||
```dhall
|
||||
https://prelude.dhall-lang.org/v20.1.0/package.dhall
|
||||
sha256:26b0ef498663d269e4dc6a82b0ee289ec565d683ef4c00d0ebdd25333a5a3c98
|
||||
```
|
||||
|
||||
… and if the import is cached then the interpreter will load the import from
|
||||
cache instead of fetching the URL.
|
||||
|
||||
Nixpkgs uses this trick to add all of a Dhall expression's dependencies into the
|
||||
cache so that the Dhall interpreter never needs to resolve any remote URLs. In
|
||||
fact, Nixpkgs uses a Dhall interpreter with remote imports disabled when
|
||||
packaging Dhall expressions to enforce that the interpreter never resolves a
|
||||
remote import. This means that Nixpkgs only supports building Dhall expressions
|
||||
if all of their remote imports are protected by semantic integrity checks.
|
||||
|
||||
Instead of remote imports, Nixpkgs uses Nix to fetch remote Dhall code. For
|
||||
example, the Prelude Dhall package uses `pkgs.fetchFromGitHub` to fetch the
|
||||
`dhall-lang` repository containing the Prelude. Relying exclusively on Nix
|
||||
to fetch Dhall code ensures that Dhall packages built using Nix remain pure and
|
||||
also behave well when built within a sandbox.
|
||||
|
||||
## Packaging a Dhall expression from scratch
|
||||
|
||||
We can illustrate how Nixpkgs integrates Dhall by beginning from the following
|
||||
trivial Dhall expression with one dependency (the Prelude):
|
||||
|
||||
```dhall
|
||||
-- ./true.dhall
|
||||
|
||||
let Prelude = https://prelude.dhall-lang.org/v20.1.0/package.dhall
|
||||
|
||||
in Prelude.Bool.not False
|
||||
```
|
||||
|
||||
As written, this expression cannot be built using Nixpkgs because the
|
||||
expression does not protect the Prelude import with a semantic integrity
|
||||
check, so the first step is to freeze the expression using `dhall freeze`,
|
||||
like this:
|
||||
|
||||
```bash
|
||||
$ dhall freeze --inplace ./true.dhall
|
||||
```
|
||||
|
||||
… which gives us:
|
||||
|
||||
```dhall
|
||||
-- ./true.dhall
|
||||
|
||||
let Prelude =
|
||||
https://prelude.dhall-lang.org/v20.1.0/package.dhall
|
||||
sha256:26b0ef498663d269e4dc6a82b0ee289ec565d683ef4c00d0ebdd25333a5a3c98
|
||||
|
||||
in Prelude.Bool.not False
|
||||
```
|
||||
|
||||
To package that expression, we create a `./true.nix` file containing the
|
||||
following specification for the Dhall package:
|
||||
|
||||
```nix
|
||||
# ./true.nix
|
||||
|
||||
{ buildDhallPackage, Prelude }:
|
||||
|
||||
buildDhallPackage {
|
||||
name = "true";
|
||||
code = ./true.dhall;
|
||||
dependencies = [ Prelude ];
|
||||
source = true;
|
||||
}
|
||||
```
|
||||
|
||||
… and we complete the build by incorporating that Dhall package into the
|
||||
`pkgs.dhallPackages` hierarchy using an overlay, like this:
|
||||
|
||||
```nix
|
||||
# ./example.nix
|
||||
|
||||
let
|
||||
nixpkgs = builtins.fetchTarball {
|
||||
url = "https://github.com/NixOS/nixpkgs/archive/94b2848559b12a8ed1fe433084686b2a81123c99.tar.gz";
|
||||
sha256 = "1pbl4c2dsaz2lximgd31m96jwbps6apn3anx8cvvhk1gl9rkg107";
|
||||
};
|
||||
|
||||
dhallOverlay = self: super: {
|
||||
true = self.callPackage ./true.nix { };
|
||||
};
|
||||
|
||||
overlay = self: super: {
|
||||
dhallPackages = super.dhallPackages.override (old: {
|
||||
overrides =
|
||||
self.lib.composeExtensions (old.overrides or (_: _: {})) dhallOverlay;
|
||||
});
|
||||
};
|
||||
|
||||
pkgs = import nixpkgs { config = {}; overlays = [ overlay ]; };
|
||||
|
||||
in
|
||||
pkgs
|
||||
```
|
||||
|
||||
… which we can then build using this command:
|
||||
|
||||
```bash
|
||||
$ nix build --file ./example.nix dhallPackages.true
|
||||
```
|
||||
|
||||
## Contents of a Dhall package
|
||||
|
||||
The above package produces the following directory tree:
|
||||
|
||||
```bash
|
||||
$ tree -a ./result
|
||||
result
|
||||
├── .cache
|
||||
│ └── dhall
|
||||
│ └── 122027abdeddfe8503496adeb623466caa47da5f63abd2bc6fa19f6cfcb73ecfed70
|
||||
├── binary.dhall
|
||||
└── source.dhall
|
||||
```
|
||||
|
||||
… where:
|
||||
|
||||
* `source.dhall` contains the result of interpreting our Dhall package:
|
||||
|
||||
```bash
|
||||
$ cat ./result/source.dhall
|
||||
True
|
||||
```
|
||||
|
||||
* The `.cache` subdirectory contains one binary cache product encoding the
|
||||
same result as `source.dhall`:
|
||||
|
||||
```bash
|
||||
$ dhall decode < ./result/.cache/dhall/122027abdeddfe8503496adeb623466caa47da5f63abd2bc6fa19f6cfcb73ecfed70
|
||||
True
|
||||
```
|
||||
|
||||
* `binary.dhall` contains a Dhall expression which handles fetching and decoding
|
||||
the same cache product:
|
||||
|
||||
```bash
|
||||
$ cat ./result/binary.dhall
|
||||
missing sha256:27abdeddfe8503496adeb623466caa47da5f63abd2bc6fa19f6cfcb73ecfed70
|
||||
$ cp -r ./result/.cache .cache
|
||||
|
||||
$ chmod -R u+w .cache
|
||||
|
||||
$ XDG_CACHE_HOME=.cache dhall --file ./result/binary.dhall
|
||||
True
|
||||
```
|
||||
|
||||
The `source.dhall` file is only present for packages that specify
|
||||
`source = true;`. By default, Dhall packages omit the `source.dhall` in order
|
||||
to conserve disk space when they are used exclusively as dependencies. For
|
||||
example, if we build the Prelude package it will only contain the binary
|
||||
encoding of the expression:
|
||||
|
||||
```bash
|
||||
$ nix build --file ./example.nix dhallPackages.Prelude
|
||||
|
||||
$ tree -a result
|
||||
result
|
||||
├── .cache
|
||||
│ └── dhall
|
||||
│ └── 122026b0ef498663d269e4dc6a82b0ee289ec565d683ef4c00d0ebdd25333a5a3c98
|
||||
└── binary.dhall
|
||||
|
||||
2 directories, 2 files
|
||||
```
|
||||
|
||||
Typically, you only specify `source = true;` for the top-level Dhall expression
|
||||
of interest (such as our example `true.nix` Dhall package). However, if you
|
||||
wish to specify `source = true` for all Dhall packages, then you can amend the
|
||||
Dhall overlay like this:
|
||||
|
||||
```nix
|
||||
dhallOverrides = self: super: {
|
||||
# Enable source for all Dhall packages
|
||||
buildDhallPackage =
|
||||
args: super.buildDhallPackage (args // { source = true; });
|
||||
|
||||
true = self.callPackage ./true.nix { };
|
||||
};
|
||||
```
|
||||
|
||||
… and now the Prelude will contain the fully decoded result of interpreting
|
||||
the Prelude:
|
||||
|
||||
```bash
|
||||
$ nix build --file ./example.nix dhallPackages.Prelude
|
||||
|
||||
$ tree -a result
|
||||
result
|
||||
├── .cache
|
||||
│ └── dhall
|
||||
│ └── 122026b0ef498663d269e4dc6a82b0ee289ec565d683ef4c00d0ebdd25333a5a3c98
|
||||
├── binary.dhall
|
||||
└── source.dhall
|
||||
|
||||
$ cat ./result/source.dhall
|
||||
{ Bool =
|
||||
{ and =
|
||||
\(_ : List Bool) ->
|
||||
List/fold Bool _ Bool (\(_ : Bool) -> \(_ : Bool) -> _@1 && _) True
|
||||
, build = \(_ : Type -> _ -> _@1 -> _@2) -> _ Bool True False
|
||||
, even =
|
||||
\(_ : List Bool) ->
|
||||
List/fold Bool _ Bool (\(_ : Bool) -> \(_ : Bool) -> _@1 == _) True
|
||||
, fold =
|
||||
\(_ : Bool) ->
|
||||
…
|
||||
```
|
||||
|
||||
## Packaging functions
|
||||
|
||||
We already saw an example of using `buildDhallPackage` to create a Dhall
|
||||
package from a single file, but most Dhall packages consist of more than one
|
||||
file and there are two derived utilities that you may find more useful when
|
||||
packaging multiple files:
|
||||
|
||||
* `buildDhallDirectoryPackage` - build a Dhall package from a local directory
|
||||
|
||||
* `buildDhallGitHubPackage` - build a Dhall package from a GitHub repository
|
||||
|
||||
The `buildDhallPackage` is the lowest-level function and accepts the following
|
||||
arguments:
|
||||
|
||||
* `name`: The name of the derivation
|
||||
|
||||
* `dependencies`: Dhall dependencies to build and cache ahead of time
|
||||
|
||||
* `code`: The top-level expression to build for this package
|
||||
|
||||
Note that the `code` field accepts an arbitrary Dhall expression. You're
|
||||
not limited to just a file.
|
||||
|
||||
* `source`: Set to `true` to include the decoded result as `source.dhall` in the
|
||||
build product, at the expense of requiring more disk space
|
||||
|
||||
* `documentationRoot`: Set to the root directory of the package if you want
|
||||
`dhall-docs` to generate documentation underneath the `docs` subdirectory of
|
||||
the build product
|
||||
|
||||
The `buildDhallDirectoryPackage` is a higher-level function implemented in terms
|
||||
of `buildDhallPackage` that accepts the following arguments:
|
||||
|
||||
* `name`: Same as `buildDhallPackage`
|
||||
|
||||
* `dependencies`: Same as `buildDhallPackage`
|
||||
|
||||
* `source`: Same as `buildDhallPackage`
|
||||
|
||||
* `src`: The directory containing Dhall code that you want to turn into a Dhall
|
||||
package
|
||||
|
||||
* `file`: The top-level file (`package.dhall` by default) that is the entrypoint
|
||||
to the rest of the package
|
||||
|
||||
* `document`: Set to `true` to generate documentation for the package
|
||||
|
||||
The `buildDhallGitHubPackage` is another higher-level function implemented in
|
||||
terms of `buildDhallPackage` that accepts the following arguments:
|
||||
|
||||
* `name`: Same as `buildDhallPackage`
|
||||
|
||||
* `dependencies`: Same as `buildDhallPackage`
|
||||
|
||||
* `source`: Same as `buildDhallPackage`
|
||||
|
||||
* `owner`: The owner of the repository
|
||||
|
||||
* `repo`: The repository name
|
||||
|
||||
* `rev`: The desired revision (or branch, or tag)
|
||||
|
||||
* `directory`: The subdirectory of the Git repository to package (if a
|
||||
directory other than the root of the repository)
|
||||
|
||||
* `file`: The top-level file (`${directory}/package.dhall` by default) that is
|
||||
the entrypoint to the rest of the package
|
||||
|
||||
* `document`: Set to `true` to generate documentation for the package
|
||||
|
||||
Additionally, `buildDhallGitHubPackage` accepts the same arguments as
|
||||
`fetchFromGitHub`, such as `sha256` or `fetchSubmodules`.
|
||||
|
||||
## `dhall-to-nixpkgs`
|
||||
|
||||
You can use the `dhall-to-nixpkgs` command-line utility to automate
|
||||
packaging Dhall code. For example:
|
||||
|
||||
```bash
|
||||
$ nix-env --install --attr haskellPackages.dhall-nixpkgs
|
||||
|
||||
$ nix-env --install --attr nix-prefetch-git # Used by dhall-to-nixpkgs
|
||||
|
||||
$ dhall-to-nixpkgs github https://github.com/Gabriel439/dhall-semver.git
|
||||
{ buildDhallGitHubPackage, Prelude }:
|
||||
buildDhallGitHubPackage {
|
||||
name = "dhall-semver";
|
||||
githubBase = "github.com";
|
||||
owner = "Gabriel439";
|
||||
repo = "dhall-semver";
|
||||
rev = "2d44ae605302ce5dc6c657a1216887fbb96392a4";
|
||||
fetchSubmodules = false;
|
||||
sha256 = "0y8shvp8srzbjjpmnsvz9c12ciihnx1szs0yzyi9ashmrjvd0jcz";
|
||||
directory = "";
|
||||
file = "package.dhall";
|
||||
source = false;
|
||||
document = false;
|
||||
dependencies = [ (Prelude.overridePackage { file = "package.dhall"; }) ];
|
||||
}
|
||||
```
|
||||
|
||||
The utility takes care of automatically detecting remote imports and converting
|
||||
them to package dependencies. You can also use the utility on local
|
||||
Dhall directories, too:
|
||||
|
||||
```bash
|
||||
$ dhall-to-nixpkgs directory ~/proj/dhall-semver
|
||||
{ buildDhallDirectoryPackage, Prelude }:
|
||||
buildDhallDirectoryPackage {
|
||||
name = "proj";
|
||||
src = /Users/gabriel/proj/dhall-semver;
|
||||
file = "package.dhall";
|
||||
source = false;
|
||||
document = false;
|
||||
dependencies = [ (Prelude.overridePackage { file = "package.dhall"; }) ];
|
||||
}
|
||||
```
|
||||
|
||||
## Overriding dependency versions
|
||||
|
||||
Suppose that we change our `true.dhall` example expression to depend on an older
|
||||
version of the Prelude (19.0.0):
|
||||
|
||||
```dhall
|
||||
-- ./true.dhall
|
||||
|
||||
let Prelude =
|
||||
https://prelude.dhall-lang.org/v19.0.0/package.dhall
|
||||
sha256:eb693342eb769f782174157eba9b5924cf8ac6793897fc36a31ccbd6f56dafe2
|
||||
|
||||
in Prelude.Bool.not False
|
||||
```
|
||||
|
||||
If we try to rebuild that expression the build will fail:
|
||||
|
||||
```
|
||||
$ nix build --file ./example.nix dhallPackages.true
|
||||
builder for '/nix/store/0f1hla7ff1wiaqyk1r2ky4wnhnw114fi-true.drv' failed with exit code 1; last 10 log lines:
|
||||
|
||||
Dhall was compiled without the 'with-http' flag.
|
||||
|
||||
The requested URL was: https://prelude.dhall-lang.org/v19.0.0/package.dhall
|
||||
|
||||
|
||||
4│ https://prelude.dhall-lang.org/v19.0.0/package.dhall
|
||||
5│ sha256:eb693342eb769f782174157eba9b5924cf8ac6793897fc36a31ccbd6f56dafe2
|
||||
|
||||
/nix/store/rsab4y99h14912h4zplqx2iizr5n4rc2-true.dhall:4:7
|
||||
[1 built (1 failed), 0.0 MiB DL]
|
||||
error: build of '/nix/store/0f1hla7ff1wiaqyk1r2ky4wnhnw114fi-true.drv' failed
|
||||
```
|
||||
|
||||
… because the default Prelude selected by Nixpkgs revision
|
||||
`94b2848559b12a8ed1fe433084686b2a81123c99is` is version 20.1.0, which doesn't
|
||||
have the same integrity check as version 19.0.0. This means that version
|
||||
19.0.0 is not cached and the interpreter is not allowed to fall back to
|
||||
importing the URL.
|
||||
|
||||
However, we can override the default Prelude version by using `dhall-to-nixpkgs`
|
||||
to create a Dhall package for our desired Prelude:
|
||||
|
||||
```bash
|
||||
$ dhall-to-nixpkgs github https://github.com/dhall-lang/dhall-lang.git \
|
||||
--name Prelude \
|
||||
--directory Prelude \
|
||||
--rev v19.0.0 \
|
||||
> Prelude.nix
|
||||
```
|
||||
|
||||
… and then referencing that package in our Dhall overlay, by either overriding
|
||||
the Prelude globally for all packages, like this:
|
||||
|
||||
```bash
|
||||
dhallOverrides = self: super: {
|
||||
true = self.callPackage ./true.nix { };
|
||||
|
||||
Prelude = self.callPackage ./Prelude.nix { };
|
||||
};
|
||||
```
|
||||
|
||||
… or selectively overriding the Prelude dependency for just the `true` package,
|
||||
like this:
|
||||
|
||||
```bash
|
||||
dhallOverrides = self: super: {
|
||||
true = self.callPackage ./true.nix {
|
||||
Prelude = self.callPackage ./Prelude.nix { };
|
||||
};
|
||||
};
|
||||
```
|
||||
|
||||
## Overrides
|
||||
|
||||
You can override any of the arguments to `buildDhallGitHubPackage` or
|
||||
`buildDhallDirectoryPackage` using the `overridePackage` attribute of a package.
|
||||
For example, suppose we wanted to selectively enable `source = true` just for the Prelude. We can do that like this:
|
||||
|
||||
```nix
|
||||
dhallOverrides = self: super: {
|
||||
Prelude = super.Prelude.overridePackage { source = true; };
|
||||
|
||||
…
|
||||
};
|
||||
```
|
||||
|
||||
[semantic-integrity-checks]: https://docs.dhall-lang.org/tutorials/Language-Tour.html#installing-packages
|
@ -11,6 +11,7 @@
|
||||
<xi:include href="bower.section.xml" />
|
||||
<xi:include href="coq.section.xml" />
|
||||
<xi:include href="crystal.section.xml" />
|
||||
<xi:include href="dhall.section.xml" />
|
||||
<xi:include href="emscripten.section.xml" />
|
||||
<xi:include href="gnome.section.xml" />
|
||||
<xi:include href="go.section.xml" />
|
||||
|
Loading…
Reference in New Issue
Block a user