Module backlog 

The work still running while a run goes on, and the one place it is stopped.

runtime::turn consumes an interruption at a phase boundary. A child process waited on inside a system call is not at a phase boundary, so a command blocked there cannot be stopped. Every command therefore enters this table before it is waited on: the wait is a bounded number of short polls against a member somebody else can reach, rather than one blocking call nobody can interrupt.

Two facts about the wait are deliberate. It is counted rather than timed, because the clock is sampled at one point in this city and a module that sampled it to wait ten seconds would be the second one. And a child’s output goes to files rather than to pipes, because a pipe buffer that fills stops the child inside a write — which is the same hang this module exists to remove, wearing another name.

How many polls that wait is, and how an ending is read, both belong to waiting: the window is carried by the table rather than read from a constant here, so a caller can choose one short enough to observe both answers.

The table has two kinds of member: a background command, which a halt kills, and a run a resident handed down, which a halt marks and which stops itself at its next safe point by asking Backlog::stopping (crates/runtime/spec/Backlog.lean §8-28-2). One table, one halt, so a stopped scope has nothing left going in it under either name.

Re-exports

pub use waiting::Exit;

pub use waiting::PollBudget;

pub use waiting::Unseen;

Modules

waiting

How long a caller waits for a child, and how that child’s ending is read.

Structs

Backlog

The table itself. Cloning gives another handle onto the same table, which is how the assembly point can stop what a tool started without either of them knowing about the other. A clone carries scratch too, so it keeps naming that backlog’s directories.

BacklogId

One member of the table, for as long as this process lives.

Chunk

One piece of output, in the order it was written to its stream.

Finished

A member that has stopped, collected once and then forgotten.

RunProcesses

The processes one run has in the backlog right now.

Sink

Where the pieces go. A backlog without one reads nothing at all, so a city nobody watches pays for none of this.

Standing

A member that is still running.

Enums

BacklogKind

Which of the two kinds of member a standing entry is.

Started

What the short window came to. Exhaustive rather than an optional handle: “it finished” and “it is still going” are two different things for the caller to say to a model, and a None would leave which one it was to be inferred.

Stream

Which of a command’s two outputs a piece came from.