forked from bai/curriculum-project-hub
sjfhsjfh
c684d25d50
Spec母本噪音清理 + 一处 spec↔impl 对齐 + 一处契约自洽修正。 Part A — spec doc 瘦身:每条 doc 收到"语义点 + 标签 + ADR ref + 承载性 why", 把跨文件复读的方法论(element-kind 开放性对比、likec4 画不出、分歧点测试)上移到 module header。OPEN 框架保持清晰(RunState/Capability 完整性仍明示须 surface)。 Part B — Courseware/ 由 10 文件平铺重组为 Model/ Export/ Check/ Open/ 四子命名空间 (namespace Spec.Courseware 不变,零引用改动)+ 四个子 aggregator。lake build 绿(24 jobs)。 Part C — 渲染覆盖落为数据(ADR-0011 对齐):去掉 cph-check 里硬编码的 COVERED_TARGETS,改读 TargetConfig.covers。cph-model 新增 covers: Option<Vec<String>> (None=未声明,由 cph-check 默认为全部 known kinds;显式 [] 表示不覆盖任何 kind)。 新增 3 个覆盖行为测试。 ADR-0012 — DanglingReference 退役(诊断 7→6 类):其两种情形(未解析 @ref、越界/缺失 相对 import)都是 typst 编译期失败,归 typstCompile。同步移除 Oracle.refsResolve (被 compiles 蕴含),Legal 少一个合取项。impl 删去从未被发射的 DiagCode::DanglingReference, 闭合 named-but-unemitted 的 spec↔impl 缝。ADR-0010 加修订指针。 OPEN 点(RunState/Capability 完整性、QuestionBank、Course)按既定纪律保持 OPEN,本次 只改善其框架措辞,不决策。 验证:spec lake build 绿;cargo test 全绿(含新增覆盖测试);clippy 静默; TH-141 check 0 errors/0 warnings 无回归。 Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
139 lines
8.2 KiB
Markdown
139 lines
8.2 KiB
Markdown
# 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*.
|
||
|
||
> **Corrected by ADR-0012.** The taxonomy below lists *seven* classes including
|
||
> `DanglingReference`. ADR-0012 retires `DanglingReference` — its cases
|
||
> (unresolved `@ref`, out-of-boundary `import`) are all typst compile-time
|
||
> failures, so they fold into `TypstCompile` — leaving *six* classes, and removes
|
||
> the `Oracle.refsResolve` conjunct from `Legal`. Read the taxonomy and the
|
||
> `Legal` definition here through that correction.
|
||
|
||
## 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).
|