typeof Derivation
Derivation
In this blog entry I will try to find the right type abstraction of the Derivation type
Properly typing Derivation is one of the most important steps in nix to fully understand how the build system works, and how it can be expressed from a type perspective.
The
typeabstraction is a very powerful way to condensate the most important information. In my opinion.
builtins.derivation is not a builtin
builtins.derivation is not an actual primop it is a wrapper around builtins.derivationStrict. But no user would actually call derivationStrict, usually everything in nixpkgs and every other nix framework calls mkDerivation which is an opinionated wrapper around derivation.
Lets start with the first layer of abstraction. We will see how the derivation function is created out of derivationStrict
The following code block is the actual implementation of builtins.derivation by the time of this writing. And can be found here:
https://github.com/NixOS/nix/blob/master/src/libexpr/primops/derivation.nix
/* This is the implementation of the ‘derivation’ builtin function.
It's actually a wrapper around the ‘derivationStrict’ primop. */
drvAttrs @ { outputs ? [ "out" ], ... }:
let
strict = derivationStrict drvAttrs;
outputsList = map outputToAttrListElement outputs;
commonAttrs = drvAttrs // (builtins.listToAttrs outputsList) //
{ all = map (x: x.value) outputsList;
inherit drvAttrs;
};
outputToAttrListElement = outputName:
{ name = outputName;
value = commonAttrs // {
outPath = builtins.getAttr outputName strict;
drvPath = strict.drvPath;
type = "derivation";
inherit outputName;
};
};
in (builtins.head outputsList).value
What is referred to as Derivation?
Very often in nixpkgs we often see type comments like this:
toDerivation :: Path -> Derivation
but also
builtins.derivation :: { ... } -> Derivation
and
stdenv.mkDerivation :: { ... } -> Derivation
Nix uses Derivations everywhere. It encapsulates one of its core concepts. But are all of these Derivations of the same type?
How can we express the type of Derivation?
Typeof Derivation
To express the type of Derivation we first need a way to express types in this post i will use the syntax of type system that i introduced here in a proposal for unifying the comment syntax for types.
Lets have a look at the type of the primop derivationStrict
derivationStrict :: {
name :: String;
outputs :: String;
builder :: String;
system :: String;
} -> {
drvPath :: String;
${output} :: String;
}
derivationStrict returns at least the drvPath which is set to a nix/store/<path>.drv where the drv file is located at. Also it holds one attribute for every space seperated output.
Like
outputs = "out doc lib"
would return
{
drvPath="nix/store/<hash>.drv";
out="nix/store/<hash>";
doc="nix/store/<hash>";
lib="nix/store/<hash>";
}
Lets have a look at the type of the builtins.Derivation now:
We do this by adding type annotations to every expression during construction of the internal builtins.derivation function
I soon found out that Derivation is a recursive, dependent type.
It is recursive, as it has itself in the all attribute and every entry declared in outputs is a Derivation itself.
And it is dependent because its final type depends on the value of input attributes.
If the following is to much information overload for you, go right to the end of this post, where you can find the final type.
/* This is the implementation of the ‘derivation’ builtin function.
It's actually a wrapper around the ‘derivationStrict’ primop. */
/*
Type:
{
outputs :: ? [ String ];
${additionalArg} :: a;
}
*/
drvAttrs @ { outputs ? [ "out" ], ... }:
let
/*
Type:
{
name :: String;
outputs :: ? String;
builder :: String;
system :: String;
${additionalArg} :: a;
} -> {
drvPath :: String;
${output} :: String;
}
*/
strict = derivationStrict drvAttrs;
/*
outputs :: [String] is transformed using the outputToAttrListElement
Type:
[
{
name :: String;
value :: {
outPath :: String;
drvPath :: String;
type :: "derivation";
${outputName} :: String;
${commonAttrs} :: Any;
}
}
]
*/
outputsList = map outputToAttrListElement outputs;
/*
{
name :: String;
outputs :: ? String;
builder :: String;
system :: String;
${additionalArg} :: String;
} // {
${name} :: Derivation
} // {
all :: [ Derivation ]
drvAttrs :: {
outputs :: [ String ];
${additionalArg} :: a;
}
}
*/
commonAttrs = drvAttrs // (builtins.listToAttrs outputsList) //
{ all = map (x: x.value) outputsList;
inherit drvAttrs;
};
/*
String -> {
name :: String
value :: {
outPath :: String;
drvPath :: String;
type :: "derivation";
outputName :: String;
${commonAttrs} :: Any;
}
}
*/
outputToAttrListElement = outputName:
{ name = outputName;
value = commonAttrs // {
outPath = builtins.getAttr outputName strict;
drvPath = strict.drvPath;
type = "derivation";
inherit outputName;
};
};
/*
This returns the value attribute o the first element
in the outputsList
which I found to be a recursive expression:
commonAttrs =
drvAttrs //
outputsList.asAttrSet //
{all= valuesOf outputsList; drvAttrs=drvAttrs;}
outputsList =
map outputs over -> outputName:
[
{ name=outputName; value=commonAttrs//{...}; }
]
*/
in (builtins.head outputsList).value
So i find the type of builtins.derivation:
# As returned by builtins.derivation
Derivation :: {
all :: [ Derivation ];
builder :: String;
drvAttrs :: {
builder :: String;
name :: String;
outputs :: [ output :: String ];
system :: String;
${additionalArg} :: a;
}
drvPath :: String;
name :: String;
outPath :: String;
outputName :: String;
outputs :: [ output :: String];
system :: String;
type :: "derivation";
${output} :: Derivation;
${additionalArg} :: a;
};
This type cannot be seen as a standalone type because it is a dependent type. It depends on the input attributes and of the input values of builtins.derivation
Final Type
To get the final type we also need to resolve the type constraints for the type variable a that was introduced here.
a :: String
actually derivation accepts more types here: -> everything that can be coerced into string
I also added the special args keyword which is one of the possible additionalArg but it is passed as cli argument to the builder.
Every other additionalArg is passed as env variable instead.
With the type syntax proposed here
it is possible to write the following expression for the type of derivation
using the
let insyntax that we all know and love. 😁
let
Derivation :: {
all :: [ Derivation ];
builder :: String;
drvAttrs :: {
builder :: String;
name :: String;
outputs :: [ output@String ];
system :: String;
args :: [ String ]?;
${additionalArg} :: String;
}
drvPath :: String;
name :: String;
outPath :: String;
outputName :: String;
outputs :: [ output@String ];
system :: String;
type :: "derivation";
args :: [ String ]?;
${output} :: Derivation;
${additionalArg} :: String?;
};
in
{
name :: String;
outputs :: [ output@String ]?;
builder :: String;
system :: String;
args :: [ String ] ?;
${additionalArg} :: String?;
} -> Derivation
#builtins.derivation
Adding more attributes to the builtins.derivation call adds those as environment variables.
The logic can be seen below:
# additionalArg
# e.g. derivation {... more="foo"; }
export more='foo'
# common PATHs
export HOME='/homeless-shelter'
export NIX_BUILD_CORES='0'
export NIX_BUILD_TOP='/build'
export NIX_LOG_FD='2'
export NIX_STORE='/nix/store'
export PATH='/path-not-set'
export PWD='/build'
export SHLVL='1'
export TEMP='/build'
export TEMPDIR='/build'
export TERM='xterm-256color'
export TMP='/build'
export TMPDIR='/build'
export builder='/nix/store/a600x16bxc1qks8rbgalj5vaixgbxdhj-builder.sh'
export name='simple'
export out='/nix/store/y5n7k4hachqzih2i9pwi4wkkd9i97swl-simple'
export system='x86_64-linux'
Thanks for reading and have good time. I hope this was helpful and interesting
Edit: refactor the type expression to be conform to the proposed type language