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