# ADR 0010: Checker Diagnostics, Legal Lesson, And The Check Pipeline

## Status

Accepted — for the decisions below. **Backfills the "full lesson legality"** item
ADR-0005 explicitly deferred ("the complete definition of a legal lesson; this
ADR fixes only the one seed rule"). Builds on ADR-0005's seed (missing render ⇒
warning) and ADR-0009 (target = build). Some items deferred; see *Open Questions*.

## Context

The checker is the product's moat — the thing that "stands in Lean's position" at
runtime, validating an engineering file and emitting helpful fix hints. The MVP
implementation grew a **diagnostic taxonomy** (seven codes), a notion of when a
lesson is **legal** (publishable / buildable), and an ordered **check pipeline** —
and then treated all three as "implementation detail." They are not. What each
error class *means*, whether it blocks, what "legal" *is*, and in what order
checks run with what gating are exactly the non-obvious domain decisions the
constitution (rule 5) says must be pinned: the developer and the agent would
otherwise each assume a different answer. This ADR lifts them into the contract.

A deliberate boundary runs through the taxonomy. Some checks the model can state
structurally (a manifest part points at a folder that exists; a declared kind is
known). Others are **external facilities** the semantic model cannot itself
decide — does this typst source compile? do its cross-references resolve? does
this data conform to its JSON Schema? Those are real, contractually-named
diagnostics, but their *verdict* comes from an implementation oracle (the typst
compiler, the schema validator), not from Lean. The contract names them and fixes
their severity; it does not pretend to decide them.

## Decision

### The diagnostic taxonomy (seven classes)

Each diagnostic carries a **code**, a **severity** (`error` | `warning`, per
ADR-0005 / `Spec.Courseware.Severity` — two-valued, no info/note), a message, an
optional source span, and a fix hint. The MVP classes:

| Code | Meaning | Severity | Kind |
|------|---------|----------|------|
| `PartPathMissing` | A manifest `[[parts]]` entry points at a folder that does not exist (or escapes the root via `..`). | error | structural |
| `UnknownKind` | A part declares a kind not in the known kind set (and: a part/`element.toml` kind mismatch). | error | structural |
| `MissingContentFile` | A `content` field required by the kind's schema has no corresponding `<field>.typ` on disk. | error | structural/schema |
| `SchemaViolation` | Instance data does not conform to its kind's JSON Schema (bad scalar type, missing required, stray key); also the fallback for a malformed `manifest.toml`/`element.toml`. | error | schema / external |
| `DanglingReference` | A reference does not resolve — a relative import outside the import boundary, or an unresolved cross-reference. | error | external |
| `TypstCompile` | The assembled typst source fails to compile (syntax error, unresolved `@ref`, etc.). | error | external |
| `RenderIgnored` | A used kind has no render rule for a declared target; the element is omitted from that export. | **warning** | semantic |

Six are `error` (blocking); **`RenderIgnored` alone is a `warning`** — the
ADR-0005 seed rule, restated. The split between *structural* (model decides),
*schema/external* (oracle decides), and *semantic* (the coverage rule) is the
boundary described above.

`RenderIgnored`'s severity is pinned to `warning` as a named contract fact (Lean:
`renderIgnoredSeverity`), so "it does not block export" is greppable and
alignable, not an inline literal.

### A legal lesson has no error-level diagnostic

A lesson is **legal** (valid, publishable) iff the check pipeline produces **no
`error`-severity diagnostic**. Warnings do not affect legality — a lesson with
`RenderIgnored` warnings is still legal and still exports (lossily). This is the
complete legality predicate ADR-0005 deferred: legality is defined *by the
diagnostic set*, not by a separate hand-written rulebook. New rules enter
legality by adding diagnostics, keeping one source of truth.

### External-facility diagnostics are oracle verdicts, not model judgments

`TypstCompile`, `DanglingReference`, and the schema-conformance face of
`SchemaViolation` assert facts the semantic model **cannot decide on its own**:
they depend on running the typst compiler and the schema validator. The contract
therefore models them as **abstract predicates** (e.g. "this source compiles",
"these references resolve", "this data conforms") **parameterized over an
implementation-provided oracle**. The Lean spec states *that* such a diagnostic
exists, what it means, and its severity — and explicitly marks that its truth
value is supplied by the implementation, not computed in Lean. This keeps the
contract honest (it does not embed a typst compiler) while still naming the
diagnostic as part of the legality definition.

### The check pipeline: ordered phases with compile gating

`check` runs five phases in a fixed order, collecting all diagnostics:

1. **load** — parse `manifest.toml` + each `element.toml`. A hard failure (no
   parseable lesson) stops the pipeline; nothing downstream can run.
2. **structural** — every part path exists, no `..`, kind is known, part/element
   kinds agree. Parts already flagged missing here are skipped downstream (no
   piling diagnostics on one root cause).
3. **schema** — each present, known-kind part's data validated against its kind
   schema (scalars + required content files).
4. **typst compile** — the external-facility phase. **Gated: it runs only if
   phases 1–3 produced zero errors**, because compiling known-broken input yields
   noise on top of the real cause. When it runs, it compiles each declared target
   (ADR-0009), deduping identical diagnostics across targets.
5. **render-coverage** — the semantic warning rule; runs regardless of gating.

`build --target T` runs phases 1–3, refuses (no artifact) if any error, else
compiles + exports T's artifact (ADR-0009). It does **not** run coverage —
coverage describes export loss, informational for `check`, not a gate on one
target's build.

The **order and the gating are contract**, because they determine which
diagnostics a user sees (a syntax error behind a missing file is hidden until the
file exists — deliberate). The per-phase *algorithms* are not pinned in Lean
(depth ceiling, rule 5): the spec fixes the phases, their order, and the gate, not
how each check is computed.

## Consequences

- "Is this lesson done / publishable?" has one precise answer: no error-level
  diagnostic. The CLI's exit code (1 on any error) is this predicate.
- Adding a checker rule = adding a diagnostic with a severity; legality updates
  automatically, no separate legality rulebook to keep in sync.
- The contract can name compile/reference/schema diagnostics as part of legality
  without embedding the oracles that decide them — the spec stays a semantic
  master, not a re-implementation.
- The implementation's `DiagCode` enum, `CheckReport`, and phase sequence now have
  a contract to align to (by review, per the constitution — no CI gate); the
  alignment is documented at both ends.

## Open Questions / Deferred

- **Additional codes.** A dedicated `ManifestMalformed` (today folded into
  `SchemaViolation`) and finer schema/reference codes may be added; the taxonomy
  is open to growth, each addition a deliberate decision.
- **Cross-lesson diagnostics.** Anything about a *course* (arrangement of lessons)
  or the question bank is out of scope — those models are still OPEN (ADR-0005).
- **Severity of future classes.** Each new diagnostic's blocking/non-blocking
  status is decided when introduced; only the seven above are fixed here.
- **Warning sub-structure.** Whether warnings ever need ordering/grouping or a
  third "info" level remains deferred (ADR-0005 kept `Severity` two-valued).