Expand description
Red, and how far it reaches.
The part crates/kernel/spec/Blockage.lean specifies this module.
Red is not a new mechanism. Every source of it is a fact the city
already records — a run that froze without citing anything, a door
that has waited too long for a person, crate::stall finding a run
going nowhere, or a resident saying in as many words that it is
stuck. This module answers the one question those facts do not: given
that 2.3.1 is red, what else in the plan cannot move?
The answer names the source, not the symptom. A plan with one real problem produces one blockage that says which node it is and which nodes are waiting behind it, rather than seventeen red dots a person has to trace back by hand. That is the whole reason to propagate at all: the first screen has room for a cause, not for a list of consequences.
Red travels two ways, and both are the same relation seen from two sides: up the tree, because a branch whose child is stuck is stuck, and along the dependency edges, because a node that waits for a red node waits for something that is not coming. Nothing here reads a clock or a disk; the caller supplies the facts and gets a verdict.
Structs§
- Blockage
- One cause and everything waiting behind it.
- Notice
- Somebody to tell, and what about.
- RedNode
- One node the city has a reason to call red.