From 9b37914bfb26cf8a1dc417cecb6281d3e8f3d079 Mon Sep 17 00:00:00 2001 From: sjfhsjfh Date: Mon, 22 Jun 2026 09:44:32 +0800 Subject: [PATCH] docs(adr): add ADR-0011 (export builds = typed steps over templates), correct ADR-0008 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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/.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) --- ...008-engineering-file-layout-conventions.md | 13 +- ...t-builds-are-typed-steps-over-templates.md | 142 ++++++++++++++++++ 2 files changed, 151 insertions(+), 4 deletions(-) create mode 100644 docs/adr/0011-export-builds-are-typed-steps-over-templates.md diff --git a/docs/adr/0008-engineering-file-layout-conventions.md b/docs/adr/0008-engineering-file-layout-conventions.md index 25bd3d9..34c67c1 100644 --- a/docs/adr/0008-engineering-file-layout-conventions.md +++ b/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 - *generated artifact* the renderer produces from the manifest per target; it is - never the canonical lesson and is not hand-edited. +- A per-target **export template** (a real, editable `.typ` file, e.g. + `exports/student.typ`) reads the manifest and renders the lesson; it is the + 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). diff --git a/docs/adr/0011-export-builds-are-typed-steps-over-templates.md b/docs/adr/0011-export-builds-are-typed-steps-over-templates.md new file mode 100644 index 0000000..e58a765 --- /dev/null +++ b/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=` (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.