Offline use of Prelude


#1

The Dhall Prelude documentation recommends using the Prelude like this:

let Prelude = https://prelude.dhall-lang.org/package.dhall

This seems to always fetch the prelude from the network or at least require network access, because without it, evaluation fails with

Error: Remote host not found

This is unfortunate for many reasons, the most important is that it means that Dhall can’t be easily used in a build container without network access.

Given that the Prelude contains many essential functions, I assume it would make sense to ship it with the interpreter and recognize this well-known URL. Otherwise, everybody has to reinvent the wheel when including the Prelude.

Any opinions? Am I missing the obvious way how to use Dhall offline?


#2

I believe if you freeze the import (i.e. provide the hash), Dhall will pull from the cache. For example:

let Prelude =
      https://prelude.dhall-lang.org/package.dhall sha256:4aa8581954f7734d09b7b21fddbf5d8df901a44b54b4ef26ea71db92de0b1a12

in  Prelude

works fine when offline, so long as it’s been accessed once by Dhall.

That is of course separate from the question of should the prelude be accessible without ever having been online, though.


#3

This solves the problem of developing with poor internet connectivity, but regarding the problem of using Dhall in sandboxed environments, the only solution I can come up with right now is to manually git clone the Prelude somewhere. This also means that scripts have to patched to work in sandboxed environments and in general feels inelegant. :wink:


#4

@blitz: I’ll present a few options that are available today and if none of them are satisfactory we can discuss what user experience or workflow would work best for you.

If you need to be able to edit and iterate on a dhall expressions in an offline environment, then one option is the dhall freeze subcommand, which you can use like this:

-- ./example.dhall

let Prelude = https://prelude.dhall-lang.org/v13.0.0/package.dhall

in  Prelude.Bool.not True
$ dhall freeze < ./example.dhall 
-- ./example.dhall

let Prelude =
      https://prelude.dhall-lang.org/v13.0.0/package.dhall sha256:4aa8581954f7734d09b7b21fddbf5d8df901a44b54b4ef26ea71db92de0b1a12

in  Prelude.Bool.not True

That would then store the Prelude in an offline cache underneath ~/.cache/dhall by default, but you can change the directory that it uses with the XDG_CACHE_HOME environment variable, like this::

$ XDG_CACHE_HOME=/path/to/offline_cache dhall freeze < ./example.dhall

… and then you can share whichever cache you use with the offline environment. This is an example of one place we can improve tooling (such as by making it easier to publish and subscribe to caches, like Nix does).

Another option is similar to the one you suggested afterwards, which is to swap out the Prelude if it is available locally, but fall back to a remote import if not. You can do this with the language’s support for fallback imports, like this:

-- ./example.dhall

let Prelude =
        env:DHALL_PRELUDE
      ? /usr/share/dhall/Prelude
      ? https://prelude.dhall-lang.org/v13.0.0/package.dhall

in  Prelude.Bool.not True

The above program checks:

That lets you override the Prelude with an offline version when working in an offline environment.

If you have no intention of editing the file further and just need some offline environment to be able to non-interactively interpret the expression, then you can inline all imports within your file, using dhall resolve, like this:

$ dhall resolve --file ./example
let Prelude =
      { Bool =
          { and =
                λ(_ : List Bool)
              → List/fold
                  Bool
                  _
                  Bool
                  (λ(_ : Bool) → λ(_ : Bool) → _@1 && _)
                  True
…
                          }
                        → _@1
                    , text : Text → _@1
                    }
                  )
              → _.text _@2
          }
      }

in  Prelude.Bool.not True

If none of those work for you, then perhaps suggest what user experience would be ideal for you and we can use that to inspire improvements to the tooling.


#5

Thanks for the detailed response. This is very helpful!

I’m going to see which option lends it self best to packaging in Nix and report back.


#6
let Prelude =
        env:DHALL_PRELUDE ? https://prelude.dhall-lang.org/v13.0.0/package.dhall

This works the best for now, because I can just populate the environment variable from builtins.fetchgit in Nix. The downside of this solution is of course that there is no way to write Dhall files that use the Prelude offline without agreeing where to get it from. Using URLs as module names is in some way nice, but then ties your module system to actually having network available.

One quick question: Is there any documentation on the ? operator?


#7

See https://github.com/dhall-lang/dhall-lang/blob/master/standard/imports.md, at the bottom of the page.

I’m not sure precisely what the problem is. You might be interested in the pattern of collecting dependencies in separate files that the rest of your code can import relatively. See e.g.


#8

The downside of this solution is of course that there is no way to write Dhall files that use the Prelude offline without agreeing where to get it from.

See e.g.

Every Dhall expression in that repository then has let Prelude = (./imports.dhall).Prelude or let Kubernetes = (./imports.dhall).Kubernetes etc.


#9

@blitz: There actually is a way to use the Prelude offline without agreeing where to get it from, by using integrity checks. If you freeze the import it does exactly what you requested:

https://prelude.dhall-lang.org/v13.0.0/package.dhall sha256:4aa8581954f7734d09b7b21fddbf5d8df901a44b54b4ef26ea71db92de0b1a12

The reason why is because the hash takes precedence over the URL for resolving the package if the import is present in the cache. For example, a little known fact is that this is valid Dhall code:

-- missing is an import that always fails
missing sha256:4aa8581954f7734d09b7b21fddbf5d8df901a44b54b4ef26ea71db92de0b1a12

The above code works so long as version 13.0.0 of the Prelude is locally cached. However, it’s typically better to include both the URL and the hash so that:

  • When the user is online and their cache is empty, they can use dhall resolve to fetch all imports and populate the cache
  • When the user is offline and their cache is full, the imports continue to work

This works because the hash has both of the properties that you were looking for in a “package”:

  • It’s globally valid, meaning that a hash always resolves to the same import (if it succeeds) regardless of the context
  • It works offline is the package is already “installed” (resolved at least once in this case)

Or in other words, you can do “traditional package management” in Dhall using the binary cache as the package distribution mechanism and the hashes as globally unambiguous identifiers.

For Nix integration specifically, one approach that builds upon that idea is to add a buildDhallPackage Nix utility whose input is Dhall source code and whose output is a derivation that returns the binary encoding of the fully interpreted expression

In other words, something like this:

let
  buildDhallPackage =
    { name, code }:
      let
        file = pkgs.writeText "${name}.dhall" code;

      in
        pkgs.runCommand "${name}.cbor" {} ''
          ${pkgs.dhall}/bin/dhall encode --file ${file} > $out
        '';

… and then provide a withDhallPackages utility that, given a list of Dhall expressions returns a populated binary cache that your Dhall code can use to resolve imports offline.


#10

Here is a more complete illustration of my previous comment:

let
  nixpkgs = builtins.fetchTarball {
    url    = "https://github.com/NixOS/nixpkgs/archive/e3a9318b6fdb2b022c0bda66d399e1e481b24b5c.tar.gz";
    sha256 = "1hlblna9j0afvcm20p15f5is7cmwl96mc4vavc99ydc4yc9df62a";
  };

  overlay = pkgsNew: pkgsOld: {
    buildDhallPackage =
      { name, code, dependencies ? [] }:
        let
          file = pkgsNew.writeText "${name}.dhall" code;

        in
          pkgs.runCommand "${name}" { inherit dependencies; } ''
            set -eu

            ${pkgsNew.coreutils}/bin/mkdir -p cache/dhall

            for dependency in $dependencies; do
              ${pkgsNew.xorg.lndir}/bin/lndir -silent $dependency cache/dhall
            done

            export XDG_CACHE_HOME="$PWD/cache"

            ${pkgs.dhall}/bin/dhall --alpha --file '${file}' > ./tmp.dhall

            HASH="$(${pkgs.dhall}/bin/dhall hash <<< ./tmp.dhall)"

            mkdir "$out"

            ${pkgs.dhall}/bin/dhall encode --file ./tmp.dhall > "$out/''${HASH/sha256:/1220}"
          '';

      haskellPackages = pkgsOld.haskellPackages.override (old: {
          overrides =
            pkgsNew.lib.composeExtensions
              (old.overrides or (_: _: {}))
              (haskellPackagesNew: haskellPackagesOld: {
                  dhall = haskellPackagesOld.dhall_1_29_0;
                }
              );
        }
      );
  };

  pkgs = import nixpkgs { config = {}; overlays = [ overlay ]; };

  # Simplest solution if the Prelude dependency can be prebuilt and cached in an
  # environment with remote access
  online-prelude = pkgs.buildDhallPackage {
    name = "prelude-13.0.0";

    code = "https://prelude.dhall-lang.org/v13.0.0/package.dhall";
  };

  # More sophisticated solution if you want prefer to use Nix to fetch remote
  # dependencies when bootstrapping things
  offline-prelude = pkgs.buildDhallPackage {
    name = "prelude-13.0.0";

    code =
      let
        src = pkgs.fetchFromGitHub {
          owner = "dhall-lang";

          repo = "dhall-lang";

          rev = "48db9e1ff1f8881fa4310085834fbc19e313ebf0";

          sha256 = "0kg3rzag3irlcldck63rjspls614bc2sbs3zq44h0pzcz9v7z5h9";
        };

      in
        "${src}/Prelude/package.dhall";
  };

  example = pkgs.buildDhallPackage {
    name = "example";

    code = ''
      let Prelude = https://prelude.dhall-lang.org/v13.0.0/package.dhall sha256:4aa8581954f7734d09b7b21fddbf5d8df901a44b54b4ef26ea71db92de0b1a12

      in  Prelude.Bool.not True
    '';

    dependencies = [ offline-prelude ];
  };

in
  example

The idea is that a Dhall “package” is just a pre-populated cache directory.

When you build a Dhall expression like the example expression above then by default (if you don’t specify any dependencies) it will attempt to fetch them, like normal. However, if you add dependencies to a Dhall expression (such as offline-prelude or online-prelude) then they will satisfy the integrity checks as a cache hit and avoid the remote fetch.

You can bootstrap the system in one of two ways, which the online-prelude and offline-prelude illustrate:

  • online-prelude: Just have the dependency build in an online environment
  • offline-prelude: Use Nixpkgs’s built in utilities to fetch offline dependencies

Building the above example gives:

$ nix-build test.nix
…
building '/nix/store/z1l5ms0f98krk5if7fnm9ks3iy472ic3-prelude-13.0.0.dhall.drv'...
building '/nix/store/018klmgl4f48h9lgzj1pqq1j9wbz6ajc-prelude-13.0.0.drv'...
building '/nix/store/hf19la93b2w9cqx7w7fz6cjiyka1y07x-example.drv'...
/nix/store/ln8v6sa62wx00dz03gl8p8appshi9kmb-example

$ dhall decode < result/12202017ff3461395672aa0aa4f64894fd2f95a4b120e2690e8951656d79adc2eed2 
False

I’ll probably make a pull request to Nixpkgs to add these utilities after polishing them up a bit.


#11

Alright, I finally polished up the Nix code and I have a pull request out adding Nixpkgs support for fully offline Dhall builds:

… which includes a fully offline build for the largest package in the ecosystem: dhall-packages-0.11.0!

Even if you would like to implement offline builds for a package manager other than Nix you should consult that pull request as it documents what I consider to be the idiomatic way to do so.