The checks
Every problem flow check and library check report carries a code; this page names each, then says what formal check and formal handoffcheck verify.
The kit’s tests hold it to the scripts: a code a script can report and this page does not name fails them.
Each check ends with coverage lines saying what it looked at and what it did not, and each script’s --selftest plants one defect per code and fails when a code it can report is planted nowhere.
Exit codes
Every check exits 0 when clean, 1 when it found problems, each printed with its place, and 2 when it could not run: no bindings file at the root, or one that does not parse. The 2 is its own code so that a hook or a CI job never reads “did not run” as “clean”.
flow check
| Code | What it says |
|---|---|
| V0 | a record file cannot be read: no front matter, a value outside the subset the tool writes, a byte that is not UTF-8, or an id another file carries; the check reads the rest of the tree without it |
| V1 | the record’s type is not one of the four, it has no id, or its id does not match its filename or its type’s prefix |
| V2 | a reference field names an id that does not exist, or a record of the wrong type |
| V3 | a field is missing or unknown, or a state, kind, size, owner, status or origin is not a legal value |
| V4 | a task of a kind that needs a question has none |
| V5 | a ready task has unmet requires |
| V6 | a finding has no evidence, an evidence item does not resolve, or the status does not match the kinds of evidence present |
| V8 | a cycle through derived_from, depends_on or a question’s parent |
| V9 | an active task has no owner, or an owner holds more active tasks than its hand limit |
| V10 | a decomposed question has no task |
| V11 | the index is missing or stale — run flow index |
| V12 | an open or decomposed question has no last-checked date |
| V13 | an open task sits under a question that is neither open nor decomposed |
| V14 | a rank on a closed record, on owner-only work or on a parked question, a ranked record with no why_now or first_move, two records at one rank, or ranks that are not 1..n |
| V15 | a parking block that is not a map with a date and a reason, or on a question that is not open |
| V16 | a current question has no kill criteria |
| V17 | an abandoned record has no dated reason, or a consumed idea has no question deriving from it |
| V18 | an answered question names nothing it is answered by, or names a task that is not done or not drawn under it |
| V19 | a body is not one sentence per line |
| V20 | a date — created, checked, drawn, a parking’s or an abandonment’s — is not an ISO date or is in the future, or a done task still carries an owner |
| V21 | a record is not in its type’s directory, a closed task is not in the archive, or an open one is |
| V22 | a question’s direction names no bullet of the directions file |
| V23 | a record cites a library key the library does not hold, or an extract its card does not carry; or the library did not answer |
The codes are names, not a sequence: V7 is unassigned. The one warning (which does not fail the check) names a decomposed question whose tasks are all closed, which needs refine or answer.
library check
| Code | What it says |
|---|---|
| L0 | a card’s front matter cannot be read: it is outside the subset the tool writes |
| L1 | the file’s name is not lowercase letters, digits and hyphens, or the key is not the file’s name |
| L2 | a field is missing, unknown or of the wrong shape, a kind the project does not list, a title missing, a year that is not a number, metadata or verified incomplete |
| L3 | two cards carry the same identifier |
| L4 | a read grade is not one of the four, a read without its date or, for a work read in parts, without which parts; an ungraded card that is not seeded |
| L5 | via, related or a body citation names a card that does not exist, a related card that does not name this one back, or an extract the cited card does not carry |
| L6 | a copy without a path and a hash, outside the store or the kept directory, or not matching its recorded hash |
| L7 | a state not among the legal ones, an excluded card without its reason and date, a registered card with an exclusion |
| L8 | a date that is not an ISO date or is in the future, or a card without its created date |
| L9 | a body is not one sentence per line |
| L10 | a body that is not ## Notes then ## Extracts with nothing before them |
| L11 | the index is missing or stale — run library index |
| L12 | a reference entry of a bound document that no card agrees with, that two cards agree with, or that names an internal document |
| L13 | a work a bound document cites is graded unread and names no via |
| L14 | the watch file or the candidates file cannot be read |
| L15 | an extract the kept copy does not bear out: its quotation is not in the kept text, or its locator names a section, page or statement that is not |
| L16 | an extract is malformed — its id, locator, words, caveat, rule or date — or its checked date is not a date or is in the future, or an unread card with no via carries an extract |
| L17 | a card naming a project file whose file is not in the tree or whose kind is not internal, an internal document recording another copy, or a card of an internal kind naming no file |
formal check
With the formal plugin, formal check reads formal.toml and reports, in words rather than codes:
- a workspace that is not a directory, or the prover session’s instructions file missing;
- a package root with neither
<Root>.leannor<Root>/under its package directory; - a declaration manifest missing, with the command that regenerates it, or a row outside the grammar
formal --helpprints.
Its coverage line names the manifests with their row counts by kind, the packages bound and the documents scanned, and says the prover tree itself is neither built nor read.
formal handoffcheck
formal handoffcheck DRAFT checks the decidable shape of a prover handoff before it is sent, never its content:
- one
<prompt session=fresh>or<prompt session=continue>block, closed, with nothing after the closing tag, and acontinuethat states its reason; - none of the phrases
formal.tomlbans; - a record named as a source carries the docstring-register warning;
- paths relative to the workspace, the project’s own directories written
../; - a
Refute first:line and aCommissioned:line naming the declarations (ornone —and why); - a bundle of two or more pieces with a
Bundle shape:line and a sentence keeping its own words out of the docstrings.
A draft with no prompt block exits 2, since there was nothing to check; the handoff skill says what each line is for.