forked from EduCraft/curriculum-project-hub
81cf762a0c
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) <noreply@anthropic.com>
150 lines
8.4 KiB
Markdown
150 lines
8.4 KiB
Markdown
# 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.
|