check: uncatchable evaluation errors abort the run instead of failing a case #17

New issue

Open

opened 2026-09-14 02:04:01 +09:00 by natsukium · 0 comments

natsukium commented

2026-09-14 02:04:01 +09:00

Owner

Bug

builtins.tryEval catches throw and a failed assert and nothing else, so a
predicate that hits a type error, builtins.head [], division by zero or
infinite recursion aborts the whole run rather than failing one case. The README
says so since #15; what it does not say is how often that happens, which decides
whether the current design is good enough.

Measurement

34 nixpkgs lib functions, one process per property, each asked only whether it
produces a value on input of the shape it declares. Outcomes classified by exit
code: PASS, REPORTED (a counterexample came back), ABORT (the evaluation
died).

generators	PASS	REPORTED	ABORT
the declared shape (lists to list functions, strings to string functions)	26	5	3
`gen.anything`	3	2	29

Of the properties that did not pass, 3 of 8 aborted with typed generators and
29 of 31 — 94% — with gen.anything.

So testing well-typed code works today. Sweeping an unfamiliar API, which is
what examples/nixpkgs-lib-comprehensive.nix is for and what the README calls
the "run nixcheck against the whole surface" target, mostly does not: the
interesting outcomes are almost all aborts with no counterexample and no
shrinking. The curated examples abort zero times only because they were written
to pass.

The sharpest part is an asymmetry the caller cannot predict:

function	empty list	outcome
`lib.head`, `lib.tail`	aborts the run	no counterexample
`lib.init`, `lib.last`	fails the case	shrinks to `[]`

Same failure, opposite behaviour, purely because the latter pair use throw
while the former call a builtin. Whether a user gets a counterexample depends on
an implementation detail of the function under test.

Suggested fix

Diagnose out of process, on demand. An uncatchable error is invisible from
inside the evaluator but perfectly visible from outside it, and shrink-tree
nodes are already addressable as (case index, path of child indices):

peek returns a node's value and child count without applying the
predicate, so it always evaluates.
judge applies the predicate and lets the process die; the exit code is the
verdict.

Greedy descent over those verdicts reproduces shrinking at about one nix eval
per candidate, run only after a run has already aborted. Verified on a
division-by-zero predicate: [1,0,1,4,4,4,4,4,1] shrank in 7 steps and 8
judging processes.

This needs no library change — sampleTree plus the { value; shrinks; } shape
is enough for a driver to walk the tree from the expression it passes to
nix eval.

Note that the shrunk result above is [0,0,0,0,0,0], not [0]. That is the
existing greedy shrinker finding a local minimum, as the README already
describes; out-of-process diagnosis makes it more visible but does not cause it.

If that does not work

Host the runner in Rust on the Nix C API. Catching a predicate's evaluation
error requires being the host, which is the same reason nix-unit links the
evaluator rather than shelling out to nix eval.

This is not a thin adapter: the predicate application, the case loop, the shrink
walk and the label/cover accumulation all move out, so lib/property.nix gets
reimplemented. Generators, ranges, trees and the rng stay in Nix either way —
they are the user-facing API and they are good because they are Nix values.

The C API is the smaller surface than nix-unit's C++ route, but the Nix manual
still calls it in development and explicitly not stable, so this is a bet rather
than a free win. Only take it if the diagnosis driver proves unworkable in
practice.

## Bug `builtins.tryEval` catches `throw` and a failed `assert` and nothing else, so a predicate that hits a type error, `builtins.head []`, division by zero or infinite recursion aborts the whole run rather than failing one case. The README says so since #15; what it does not say is how often that happens, which decides whether the current design is good enough. ## Measurement 34 nixpkgs `lib` functions, one process per property, each asked only whether it produces a value on input of the shape it declares. Outcomes classified by exit code: `PASS`, `REPORTED` (a counterexample came back), `ABORT` (the evaluation died). | generators | PASS | REPORTED | ABORT | | --- | --- | --- | --- | | the declared shape (lists to list functions, strings to string functions) | 26 | 5 | 3 | | `gen.anything` | 3 | 2 | 29 | Of the properties that did not pass, 3 of 8 aborted with typed generators and 29 of 31 — 94% — with `gen.anything`. So testing well-typed code works today. Sweeping an unfamiliar API, which is what `examples/nixpkgs-lib-comprehensive.nix` is for and what the README calls the "run nixcheck against the whole surface" target, mostly does not: the interesting outcomes are almost all aborts with no counterexample and no shrinking. The curated examples abort zero times only because they were written to pass. The sharpest part is an asymmetry the caller cannot predict: | function | empty list | outcome | | --- | --- | --- | | `lib.head`, `lib.tail` | aborts the run | no counterexample | | `lib.init`, `lib.last` | fails the case | shrinks to `[]` | Same failure, opposite behaviour, purely because the latter pair use `throw` while the former call a builtin. Whether a user gets a counterexample depends on an implementation detail of the function under test. ## Suggested fix Diagnose out of process, on demand. An uncatchable error is invisible from inside the evaluator but perfectly visible from outside it, and shrink-tree nodes are already addressable as `(case index, path of child indices)`: - `peek` returns a node's `value` and child count without applying the predicate, so it always evaluates. - `judge` applies the predicate and lets the process die; the exit code is the verdict. Greedy descent over those verdicts reproduces shrinking at about one `nix eval` per candidate, run only after a run has already aborted. Verified on a division-by-zero predicate: `[1,0,1,4,4,4,4,4,1]` shrank in 7 steps and 8 judging processes. This needs no library change — `sampleTree` plus the `{ value; shrinks; }` shape is enough for a driver to walk the tree from the expression it passes to `nix eval`. Note that the shrunk result above is `[0,0,0,0,0,0]`, not `[0]`. That is the existing greedy shrinker finding a local minimum, as the README already describes; out-of-process diagnosis makes it more visible but does not cause it. ## If that does not work Host the runner in Rust on the Nix C API. Catching a predicate's evaluation error requires being the host, which is the same reason nix-unit links the evaluator rather than shelling out to `nix eval`. This is not a thin adapter: the predicate application, the case loop, the shrink walk and the label/cover accumulation all move out, so `lib/property.nix` gets reimplemented. Generators, ranges, trees and the rng stay in Nix either way — they are the user-facing API and they are good because they are Nix values. The C API is the smaller surface than nix-unit's C++ route, but the Nix manual still calls it in development and explicitly not stable, so this is a bet rather than a free win. Only take it if the diagnosis driver proves unworkable in practice.

natsukium referenced this issue from a commit

2026-09-16 01:40:02 +09:00

Run the nixpkgs lib sweep on demand, not in CI

No labels

No milestone

No project

No assignees

1 participant

Notifications

Due date

The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set

Reference

natsukium/nixcheck#17

No description provided.

Rows
Columns