forked from EduCraft/curriculum-project-hub

Files

T

chore(spec+checker): cleanup pass — trim docs, reorg Courseware, covers-as-data, fold DanglingReference (ADR-0012)

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>

2026-06-22 23:59:32 +08:00

4.9 KiB

Raw Permalink Blame History

ADR 0012: Reference Resolution Folds Into `TypstCompile` (Taxonomy 7 → 6)

Status

Accepted. Corrects ADR-0010, which fixed the diagnostic taxonomy at seven classes including a separate DanglingReference. This ADR retires DanglingReference, folding reference-resolution failures into TypstCompile, so the taxonomy is now six classes. ADR-0010 stays the record of the original decision; this one records the correction.

Context

ADR-0010 named two distinct external-facility diagnostics for reference problems:

DanglingReference — "a relative import outside the import boundary, or an unresolved cross-reference."
TypstCompile — "the assembled typst source fails to compile (syntax error, unresolved @ref, etc.)."

The unresolved cross-reference (@ref) was listed under both — a genuine contradiction in the contract. And on inspection, the other DanglingReference case (an out-of-boundary relative import) is also a typst compile-time error: typst resolves import/include paths at runtime (ADR-0011's Correction), so a path escaping the import boundary fails as "cannot access file system from here" — a TypstCompile diagnostic. Both of DanglingReference's cases are therefore detected by, and surface as, the typst compiler's own output.

The implementation reflected this from the start: cph-typst maps every typst SourceDiagnostic to DiagCode::TypstCompile (crates/cph-typst/src/diag.rs), and no code path ever emits DanglingReference. The Lean Oracle likewise had a refsResolve field separate from compiles, but compiles t already entails that target t's references resolve (the source would not compile otherwise) — so refsResolve was redundant in the Legal conjunction.

DanglingReference was thus a contract class with no distinct verdict, no distinct emitter, and a definition overlapping TypstCompile. It diluted the taxonomy rather than carving a real boundary.

Decision

`TypstCompile` owns reference resolution

TypstCompile is the single external-facility diagnostic for the assembled typst source failing to compile — including an unresolved cross-reference (@ref) and a relative import/include that escapes the import boundary or names a missing file. There is no separate reference-resolution diagnostic.

`DanglingReference` is retired; the taxonomy is six classes

The diagnostic taxonomy is now:

Code	Meaning	Severity	Kind
`PartPathMissing`	A manifest `[[parts]]` entry points at a non-existent folder (or escapes the root via `..`).	error	structural
`UnknownKind`	A part declares a kind not in the known set (or a part/`element.toml` kind mismatch).	error	structural
`MissingContentFile`	A `content` field required by the kind schema has no `<field>.typ`.	error	structural/schema
`SchemaViolation`	Instance data violates its kind's JSON Schema; also the malformed-`manifest`/`element.toml` fallback.	error	schema / external
`TypstCompile`	The assembled typst source fails to compile — syntax error, unresolved `@ref`, out-of-boundary or missing `import`/`include`.	error	external
`RenderIgnored`	A used kind a target does not cover; the element is omitted from that export.	warning	semantic

RenderIgnored alone is a warning; the other five are error. The structural / external / semantic boundary from ADR-0010 is unchanged.

`Oracle.refsResolve` is removed

The Legal-predicate oracle drops its refsResolve field. Reference resolution is subsumed by compiles (per target): compiles t already requires t's assembled source to compile, which requires its references to resolve. Legal becomes dataConforms ∧ contentFilesPresent ∧ (∀ declared t, compiles t).

Consequences

The contract no longer contradicts itself on where an unresolved @ref is reported: it is a TypstCompile diagnostic, full stop.
The implementation needs no behavioral change — it already routed all reference failures to TypstCompile and never emitted DanglingReference. The correction removes the unused DiagCode::DanglingReference variant, closing the spec↔impl gap (a named-but-unemitted code) rather than leaving it as a permanent MVP-deferred stub.
The Oracle / Legal definitions in the Lean master shrink by one redundant conjunct, with no change to which lessons are legal.

Open Questions / Deferred

Finer reference diagnostics. Should a future checker want to distinguish an out-of-boundary import from a missing file from an unresolved @ref — with reference-specific fix hints better than typst's generic message — that is a new diagnostic class, introduced deliberately when the need is real (ADR-0010's "taxonomy is open to growth" still holds). This ADR removes the redundant class; it does not forbid a genuinely distinct one later.

4.9 KiB Raw Permalink Blame History

ADR 0012: Reference Resolution Folds Into TypstCompile (Taxonomy 7 → 6)