doc: explain assert condition -> package != null;

[Anton-Latukha]

Issue description

There are a plethora of:

{ enableFeature ? false, package ? null
}:

assert enableFeature -> package !=null;

And this assertion broke my head for a long time. Major part of the year.

I know some Haskell.
I was a Haskell/NixPkgs/Nix/NixOps DevOps, contributed to some number of Nixpkgs, become a maintainer of some packages.

I dig into this question a couple of times, and extracted sort-of answer.
I found Dolstra explanation somewhere on GitHub couple of times. That is hard to find, even when you specifically look for it.

But. I still didn't understood that assertion fully.

Until I admitted dumbness and asked in the chat room.

-> can be a sign of a function, a sign of a binding, and a sign of implication.

But because of what is the resulting expression: package !=null; - it is not a result, it does not evaluate to anything, it is not used. I thought that -> is probably or a binding, or a function sign, but it behaved as an assertion, which broke my head completely.

Please write something in lines:

There are number of option->dependency, option->option checks in the code.

{ enableFeature ? false, package ? null
}:

assert enableFeature -> package !=null;

-> is the sign of implication
So assertion can be read as (if enableFeature == True then test that package !=null).
This accert structure checks that when condition is true package must be used in the expression.

And if, after binding values to variables, expression package !=null evaluates to False, so all that assert expression evaluates to False, which puts False in the global scope on that Nix (package) expression, which as result throws Error, so evaluation/build stops.

That is how that accert structure guides the options conditions.

If that accert is one - it is probably useless, as it tests the already working code that has logical expressions (optional) in it and that evaluates normally.

Number of accerts are needed to sort-out collisions between options of the package, for example when one option requires package to be included, and other option - to be excluded, and the third...

---

And moreover.

Manual shows:

assert e1; e2;

Which is the same as

assert e1 -> e2;

Which multiplies confusion, that -> must be some special sign for some special case of accert.

Steps to reproduce

Read the Nixpkgs code.

[orivej]

-> is not a syntax for assert, it is a generic boolean function, like && and ||: https://nixos.org/nix/manual/#sec-language-operators. e1 -> e2 is equivalent to !e1 || e2.

assert e1; e2 is an expression those value is e2 if e1 is true, and which aborts evaluation if e1 is false. assert e1 -> e2; e3 is an expression those value is e3 if e1 -> e2 is true, and which aborts evaluation if e1 -> e2 is false. (Since -> is a boolean function, e2 has to be a boolean value in this example, otherwise evaluation aborts with a type error.)

[Anton-Latukha]

OK. Now I know that the whole tail expression after assert in those cases is a resulting expression if the whole e1 - > e2is true.

OK, thank you.

[Anton-Latukha]

e1 -> e2 is if e1 then e2 else True
And e1; e2 is if e1 then e2 else False

They are both are if ... then ... else ... structures, that is why they look they are the same thing, interchangeable, but different notation, I thought one of them (the ->) is legacy, since not in the documentation.

{ enableFeature ? false, package ? null
}:

assert enableFeature -> package !=null;

stdenv.mkDerivation rec {}

is:

if (if enableFeature then package !=null else True)
  then stdenv.mkDerivation rec {}
  else False

[jtojnar]

And e1; e2 is if e1 then e2 else False

There is no such thing as e1; e2 in Nix. The semicolon only makes sense as a separator in let…in or assert construct.

You could compare the assert e1; e2 expression to if…else expression, but it would not return false in the else branch, but a bottom:

if (if enableFeature then package !=null else True)
  then stdenv.mkDerivation rec {}
  else error "assertion failed"

[Anton-Latukha]

Yes. This is in a more strict terms.

[Anton-Latukha]

So all this volume (first round of explanations was in a chatroom), seems to indicate the need to explain example of this often used, but strangely looking case of assert in a documentation.

Assumption that people would/should deduce it themselves with full understanding, is a very long shot.

[jtojnar]

Well the -> is a built-in operator in Nix. I would expect people to at least familiarize themselves with the syntax of Nix, which is described in the Nix manual.

[Anton-Latukha]

I read it, it was more than a half year ago.
And as I already said, it broke my head. Assert in manual looks like this:

assert e1; e2 #;?

and assert in real life looks like this:

{ enableFeature ? false, package ? null
}:

assert enableFeature -> package !=null;

I deliberately over exaggerate.

Asked maybe to add live example.

If you think this is obvious, ok.