Expand description
The plan as a tree: what the nodes are, what each one is worth, what
may be started now, and the two ways a held node is put down.
The part crates/kernel/spec/Plan.lean specifies this module.
crate::spine owns the document — how a row is written and read.
This module owns the structure that document describes, and the two
are separate because the grammar of a line and the arithmetic of a
plan fail in different ways: a mistyped row is repaired by editing
it, while a cycle in the dependencies is repaired by rethinking the
work.
Weight is conserved because crate::share is the only way to
hold any. A node’s share is divided out of its parent’s when the
tree is built, so the total is 1 whatever the plan turns into and no
version number is needed for the denominator. What grows when a
branch is split is the number of leaves, not the total; that is why
the interface shows both — a percentage says how much is done and a
leaf count says how much was found.
Progress is counted on leaves only. A branch has no work of its
own: its children are its work, and counting both would count the
same effort twice. A branch that says Done while a child does not
is refused where the tree is built, so the status column of a branch
is a summary a reader can trust rather than a second opinion.
Structs§
- Held
- A node this run holds.
- Plan
Node - One node, placed: the row as written plus what the tree worked out.
- Plan
Tree