curriculum-project-hub/docs/adr/0010-diagnostics-legal-lesson-and-check-pipeline.md

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).