Module pursuit 

A pursuit: a goal the city keeps working towards, and the one condition under which a city that holds one stops. The part crates/kernel/spec/Pursuit.lean specifies this module.

The construction plan called this Endless. It is named for what it is rather than for how long it lasts, because three other things in this repository are already called standing something.

A society does not stop because somebody shouts stop. It stops because there is nothing ready to do. That is the whole criterion: the ready set is empty and no run is still going. Both halves are needed — an empty ready set while four runs are working means the work is in somebody’s hands, not that it is finished.

Money is deliberately not a criterion. The cost surface in this city is material an agent optimises against, not a brake somebody pulls, and a stop condition that read a budget would answer a question nobody here asked.

A pursuit is the person’s, and a delegate cannot declare one. Pursuit::declare takes the depth-zero position by reference, and a Delegate value has no way to produce one — the same two-layer guard crate::delegation uses, for the same reason: a sub-agent that could set the city working until it runs out of work is a sub-agent that can spend the night on its own idea.

Pausing and clearing are different actions and both exist. Pause keeps the goal and stops taking work; clearing is dropping the value, so a cleared goal leaves nothing behind to be resumed by accident. Cancelling a run is a third thing again, and it lives where runs do.

Structs

Pursuit

A goal that keeps taking work until the work runs out.

Enums

PursuitState

Whether a pursuit is taking work right now.

PursuitVerdict

What a city holding a pursuit does next. Exhaustive: every arm is something the caller has to do, and a fifth would be a state nobody wrote an action for.

Functions

observe

The stop condition, as a pure function of what the plan says and what is running.