forked from bai/curriculum-project-hub
sjfhsjfh
5dc29fe558
一节课可多人署名(教研组),故 canonical author 是**有序列表**而非单值。on-disk 形式接受裸字符串(单作者)或数组(多作者),但此"字符串或数组"二态**只活在加载边界**: RawInfo 经归一化折叠成 canonical Info,其后系统只见 List。 Lean 母本(ADR-0008 范围):新增 Model/Info.lean,把 Info(canonical,authors: List String)与 RawInfo/RawAuthor(授权便利 surface)+ 归一化 RawInfo.toInfo 钉死—— canonical 接收端恒为列表,raw 形式不泄漏。ADR-0008 [info] 块补 author-as-list 决策。 impl 对齐:cph-model Info.author: Option<String> → authors: Vec<String>;RawAuthor untagged enum(One|Many)+ into_vec 归一化;augmented manifest 发射 author 数组 (typst document(author:) 与模板已接受 string/array)。doc 两端互引 spec。 测试:load.rs 单作者→单元素列表;target-configs fixture 加数组作者断言多作者。 验证:lake build 绿(25 jobs);cargo test 全绿;clippy 静默;TH-141(单字符串作者) check+build PDF 无回归。 Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
146 lines
7.6 KiB
Markdown
146 lines
7.6 KiB
Markdown
# ADR 0008: Engineering-File Layout — Declarative Manifest + Element Descriptors
|
||
|
||
## Status
|
||
|
||
Accepted — for the layout conventions below. Some sub-decisions are deferred;
|
||
see *Open Questions / Deferred*.
|
||
|
||
Discharges the layout question ADR-0007 left open. ADR-0007 fixed that the
|
||
engineering file is a real directory tree but explicitly deferred the concrete
|
||
layout: the manifest (name, location, contents), how element instances are
|
||
arranged and how their **order** (ADR-0005's `Lesson` is an ordered sequence) is
|
||
encoded, and how rich-content `.typ` files are named. This ADR fixes those.
|
||
|
||
## Context
|
||
|
||
Two real sample engineering files exist (TH-141, TH-144). They encode the lesson
|
||
as a typst file `main.typ` containing `#import`s of each element's `main.typ`
|
||
plus a `#let parts = (("segment", 模块), ("lemma", 模块), …)` ordered tuple list.
|
||
Each element is a folder under a per-kind directory (`segments/`, `examples/`,
|
||
`lemmas/`, `sop/`); its fields are typst source files (`textbook.typ`,
|
||
`problem.typ`/`solution.typ`, `stmt.typ`/`proof.typ`, `sop.typ`) wired up by the
|
||
element's own `main.typ` via `#let f = include "f.typ"`.
|
||
|
||
That embryo has one property in tension with the contract: **the ordering
|
||
manifest is itself a typst script**. ADR-0005 rejected typst as the
|
||
definition/scripting language (its typing is too weak), and ADR-0006 moved the
|
||
kind schema off typst onto declarative JSON Schema. A checker that had to *parse
|
||
typst* to recover the lesson's element order would re-introduce exactly the
|
||
dependency those ADRs removed: the order — a first-class part of the `Lesson`
|
||
contract — would be locked inside an evaluated typst program.
|
||
|
||
## Decision
|
||
|
||
### The lesson manifest is declarative, not a typst script
|
||
|
||
The lesson's order and membership live in a **declarative `manifest.toml`** at
|
||
the engineering-file root, read directly by the checker. TOML is chosen for
|
||
consistency with the samples' existing `project.toml` / `info.toml` /
|
||
`meta.toml`. It subsumes `project.toml` and `info.toml`. Shape:
|
||
|
||
```toml
|
||
[project]
|
||
id = "…" # stable project id
|
||
name = "…" # folder/display name
|
||
|
||
[info] # passed through to render targets verbatim
|
||
title = "…"
|
||
author = "…" # one author; or a list: author = ["…", "…"]
|
||
|
||
[[parts]] # ORDER OF THIS ARRAY IS THE LESSON ORDER (ADR-0005)
|
||
kind = "segment" # one of the known kinds (ADR-0006 / stdlib set)
|
||
path = "segments/开场对照导言" # element folder, relative to root
|
||
# … one [[parts]] block per element, in order …
|
||
|
||
[targets.student] # which export targets exist for this lesson
|
||
[targets.teacher]
|
||
```
|
||
|
||
The checker reads `parts` for order and membership. It **must not** parse typst
|
||
to recover ordering — the declarative array is the single source of truth. The
|
||
sample's `main.typ` `#let parts` is **replaced** by this; any typst entrypoint
|
||
that imports elements in order is a *generated build artifact* derived from the
|
||
manifest (see ADR-0007's note that the on-disk encoding of `Lesson` is separate
|
||
from "it's a tree"), never the canonical order.
|
||
|
||
### `[info].author` is a list; the on-disk single-string form is sugar
|
||
|
||
A lesson can be authored by several people (a teaching group), so the canonical
|
||
`author` is an **ordered list**, not a single value. For authoring convenience the
|
||
on-disk form accepts **either** a bare string (`author = "…"`, one author) **or** an
|
||
array (`author = ["…", "…"]`). That "string-or-array" union lives **only at the load
|
||
boundary**: the loader normalizes a bare string to a one-element list, and
|
||
everything downstream sees a list. Absent `author` ⇒ empty list. This raw-vs-
|
||
canonical split is pinned in the Lean master as `RawInfo` (the authoring surface)
|
||
vs `Info` (the canonical model whose `authors` is always a list) — see
|
||
`spec/Spec/Courseware/Model/Info.lean`.
|
||
|
||
### An element folder is self-describing via `element.toml`
|
||
|
||
Each element folder carries an **`element.toml`** declaring its kind and its
|
||
**scalar** fields (per the kind's JSON Schema, ADR-0006):
|
||
|
||
```toml
|
||
kind = "example"
|
||
source = "41 届物理竞赛复赛第三大题(1)" # a scalar field of the example kind
|
||
```
|
||
|
||
`kind` is explicit in the descriptor (not inferred from the parent directory
|
||
name) so a folder is self-describing and the `segments/`-vs-`lemmas/` directory
|
||
grouping is a human convenience, not load-bearing for the checker.
|
||
|
||
### `content` fields are convention-named `.typ` siblings
|
||
|
||
A kind's schema (ADR-0006) marks some fields as the `content` extension type.
|
||
For each such field `F`, its value is the typst source file **`F.typ`** in the
|
||
element folder. The schema — not `element.toml`, not a per-element `main.typ` —
|
||
is the source of truth for *which* `.typ` files must exist. Concretely for the
|
||
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 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
|
||
(ADR-0007), so its spans resolve and its relative imports anchor within the tree
|
||
(ADR-0006 import boundary).
|
||
|
||
## Consequences
|
||
|
||
- 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 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).
|
||
- `path` being a real relative folder makes "the lesson references element X"
|
||
inspectable on disk; a dangling `path` is a structural error the checker can
|
||
point at.
|
||
|
||
## Open Questions / Deferred
|
||
|
||
- **Per-file render override.** ADR-0005 says the (kind × target) render matrix
|
||
lives *in* the engineering file with framework **defaults** the file may
|
||
**override**. This ADR's `[targets.*]` only *declares which targets exist*; the
|
||
MVP keeps the render rules entirely in the framework render layer with **no
|
||
per-file override**. Whether/how a lesson overrides a render rule (a block in
|
||
`manifest.toml`? a per-target file?) is deferred until a real override need
|
||
appears. This is a known, surfaced gap against ADR-0005, not an oversight.
|
||
- **Question bank (题库) on disk.** TH-144 has a `题目/` tree of problem/answer
|
||
pairs outside `parts`. Its layout and its element relationship (ADR-0005
|
||
Deferred: reference vs inline) stay open; out of MVP scope.
|
||
- **Manifest richness.** Per-part metadata, grouping/sectioning (TH-144's A/B/C
|
||
structure is only in folder names today), and target-specific options on a part
|
||
are not modeled here; add when needed rather than guessing now.
|
||
- **stdlib kind set & schema dialect** remain as ADR-0006 left them; this ADR
|
||
only fixes the on-disk *arrangement*, not the schemas themselves.
|