docs(adr): add ADR-0011 (export builds = typed steps over templates), correct ADR-0008

Refines ADR-0009 by fixing the shape of an artifact and a build; corrects a
false premise that propagated into the implementation.

ADR-0011:
- Artifact is an ADT WITH fields: SingleFile{filepath} / FileTree{root,
  outputs:glob} — the product semantics (one file where, vs a tree of what) are
  pinned, not erased behind a bare tag.
- A target = artifact + ordered typed steps: typstCompile{template} (typed
  because the framework wires the manifest in — not a raw shell line) | shell{run}
  (the hatch where ADR-0005 category-b medium-only builds land).
- Presentation (numbly numbering, styling) lives in the template file
  (exports/<target>.typ), NOT the manifest; manifest [targets.*.numbering] removed.
- Correction (verified against typst source: typst-eval/src/import.rs:22,174;
  tests/suite/scripting/include.typ): include/import paths MAY be runtime-computed
  (only a bare `import expr` without `as` is restricted). So the framework does
  NOT generate a static-include driver — a template toml()-reads the manifest and
  includes each part via a computed path. Removes a whole generated layer.
- RenderRule-as-payload retired; coverage downgraded to a declaration (which
  kinds a target renders) feeding the unchanged renderIgnored warning.

ADR-0008: corrected the two clauses (the "generated driver / static #import"
wording) that were residue of the false premise, pointing them at the
template-injection model and citing ADR-0011.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

docs/adr/0008-engineering-file-layout-conventions.md

@@ -87,7 +87,9 @@ MVP kind set: `segment` ⇒ `textbook.typ`; `example` ⇒ `problem.typ`,
 `solution.typ`; `lemma` ⇒ `stmt.typ`, `proof.typ`; `sop` ⇒ `sop.typ`. This
 **drops the samples' per-element `main.typ`** (`#let textbook = include …`):
 that field-to-file wiring is now implied by the schema + naming convention and
-materialized by the generated driver, not hand-authored.
+materialized at build time by the export template, not hand-authored. (Originally
+this said "the generated driver"; ADR-0011 supersedes that — there is no generated
+driver, an export template reads the manifest and includes each part's content.)
 
 A `content` field's denotation remains ADR-0006's: the **module body content**
 of `F.typ`, not its `#let` exports. The file sits at a real relative path
@@ -99,9 +101,12 @@ of `F.typ`, not its `#let` exports. The file sits at a real relative path
 - The checker recovers the full ordered lesson from `manifest.toml` + each
   `element.toml` without evaluating any typst — order and membership are plain
   data, diffable and greppable.
-- A typst driver entrypoint (static `#import`s + the render call) becomes a
+- A per-target **export template** (a real, editable `.typ` file, e.g.
-  *generated artifact* the renderer produces from the manifest per target; it is
+  `exports/student.typ`) reads the manifest and renders the lesson; it is the
-  never the canonical lesson and is not hand-edited.
+  build entrypoint, not the canonical lesson. (This clause originally described a
+  *generated* driver with static `#import`s, on a since-corrected belief that
+  typst forbids runtime-computed include paths — see ADR-0011's *Correction*.
+  Include/import paths may be computed, so no driver is generated.)
 - Element folders lose their per-element `main.typ`; `element.toml` + the schema's
   content-file convention replace it. Migrating the samples is a mechanical
   rewrite (the migration is part of the MVP).

docs/adr/0011-export-builds-are-typed-steps-over-templates.md

@@ -0,0 +1,142 @@
+# ADR 0011: Export Builds Are Ordered Typed Steps Over Template Files
+
+## Status
+
+Accepted. **Refines ADR-0009** (which established target = a build producing a
+typed artifact) by fixing the *shape* of a build and of an artifact. **Corrects
+ADR-0008** on one point of fact (see *Correction* below). Some items deferred;
+see *Open Questions*.
+
+## Context
+
+ADR-0009 said an export target is a build producing a typed `Artifact`, with a
+map+reduce structure and a "declarative schema + shell hatch" form. The first
+implementation of that idea (and its initial Lean encoding) got three things at
+the wrong level of abstraction, surfaced in review:
+
+1. **The `Artifact` type was a bare enum** (`singleFile | fileTree`) with no
+   fields. But "what the product *is*" — a single file at some path, vs. a tree
+   of files under some root — is exactly the non-obvious semantics that must be
+   pinned. A bare enum erases it.
+2. **A target was modeled as a loose config bag** (an artifact plus a per-kind
+   render map) with presentation knobs (heading numbering) stuffed into
+   `manifest.toml`. But a build is naturally **an ordered list of steps**, each a
+   typed operation; and presentation belongs in a **template file**, not the
+   manifest.
+3. **A false premise about typst drove the design.** The build was going to have
+   the framework *generate* a typst entrypoint with **static** `#include`s of
+   every element, on the stated belief that "typst forbids a runtime-computed
+   include/import path." That belief is **wrong** (verified below). It is the
+   reason ADR-0008 mentions "the generated driver" and "static `#import`s" — that
+   wording is a residue of the false premise and is corrected here.
+
+## Correction: include/import paths may be runtime-computed
+
+Verified against the typst source (`/Users/sjfhsjfh/Typst/typst`, 0.15):
+
+- `#include` and `#import` parse an **arbitrary code expression**, not a string
+  literal (`typst-syntax` parser uses `code_expr` for both).
+- The source operand is **evaluated at runtime**
+  (`typst-eval/src/import.rs:22` for import, `:174` for include); a
+  `Value::Str` is then resolved to a module via runtime path resolution
+  (`span.resolve_path(...)`). Path resolution is a **runtime** operation, so a
+  missing file is a runtime error, not a parse error.
+- The test suite confirms it: `tests/suite/scripting/include.typ` contains
+  `#let chap2 = include "modu" + "les/chap" + "2.typ"` — a computed path.
+- The **only** restriction: a *bare* `import expr` (no `as name`) rejects a
+  dynamic string source ("dynamic import requires an explicit name");
+  `import expr as name` and `include expr` both accept dynamic paths.
+
+**Consequence:** the framework does **not** need to generate a static-include
+driver. A template can `toml()`-read the manifest and `include` each part's
+content via a **computed** path. This removes an entire generated-artifact layer.
+
+## Decision
+
+### `Artifact` is an ADT with fields
+
+```
+SingleFile { filepath }            -- the product is one file, written at filepath
+FileTree   { root, outputs:glob }  -- the product is the files under root matching outputs
+```
+
+`SingleFile.filepath` says where the one product lands (a 讲义/教案 PDF).
+`FileTree.root` is the output directory; `FileTree.outputs` is a **glob**
+describing which files this build produces (e.g. `**/*.{html,js,json}`) — lighter
+than an explicit manifest of outputs, while still letting a consumer/checker know
+what to expect and verify. These fields are the semantics; they go in the Lean
+ADT with doc, not erased behind a bare tag.
+
+### A target is an artifact plus ordered, typed steps
+
+A target's build is `{ artifact, steps }`, where `steps` is an **ordered** list
+and each `Step` is a **typed operation** (extensible):
+
+- `typstCompile { template }` — compile a **template file** (e.g.
+  `exports/student.typ`) to the artifact. It is *typed*, not a raw shell line,
+  precisely because the framework must **wire the manifest into it** — a bare
+  `typst compile` shell string cannot express that injection.
+- `shell { run }` — an escape hatch for steps that resist declaration (this is
+  where ADR-0005's medium-only category (b): HTML interactive builds, npm, lands).
+
+MVP has exactly one step per target (a single `typstCompile`), but the structure
+is a list because a `FileTree`/third-party build will need several.
+
+### Presentation lives in the template file, not the manifest
+
+The `typstCompile.template` (e.g. `exports/student.typ`) is a **real, editable
+file** in the engineering file. Presentation — heading numbering (numbly), styling
+— lives **there**, not in `manifest.toml`. The manifest's earlier
+`[targets.*.numbering]` block is **removed**. (Framework defaults for these
+templates are written into the engineering file at project-creation time; the
+creation flow is out of this round's scope — the sample's templates are authored
+by hand and noted as "should be seeded".)
+
+### The manifest is injected, not statically inlined
+
+A `typstCompile` step compiles its template **as the main file**, passing the
+manifest in via `--input manifest=<path>` (a path relative to the typst `--root`,
+which is the engineering-file root). The template does
+`toml(sys.inputs.manifest)` to read metadata (course title, author) and the
+ordered `parts`, and `include`s each part's content via the part's path (a
+**computed** path — legal per the *Correction*). No framework-generated driver.
+
+### Render coverage is a declaration, not a payload
+
+ADR-0009's per-target render *payload* (`RenderRule`) is **retired**: the "how" of
+rendering now lives in the template/steps, not in a contract-level rule object.
+What the contract keeps is a **coverage declaration** — *which kinds a target
+renders* — used only by the seed diagnostic. ADR-0005's rule survives unchanged:
+a used kind a target does **not** cover ⇒ a `renderIgnored` **warning** (non-
+blocking). `Primitives.RenderRule` is removed from the model.
+
+## Consequences
+
+- The product type is self-describing: `SingleFile`'s path and `FileTree`'s
+  root+glob are in the contract; `cph build` and any consumer know exactly what a
+  target emits and where.
+- A build is a list of typed steps — adding a non-typst step (npm, packaging) is
+  adding a `shell` step, not bending the typst path.
+- Presentation is editable in one obvious place (the template file); the manifest
+  carries structure (parts, targets, artifacts, steps), not styling.
+- Removing the generated-driver layer simplifies the engine: it compiles a real
+  template file as main (spans resolve to a real authored file, not a synthetic
+  one) and sets one `sys.inputs` value.
+- ADR-0008's "generated driver / static `#import`s" wording is superseded by the
+  template-injection model here.
+
+## Open Questions / Deferred
+
+- **`FileTree` and `shell` step implementation** — specified here, not built this
+  round (no third-party target instance yet). MVP implements `SingleFile` + a
+  single `typstCompile` step; the rest is deferred with explicit diagnostics.
+- **Project-creation seeding** — that default templates are written into a new
+  engineering file at creation time is asserted but not implemented here; the
+  sample's templates are hand-authored.
+- **Template ↔ framework calling convention** — how exactly the template pulls
+  part content (a `cph-render` helper that takes a loader closure, vs. the
+  template doing its own `for`+`include`) is an implementation detail settled in
+  the render package, not pinned in Lean.
+- **Multiple steps / step dependencies** — ordering is fixed as a list; whether
+  steps ever need richer dependency structure is deferred until a multi-step
+  target exists.