The propagation of build inputs are explained in Nixpkgs 23.05 manual | Nix & NixOS. The section is a bit hard to understand, but I thought I had understood it. Then there comes an example in the explanation of `propagatedNativeBuildInputs`

:

For example, if package

`Y`

has`propagatedNativeBuildInputs = [X]`

, and package`Z`

has`buildInputs = [Y]`

, then package`Z`

will be built as if it included package`X`

in its`nativeBuildInputs`

. If instead, package`Z`

has`nativeBuildInputs = [Y]`

, then`Z`

will be built as if it included`X`

in the`depsBuildBuild`

of package`Z`

, because of the sum of the two`-1`

host offsets.

This gives us two examples that I’m going to write down in the style of the Natural Deduction rules in the same section

#### 1st Example

`X`

is in `propagatedNativeBuildInputs`

of `Y`

with offset `(-1,0)`

`Y`

is in `buildInputs`

of `Z`

with offset `(0,1)`

```
# Y
let mapOffset(h, t, i) = i + (if i <= 0 then h else t - 1)
dep(0, 1, Z, Y)
propagated-dep(-1, 0, Y, X)
0 + -1 in {-1, 0, 1}
0 + 0 in {-1, 0, 1}
# ->
propagated-dep(mapOffset(0, 1, -1),
mapOffset(0, 1, 0),
Z, X) = propagated-dep(-1, 0, Z, X)
```

This gives us that `X`

is in `nativeBuildInputs`

of `Z`

as stated in the example.

### 2nd Example

`X`

is in `propagatedNativeBuildInputs`

of `Y`

with offset `(-1,0)`

`Y`

is in `nativeBuildInputs`

of `Z`

with offset `(-1,0)`

```
# Y
let mapOffset(h, t, i) = i + (if i <= 0 then h else t - 1)
dep(-1, 0, Z, Y)
propagated-dep(-1, 0, Y, X)
-1 + -1 in {-1, 0, 1} # This is no true!
-1 + 0 in {-1, 0, -1}
# ->
propagated-dep(mapOffset(-1, 0, -1),
mapOffset(-1, 0, 0),
Z, X) = propagated-dep(-2, -1, Z, X)
```

This calculation gives us a propagated offset tuple of `(-2,1)`

, but the calculation is not valid because one of the conditions is not fulfilled: The host offsets sum to `-2`

.

Still, the example says that the result will be that `X`

is in `depsBuildBuild`

of `Z`

which would

correspond to `propagated-dep(-1,-1, Z, X)`

. I do not understand how to get this from the inference rules.