From 81cf762a0ca0b6f62f6440116de222b0c2ceb6c1 Mon Sep 17 00:00:00 2001 From: sjfhsjfh Date: Mon, 22 Jun 2026 08:33:11 +0800 Subject: [PATCH] docs(adr): add ADR-0009 (export target = build) + ADR-0010 (diagnostics/legality/pipeline) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Lift business decisions made during the MVP build into the contract, per constitution rule 5 (divergence points belong in the spec). ADR-0009 — amends ADR-0005's render-matrix framing: an export target is a *build* producing a typed Artifact (SingleFile | FileTree). build = map (per-kind, the field-visibility lives here) + reduce (assemble, determined by artifact type: SingleFile concatenates in lesson order then compiles — which is why @ref and counters work). Build form = declarative schema + a run-shell hatch (where ADR-0005's medium-only category (b) and npm/HTML builds live), not a Makefile. typst compile is hidden backend mechanism, not part of a target. Defaults seeded at project creation, overridable in the file — the heading-numbering bug (一、 reused → 二、一、) is the worked example of that missing override layer. ADR-0010 — backfills ADR-0005's deferred "legal lesson": the 7-class diagnostic taxonomy with per-class meaning + severity; legal lesson = no error-level diagnostic; the 5-phase pipeline (load→structural→schema→compile→coverage) with compile gated on zero prior errors. External-facility diagnostics (TypstCompile, DanglingReference, schema conformance) modeled as abstract predicates whose verdict comes from an implementation oracle, not from Lean — keeps the contract honest about what it does and doesn't decide. Co-Authored-By: Claude Opus 4.8 (1M context) --- docs/adr/0009-export-target-is-a-build.md | 149 ++++++++++++++++++ ...nostics-legal-lesson-and-check-pipeline.md | 131 +++++++++++++++ 2 files changed, 280 insertions(+) create mode 100644 docs/adr/0009-export-target-is-a-build.md create mode 100644 docs/adr/0010-diagnostics-legal-lesson-and-check-pipeline.md diff --git a/docs/adr/0009-export-target-is-a-build.md b/docs/adr/0009-export-target-is-a-build.md new file mode 100644 index 0000000..f0c718f --- /dev/null +++ b/docs/adr/0009-export-target-is-a-build.md @@ -0,0 +1,149 @@ +# ADR 0009: An Export Target Is A Build Producing A Typed Artifact + +## Status + +Accepted — for the decisions below. **Amends ADR-0005**: where ADR-0005 framed +rendering as a passive `(kind × target)` configuration matrix looked up per +element, this ADR reframes an export target as an active **build** that consumes +the lesson and produces a typed **artifact**. The seed rule ADR-0005 fixed +(missing render rule for a used kind ⇒ warning) survives, restated against the +new structure. Several sub-decisions are deferred; see *Open Questions*. + +## Context + +ADR-0005 said an export target "projects/renders the lesson", with a render +matrix that "lives in the engineering file; the framework provides defaults, the +file may override." The MVP implementation did not realize that override path: +it hardcoded one target's behavior as a `target == "student"` branch inside the +render package and baked presentation defaults (heading numbering) into the +package with no way for an engineering file to change them. That produced a +concrete bug — a single-symbol numbering pattern (`一、`) reused across heading +levels, so level-2 headings rendered as `二、一、…` — which is not a typo but the +**symptom of a missing layer**: targets were behavior welded into code, not +configuration a lesson can carry and override. + +Looking at the prototype confirms the real shape of the problem. It had two +near-identical export entrypoints (`exports/学生版.typ`, `exports/教师版.typ`) +plus a `display-control.typ` switching on `sys.inputs("x-export-target")` with a +scatter of per-concern booleans (`show-answer`, `show-discussion-script`, +`show-eg-comment`, …). The two scripts are ~95% identical; the duplication — +load, assemble, compile, page setup — is the same across every target, and only +a thin policy delta differs. **That repetition is the thing to factor out.** + +A target is therefore best understood as **a build script with the repeated +mechanism abstracted away** — closer in spirit to a GitHub Actions workflow +(declarative steps, plus a `run`-shell escape hatch) than to a Makefile. + +## Decision + +### A target is a build that produces a typed artifact + +An export target is **a build**: it consumes the (ordered, typed) lesson and +produces one **artifact**. The artifact's *shape* is part of what the target +*is*, modeled as an ADT value the target carries: + +- `SingleFile` — one bundled document (a 讲义 PDF, a teacher plan PDF). +- `FileTree` — many files plus an index/manifest (a third-party platform + archive). + +"Single file vs. many files" is a genuine divergence point — it changes what +`cph build` emits and what a consumer expects — so the artifact type is part of +the contract, not an implementation afterthought. (Backend/format beyond this — +which concrete PDF engine, which markdown dialect — stays open.) + +### A build is map + reduce; the reduce is determined by the artifact + +A build has two phases, kept distinct: + +- **map (per-kind).** For each element kind, how that kind becomes an + intermediate fragment. This is declarative and keyed by kind — the part a + GitHub-Actions-style schema expresses naturally. **Field visibility lives + here**: "student hides `example.solution` and `lemma.proof`; teacher shows + them" is simply *what this target's per-kind map does* — not a separate + concept and not a property of the element. +- **reduce / assemble.** The ordered fragments are folded into the artifact. + This fold is **determined by the artifact type**, not written per target: + - `SingleFile` ⇒ concatenate fragments in lesson order into one document, then + compile it. (This is *why* cross-references `@label`/`@ref` and the + 例题1/例题2 counters work at all: they resolve only when the whole lesson is + one compiled document. The fold's statefulness is carried by the backend's + own counters at assemble-compile time, not re-implemented in the map.) + - `FileTree` ⇒ each part to its own file, plus a generated index. + +The framework provides the assembler for each artifact shape; a build only +*chooses* its artifact type. This is the answer to "a per-kind rule can't express +aggregation": aggregation isn't crammed into the per-kind schema — the artifact +value picks a framework assembler, and the **shell escape hatch** is reserved for +the genuinely irregular case (a third-party archive that runs an npm build). + +### The build form: declarative schema plus a `run`-shell hatch + +A build is expressed declaratively (a schema — concretely a YAML-ish document, +consistent with the `manifest.toml`/`element.toml` lineage) with one **`run` +escape hatch** for steps that resist declaration. Explicitly **not** a Makefile +or a general scripting language: the declarative surface carries the common +cases (per-kind map, artifact choice, presentation knobs), and the shell hatch is +the bounded exception. This mirrors ADR-0006's stance on schemas: fix the *form* +here, keep the concrete payload an implementation detail. + +### typst compilation is a hidden backend mechanism, not part of a target + +Compiling typst to PDF is the *shared, repeated* mechanism every PDF-producing +target needs. It is therefore **backend mechanism, hidden below the target**, not +something a target re-specifies. A target says "I produce a `SingleFile` PDF"; +*how* the assembled document becomes bytes is the framework's business. (This is +also where the checker's typst-compile diagnostic belongs — an external facility, +see ADR-0010.) + +### Medium-only information rides the build's shell hatch + +ADR-0005's category **(b)** — medium-only information that exists only because of +a target's medium (HTML interactive behavior, a build script, npm dependencies) +— finally has a home: it belongs to the **target's build** (its shell hatch / +artifact assembler), never to the element. This complements ADR-0005's +category-(a) decision (semantic-but-target-specific fields ride the element); (b) +rides the build. + +### Defaults are seeded at project creation and overridable in the file + +The framework ships **default builds** for its stock targets (e.g. student, +teacher), written into the engineering file when a project is created. The file +may then **override** pieces of them. The numbering bug is the worked example: +the fix is not patching the render package but **overriding the student/teacher +build's numbering** in the engineering file (e.g. +`numbly("{1:一}、", "{1:1}.{2:1}")` — level-1 `一、`, level-2 `1.1`). This realizes +ADR-0005's "matrix lives in the file, framework gives defaults, file overrides" +as an actual editable layer rather than a slogan. + +## Consequences + +- The two duplicated export scripts collapse into one shared build mechanism plus + two small target *configurations* (artifact type + per-kind map + presentation + overrides). Adding a target is adding a config value, not copying a script. +- `cph build --target T` is defined by T's artifact type: it writes one file for + `SingleFile`, a directory for `FileTree`. +- Presentation defaults (numbering, labels, styling) are file-resident and + overridable; a wrong default is a one-line edit in the engineering file, not a + package change. +- The contract gains structure (an `Artifact` ADT; a target = build with a + per-kind map + an artifact-determined assemble) without committing the concrete + build-schema fields — those stay implementation, per the depth ceiling + (constitution rule 5). +- ADR-0005's render-matrix language is superseded by this build framing; its + warning rule (missing render for a used kind ⇒ warning, non-blocking) is + preserved and restated in ADR-0010 against the new `covers`. + +## Open Questions / Deferred + +- **Concrete build-schema fields** — the exact declarative keys (per-kind map + syntax, where the shell `run` step sits, how an override is written) are an + implementation-level schema, fixed later, not in Lean. +- **Backend / format enumeration** — beyond `SingleFile`/`FileTree`: which PDF + engine, and the markdown-dialect / React-template export ADR-0005 mentioned for + third-party platforms. Open. +- **`FileTree` and the shell hatch implementation** — specified here but not + implemented in this round (no third-party target instance yet); the MVP + implements `SingleFile`/PDF only and marks the rest deferred. +- **Override granularity** — exactly which pieces of a build a file may override + (numbering only? arbitrary presentation? the per-kind map itself?) is fixed as + needed; this ADR commits only that an override layer exists and is file-resident. diff --git a/docs/adr/0010-diagnostics-legal-lesson-and-check-pipeline.md b/docs/adr/0010-diagnostics-legal-lesson-and-check-pipeline.md new file mode 100644 index 0000000..7b601e4 --- /dev/null +++ b/docs/adr/0010-diagnostics-legal-lesson-and-check-pipeline.md @@ -0,0 +1,131 @@ +# 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 `.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).