diff --git a/crates/cph-model/src/lib.rs b/crates/cph-model/src/lib.rs index 893c7e1..7b89748 100644 --- a/crates/cph-model/src/lib.rs +++ b/crates/cph-model/src/lib.rs @@ -211,12 +211,23 @@ pub struct Project { } /// `[info]` table (passed through to render targets verbatim). +/// +/// **Mirrors `Spec.Courseware.Info`** in the Lean semantic master +/// (`spec/Spec/Courseware/Model/Info.lean`): the *canonical* model whose +/// `authors` is always a list. The authoring-surface form (string-or-array +/// `author`) is the separate [`RawInfo`] / [`RawAuthor`], normalized into this +/// at the load boundary — mirroring the Lean `RawInfo` / `RawAuthor` split. No +/// CI gate enforces this alignment (repo constitution); it is kept greppable. #[derive(Debug, Clone, PartialEq, Eq, Serialize)] pub struct Info { /// Lesson title. pub title: String, - /// Author, optional. - pub author: Option, + /// Authors, in declared order. A lesson can have several (a teaching group), + /// so this is a list, not a single name. Empty when `[info]` declares no + /// `author`. The on-disk `author` accepts either a bare string (one author) + /// or an array of strings (see [`RawAuthor`]); both load into this `Vec`. + /// Mirrors Lean `Info.authors : List String`. + pub authors: Vec, } /// One `[[parts]]` entry plus its loaded element descriptor. @@ -265,10 +276,36 @@ struct RawProject { name: String, } +/// The authoring-surface `[info]` (mirrors Lean `RawInfo` in +/// `spec/Spec/Courseware/Model/Info.lean`): the raw form that exists for +/// fill-in convenience, normalized into the canonical [`Info`] at the load +/// boundary. Not the form the rest of the model traffics in. #[derive(Debug, Deserialize)] struct RawInfo { title: String, - author: Option, + author: Option, +} + +/// On-disk `author`: either a single name (`author = "…"`) or a list +/// (`author = ["…", "…"]`). Mirrors Lean `RawAuthor`: a fill-in convenience whose +/// string-or-array union lives **only** at the load boundary — [`RawAuthor::into_vec`] +/// folds it into the canonical [`Info::authors`] `Vec`, after which it never appears. +#[derive(Debug, Deserialize)] +#[serde(untagged)] +enum RawAuthor { + One(String), + Many(Vec), +} + +impl RawAuthor { + /// Flatten to the ordered author list (Lean `RawAuthor.normalize`): a single + /// name becomes a one-element list; a list passes through verbatim. + fn into_vec(self) -> Vec { + match self { + RawAuthor::One(s) => vec![s], + RawAuthor::Many(v) => v, + } + } } #[derive(Debug, Deserialize)] @@ -361,7 +398,7 @@ pub fn load(root: &Path) -> (Option, Vec) { let info = match raw.info { Some(i) => Info { title: i.title, - author: i.author, + authors: i.author.map(RawAuthor::into_vec).unwrap_or_default(), }, None => { diags.push( diff --git a/crates/cph-model/tests/fixtures/target-configs/manifest.toml b/crates/cph-model/tests/fixtures/target-configs/manifest.toml index 48d0125..ba3bb29 100644 --- a/crates/cph-model/tests/fixtures/target-configs/manifest.toml +++ b/crates/cph-model/tests/fixtures/target-configs/manifest.toml @@ -4,6 +4,8 @@ name = "target-configs" [info] title = "测试课：导出目标的结构化 build 配置" +# Array form: a lesson authored by several people. +author = ["张老师", "李老师"] # Full v2 config: explicit single-file artifact + an ordered typst-compile step. [targets.student] diff --git a/crates/cph-model/tests/load.rs b/crates/cph-model/tests/load.rs index d26b8f2..9d2414f 100644 --- a/crates/cph-model/tests/load.rs +++ b/crates/cph-model/tests/load.rs @@ -27,7 +27,8 @@ fn valid_two_part_lesson_loads_in_order_with_no_errors() { assert_eq!(lesson.project.id, "fixture-valid"); assert_eq!(lesson.project.name, "valid-2-part"); assert_eq!(lesson.info.title, "测试课：两个部件"); - assert_eq!(lesson.info.author.as_deref(), Some("范式教育教研组")); + // A single-string `author` loads as a one-element list. + assert_eq!(lesson.info.authors, vec!["范式教育教研组".to_string()]); // Parts preserve declared order: segment first, lemma second. assert_eq!(lesson.parts.len(), 2); @@ -149,6 +150,12 @@ fn structured_target_configs_parse_into_typed_builds() { "well-formed target configs must have no diagnostics, got: {diags:?}" ); + // An array `author` loads as the ordered author list. + assert_eq!( + lesson.info.authors, + vec!["张老师".to_string(), "李老师".to_string()] + ); + // Declared order is preserved. assert_eq!(lesson.target_names(), vec!["student", "archive", "teacher"]); diff --git a/crates/cph-typst/src/manifest.rs b/crates/cph-typst/src/manifest.rs index f8d0671..cdd4e58 100644 --- a/crates/cph-typst/src/manifest.rs +++ b/crates/cph-typst/src/manifest.rs @@ -42,8 +42,15 @@ pub fn build_augmented_manifest(lesson: &Lesson) -> String { "title".to_string(), toml::Value::String(lesson.info.title.clone()), ); - if let Some(author) = &lesson.info.author { - info.insert("author".to_string(), toml::Value::String(author.clone())); + if !lesson.info.authors.is_empty() { + let authors = lesson + .info + .authors + .iter() + .cloned() + .map(toml::Value::String) + .collect(); + info.insert("author".to_string(), toml::Value::Array(authors)); } doc.insert("info".to_string(), toml::Value::Table(info)); diff --git a/crates/cph-typst/tests/compile.rs b/crates/cph-typst/tests/compile.rs index b4f2e2a..889efdd 100644 --- a/crates/cph-typst/tests/compile.rs +++ b/crates/cph-typst/tests/compile.rs @@ -199,7 +199,7 @@ fn file_tree_artifact_is_deferred() { }, info: Info { title: "t".into(), - author: None, + authors: vec![], }, parts: vec![], targets: vec![TargetConfig { @@ -238,7 +238,7 @@ fn shell_only_target_is_deferred() { }, info: Info { title: "t".into(), - author: None, + authors: vec![], }, parts: vec![], targets: vec![TargetConfig { diff --git a/docs/adr/0008-engineering-file-layout-conventions.md b/docs/adr/0008-engineering-file-layout-conventions.md index 34c67c1..cd66077 100644 --- a/docs/adr/0008-engineering-file-layout-conventions.md +++ b/docs/adr/0008-engineering-file-layout-conventions.md @@ -45,7 +45,7 @@ name = "…" # folder/display name [info] # passed through to render targets verbatim title = "…" -author = "…" +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) @@ -63,6 +63,18 @@ 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 diff --git a/spec/Spec/Courseware/Model.lean b/spec/Spec/Courseware/Model.lean index 2b64818..2cb5b0f 100644 --- a/spec/Spec/Courseware/Model.lean +++ b/spec/Spec/Courseware/Model.lean @@ -2,10 +2,12 @@ import Spec.Courseware.Model.Primitives import Spec.Courseware.Model.RichContent import Spec.Courseware.Model.Element import Spec.Courseware.Model.Lesson +import Spec.Courseware.Model.Info /-! # Courseware.Model —— 工程文件的内容模型 留白基元(`Primitives`)、富内容锚点(`RichContent`)、原子单位(`Element`)、单节课 -(`Lesson`)。决策出处 ADR-0005 / 0006。 +(`Lesson`)、课时元信息(`Info`:canonical author 为列表 vs `RawInfo` 授权 surface)。 +决策出处 ADR-0005 / 0006 / 0008。 -/ diff --git a/spec/Spec/Courseware/Model/Info.lean b/spec/Spec/Courseware/Model/Info.lean new file mode 100644 index 0000000..4c1d25f --- /dev/null +++ b/spec/Spec/Courseware/Model/Info.lean @@ -0,0 +1,58 @@ +/-! +# Info —— 课时元信息:canonical 模型 vs 授权 surface + +`[info]`(标题、作者)大多是 passthrough 元数据(ADR-0008),本不入契约。但**作者的 +基数**是一个真分歧点:一节课可由多人(教研组)署名,故 canonical 模型里 author 是一个 +**有序列表**,不是单值或可选单值。 + +另有一条值得钉的模式:on-disk 的授权形式是**语法糖**——单作者可写 `author = "…"`, +多作者写 `author = ["…", "…"]`——但这个"字符串或数组"的二态**只活在加载边界**:`RawInfo` +经归一化折叠成 canonical `Info`,其后不再出现。canonical 接收端始终是 `List String`, +raw 形式不泄漏进模型其余部分。这正是 `Info`(canonical)与 `RawInfo`(授权 surface) +两个结构存在的理由。 +-/ + +namespace Spec.Courseware + +/-- 作者的**授权 surface 形式**(`PINNED` 仅授权便利, ADR-0008)。on-disk 单作者可写裸 +字符串、多作者写数组——填写便利,非语义分歧。此 union **只活在加载边界**,经 +`RawAuthor.normalize` 折叠后不再出现。 -/ +inductive RawAuthor where + /-- 单作者裸字符串 `author = "…"`。 -/ + | one (name : String) + /-- 多作者数组 `author = ["…", "…"]`。 -/ + | many (names : List String) + +/-- raw 作者归一化为**有序作者列表**(`PINNED`, ADR-0008)。单作者 ⇒ 单元素列表;数组 +⇒ 原样。这条钉死"canonical 接收端始终是 `List String`"。 -/ +def RawAuthor.normalize : RawAuthor → List String + | .one n => [n] + | .many ns => ns + +/-- 课时元信息的 **canonical 模型**(`PINNED` author 为列表, ADR-0008)。`authors` 是 +**有序列表**:多人署名第一类,空列表 = 未署名。`title` 等其余字段是 passthrough 元数据, +不在此承诺更多。这是系统其余部分唯一所见的形态——author 在此**已**是列表,不再是 +"字符串或数组"。 -/ +structure Info where + /-- 标题(passthrough 元数据)。 -/ + title : String + /-- 作者**有序列表**(空 = 未署名)。canonical 始终是列表。 -/ + authors : List String + +/-- 授权 surface 的 `[info]`(`PINNED` 仅授权便利, ADR-0008)。`author` 用 `RawAuthor` +(字符串或数组),`author` 缺省即未署名。此结构刻画"为便于填写而存在的 raw 形态", +**不**是模型其余部分流通的形式——它经 `RawInfo.toInfo` 归一化为 canonical `Info`。 -/ +structure RawInfo where + /-- 标题。 -/ + title : String + /-- 作者 raw 形式(可选;缺省即未署名)。 -/ + author : Option RawAuthor + +/-- raw `[info]` 归一化为 canonical `Info`(`PINNED` 加载边界归一化, ADR-0008)。缺省 +author ⇒ 空列表,否则按 `RawAuthor.normalize`。raw 的"字符串或数组"二态在此被消解, +**不**泄漏进 `Info`——canonical 接收端恒为 `List String`。 -/ +def RawInfo.toInfo (r : RawInfo) : Info := + { title := r.title + authors := (r.author.map RawAuthor.normalize).getD [] } + +end Spec.Courseware