curriculum-project-hub/docs/adr/0009-export-target-is-a-build.md

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.