diff --git a/spec/Spec/Courseware.lean b/spec/Spec/Courseware.lean index ab5c799..ee76da3 100644 --- a/spec/Spec/Courseware.lean +++ b/spec/Spec/Courseware.lean @@ -13,16 +13,18 @@ import Spec.Courseware.Course # Courseware —— 产品层契约(课程工程文件) 护城河:课程"工程文件"的语义母本与合法性规则。决策出处 ADR-0005 / 0006 / 0007 / 0008 -/ 0009 / 0010。 +/ 0009 / 0010 / 0011。 已填实(PINNED): - `Primitives` —— 基元载体(表示留给实现;schema 形态见 ADR-0006)。 - `RichContent` —— 富内容 = 带虚拟路径的 typst 源(ADR-0006 的 prose 母本)。 -- `Artifact` —— export 产物形状(单文件 / 文件树),target 值的一部分(ADR-0009)。 +- `Artifact` —— export 产物(带字段 ADT:`singleFile filepath` / `fileTree root outputs`), + target 值的一部分(ADR-0009/0011)。 - `Element` —— kind 标签 + 依赖 schema 的数据。 - `Lesson` —— element 的有序序列(序载教学语义、不建模时长)。 -- `Render` —— export target = 一次 build(map + reduce):target-中心的 `TargetSpec` - 携产物形状 + per-kind map;`covers` 判定;build 形态结构锚点(ADR-0009,修订 ADR-0005)。 +- `Render` —— export target = artifact + 有序 typed steps:`TargetSpec` 携 `artifact` + + `steps : List Step`(`typstCompile template` / `shell run`)+ 覆盖声明 `covers`; + `RenderConfig.covers` 判定(ADR-0009/0011,修订 ADR-0005)。RenderRule 载荷已废止。 - `Diagnostic` —— Severity + 7 类诊断的含义与级别 + **合法 lesson = 无 error 级诊断**; 模型外设施诊断以抽象谓词 + `Oracle` 实现边界表示(ADR-0010)。 - `Pipeline` —— 检查管线的 5 阶段、执行序、compile 门控(ADR-0010)。 diff --git a/spec/Spec/Courseware/Artifact.lean b/spec/Spec/Courseware/Artifact.lean index 2f7ca52..4f6fe55 100644 --- a/spec/Spec/Courseware/Artifact.lean +++ b/spec/Spec/Courseware/Artifact.lean @@ -1,30 +1,35 @@ /-! -# Artifact —— export target 的产物形状 +# Artifact —— export target 的产物(ADR-0009 / 0011) ADR-0009:一个 export target 是**一次 build**,产出一个**有类型的产物**(artifact)。 -产物的**形状**是 target 值的一部分——"产出单个文件还是一棵文件树"是真分歧点,因为它 -改变 `cph build` 到底吐出什么、消费方期待什么,故进契约。 +ADR-0011 进一步钉死:产物不是一个光秃的标签,而是**带字段的 ADT**——"产物到底指什么" +(单个文件落在哪 / 一棵树产出哪些文件)是不好猜的领域语义,必须写进字段 + doc,而非 +抹成 `singleFile | fileTree` 两个空构造子。 -本模块只钉**形状**这一层。具体后端/格式(用哪个 PDF 引擎、哪种 markdown 方言)是 -ADR-0009 显式 OPEN 的,不在此承诺。 +路径/glob 在此用 `String` 承载并由 doc 赋义(它们就是文本:一个相对路径、一个 glob +模式),不复刻文件系统类型——契约只钉"这个字段是什么",不建模路径代数。 -/ namespace Spec.Courseware /-- -export 产物的形状(`PINNED`, ADR-0009)。 +export 产物(`PINNED` 带字段 ADT, ADR-0011)。 -- `singleFile` —— 一份打包文档(讲义 PDF、教案 PDF)。 -- `fileTree` —— 一棵文件树 + 索引(第三方平台 archive)。 +- `singleFile (filepath)` —— 产物是**单个文件**,落在 `filepath`(相对工程根的路径)。 + 讲义 PDF、教案 PDF 即此。`filepath` 说清"这一份产物写到哪"。 +- `fileTree (root) (outputs)` —— 产物是 `root` 目录下、匹配 `outputs` **glob** 的**一组 + 文件**(第三方平台 archive 即此)。用 glob 而非显式清单:比逐个枚举轻,又让消费方/ + checker 知道"这次 build 该产出哪些文件"、可据以校验产物完整性。 -**为什么这是分歧点而非实现细节**:产物是单件还是多件,决定 reduce/assemble 这一步 -怎么折叠(见 `Render`:`singleFile` 按 lesson 序拼成一份文档再编译——这也是交叉引用 -`@ref` 与 例题N 计数器能工作的前提;`fileTree` 每 part 一文件 + 索引),也决定 -`cph build` 写一个文件还是一个目录。后端/格式(typst→PDF、markdown 方言…)仍 OPEN, -故此处**只枚举形状**,不带后端标签。 +**为什么字段进契约**:产物形状决定 `cph build` 吐一个文件还是一个目录、消费方期待什么; +也决定 reduce/assemble 怎么折叠(`singleFile` 把有序片段拼成一份再编译——这也是交叉引用 +`@ref` 与 例题N 计数器能工作的前提;`fileTree` 每 part 落一文件)。后端/格式(哪个 PDF +引擎、哪种 markdown 方言)仍 OPEN(ADR-0009),不在字段里。 -/ inductive Artifact where - | singleFile - | fileTree + /-- 单文件产物,落在 `filepath`(相对工程根)。 -/ + | singleFile (filepath : String) + /-- 多文件产物:`root` 目录下匹配 `outputs` glob 的文件集。 -/ + | fileTree (root : String) (outputs : String) end Spec.Courseware diff --git a/spec/Spec/Courseware/Primitives.lean b/spec/Spec/Courseware/Primitives.lean index ff91b45..0c03121 100644 --- a/spec/Spec/Courseware/Primitives.lean +++ b/spec/Spec/Courseware/Primitives.lean @@ -40,15 +40,11 @@ structure Primitives where "存在一个由 kind 决定的合法数据类型",不复刻 JSON Schema / typst Content 的形状。 -/ ElementData : KindId → Type - /-- export target 的标识(`PINNED` 角色, ADR-0005;表示 `OPEN`)。一个 target 是对 lesson 的一种投影(讲义/教案/PPT/平台 archive…)。 -/ + /-- export target 的标识(`PINNED` 角色, ADR-0005;表示 `OPEN`)。一个 target 是一次 build,产出对 lesson 的一种投影(讲义/教案/PPT/平台 archive…),见 `Render`。 -/ TargetId : Type - /-- - 渲染规则的载荷(表示 `OPEN`, ADR-0005)。 - "某 kind 在某 target 下如何呈现"那条规则的**内容**。typst 是渲染后端之一(`PINNED`, - ADR-0005)、不是定义语言;但渲染管线/规则载荷的具体表示仍 `OPEN`。契约只关心规则 - **在不在**(见 `Render`),不碰它是什么。 - -/ - RenderRule : Type +-- 注:原有 `RenderRule : Type` 已随 ADR-0011 移除。渲染的"how"不再是契约层的 per-target +-- 载荷,而是 `Render.TargetSpec.steps` 里 `typstCompile` step 所引用的**模板文件**承载; +-- 契约只保留覆盖声明 `TargetSpec.covers`(该 target 渲染哪些 kind),供种子诊断用。 end Spec.Courseware diff --git a/spec/Spec/Courseware/Render.lean b/spec/Spec/Courseware/Render.lean index 5f50941..25a0d0c 100644 --- a/spec/Spec/Courseware/Render.lean +++ b/spec/Spec/Courseware/Render.lean @@ -2,22 +2,25 @@ import Spec.Courseware.Primitives import Spec.Courseware.Artifact /-! -# Render —— export target = 一次 build(ADR-0009,修订 ADR-0005) +# Render —— export target = artifact + 有序 typed steps(ADR-0009 / 0011) -ADR-0005 曾把渲染建成被动的 (kind × target) 查表矩阵。ADR-0009 **修订**之:一个 export -target 是**一次 build**,消费整节 lesson、产出一个有类型的 `Artifact`。一次 build = -**map + reduce**: +ADR-0009:export target 是**一次 build**,产出一个有类型的 `Artifact`。ADR-0011 钉死 +build 的**形状**:一个 target 是 `artifact` + 一串**有序的 typed step**。每个 step 是一个 +**有类型的操作**: -- **map(per-kind)**:每个 kind 如何变成中间片段——声明式、按 kind 索引;`RenderRule` - 是这张 map 的载荷。**字段可见性**(student 隐 `solution`/`proof`,teacher 全显)就住在 - 这张 per-kind map 里,不是独立概念、也不在 element 上。 -- **reduce/assemble**:有序片段如何折叠成产物——**由 `Artifact` 形状决定**(见 - `Courseware.Artifact`),框架按形状提供 assembler,build 只挑形状。 +- `typstCompile template` —— 把**模板文件**(如 `exports/student.typ`)编译成产物。它是 + *typed* 而非裸 shell,正因框架要把 **manifest 注入**模板(经 `--input manifest=…`), + 裸 `typst compile` 字符串表达不了这个 wiring。presentation(numbly 编号、样式)住在 + 模板里,**不**在 manifest。 +- `shell run` —— 逃生口,给难以声明的步骤(ADR-0005 的 (b) 类 medium-only:HTML 交互、 + npm build 落这)。 -本模块建 target-中心的结构与"某 kind 在某 target 下是否已配规则"的判定(`covers`, -`Diagnostic` 依赖它)。`RenderRule` 的载荷仍由 `Primitives` 抽象承载(ADR-0009 显式 -OPEN);build 形态(声明式 + shell 口子)以一个**结构锚点** `BuildStepForm` 体现——钉 -"该有的结构"而**不**复刻具体 schema(宪法第 5 条)。 +MVP 每个 target 只有一个 `typstCompile` step,但 `steps` 是 **list**,因为 `FileTree` / +第三方 build 会需要多步。 + +**渲染覆盖**:ADR-0011 废止了 per-target 的 `RenderRule` 载荷——渲染的"how"已移进模板。 +契约只保留**覆盖声明** `covers : KindId → Prop`(该 target 渲染哪些 kind),供种子诊断用; +模板是其实现。`RenderConfig.covers`/`renderIgnored` 据此,ADR-0005 种子规则不变。 -/ namespace Spec.Courseware @@ -25,62 +28,61 @@ namespace Spec.Courseware variable (P : Primitives) /-- -build 步骤的**形态**(结构锚点, ADR-0009;具体 schema 字段 `OPEN`)。 +一个 build **step**(`PINNED` typed, ADR-0011;可扩展)。 -ADR-0009 定 build 的表达形态 = **声明式 schema + 一个 `run`-shell 逃生口**(近似 -GitHub Actions、**非** Makefile)。这里只把这个二分立成一个具名结构,让"build 要么声明 -式、要么走 shell 口子"成为契约里可引用的事实: +- `typstCompile (template)` —— 编译模板文件(相对工程根的路径)成产物;框架把 manifest + 注入它。**typed** 的理由:注入这件事裸 shell 写不出。 +- `shell (run)` —— 逃生口,执行 `run` 命令(ADR-0005 的 (b) 类落这)。MVP 不实现,先建结构。 -- `declarative` —— 声明式步骤(per-kind map 的常规情形)。 -- `shell` —— shell 逃生口。ADR-0005 的 (b) 类 medium-only 信息(HTML 交互、npm build) - 正是落在这里——它属于 target 的 build,**不**上 element。 - -**刻意不**把 schema 的字段、shell 命令的内部结构写进来:那是实现细节(ADR-0009 OPEN), -此锚点只承诺"build 步骤分声明式与 shell 两形态"这一骨架。 +**刻意不**把模板内部、shell 命令的解析结构写进来:那是实现细节(ADR-0011 OPEN)。此处只钉 +"step 是有类型操作,目前两型,可扩展"这一骨架。 -/ -inductive BuildStepForm where - | declarative - | shell +inductive Step where + /-- 编译模板文件 `template`(相对工程根)成产物;框架注入 manifest。 -/ + | typstCompile (template : String) + /-- shell 逃生口:执行命令 `run`。 -/ + | shell (run : String) /-- -一个 export target 的 build 规格(`PINNED` target-中心结构, ADR-0009)。 +一个 export target 的 build 规格(`PINNED` artifact + 有序 steps, ADR-0011)。 -- `artifact` —— 产物形状(`Courseware.Artifact`)。它**决定** reduce/assemble 怎么折叠 - (单文件 vs 文件树),故是 target 值的一部分,而非事后的输出选项。 -- `renders` —— per-kind map:`renders k = none` 表示 kind `k` 在此 target 下**无渲染 - 规则**(该 element 会被该 target 忽略,见 `Diagnostic.renderIgnored`);`some _` 表示 - 有。框架默认与文件 override 最终坍缩成这一个映射(ADR-0009 的 default-at-creation + - 文件内 override);契约只看最终每格的有无,不区分"默认"与"改过"。 +- `artifact` —— 产物(`Courseware.Artifact`,带字段)。决定 build 折叠成单文件还是文件树。 +- `steps` —— **有序** step 列表。按序执行;MVP 仅一个 `typstCompile`。 +- `covers` —— **覆盖声明**:`covers k` 表示此 target **渲染** kind `k`。这是 ADR-0011 把 + 旧 `renders : KindId → Option RenderRule` 降级后的产物——契约只声明"渲染哪些 kind" + (种子诊断 `renderIgnored` 用),渲染的"how"由 `steps` 的模板实现,不再是契约层载荷。 -/ structure TargetSpec where - /-- 该 target 产物的形状(decides assemble, ADR-0009)。 -/ + /-- 产物(带字段, ADR-0011)。 -/ artifact : Artifact - /-- per-kind map:kind ↦ 该 kind 在此 target 下的渲染规则(无则 `none`)。 -/ - renders : P.KindId → Option P.RenderRule + /-- 有序 build steps。 -/ + steps : List Step + /-- 覆盖声明:此 target 是否渲染该 kind。 -/ + covers : P.KindId → Prop /-- -渲染配置(`PINNED` target-中心, ADR-0009;修订 ADR-0005 的矩阵)。 +渲染配置(`PINNED` target-中心, ADR-0009/0011)。 `spec t = none` 表示 target `t` **未声明**(此工程文件不导出该 target);`some s` 给出该 -target 的 build 规格 `s`。注意这比旧矩阵多了一层:旧矩阵默认每个 (kind,target) 格都在, -现在先要 target **存在**,其 build 规格再各自决定每个 kind 渲不渲。 +target 的 build 规格 `s`(artifact + steps + 覆盖声明)。 -/ structure RenderConfig where /-- target ↦ 该 target 的 build 规格(未声明则 `none`)。 -/ spec : P.TargetId → Option (TargetSpec P) /-- -kind `k` 在 target `t` 下**已配渲染规则**(`PINNED`, ADR-0009;承接 ADR-0005 `covers`)。 +kind `k` 在 target `t` 下**被渲染**(`PINNED`, ADR-0009/0011;承接 ADR-0005 `covers`)。 -成立 ⟺ target `t` 已声明(`spec t = some s`)**且**其 per-kind map 对 `k` 非空 -(`s.renders k = some _`)。`covers` 为假即"此 kind 在此 target 下无从渲染"——checker -据此报 warning(见 `Spec.Courseware.Diagnostic.renderIgnored`)。语义与 ADR-0005 的 -`covers` 连续,只是判定下沉到 target 的 build 规格里。`P` 隐式以便点记法。 +成立 ⟺ target `t` 已声明(`spec t = some s`)**且**其覆盖声明含 `k`(`s.covers k`)。 +`covers` 为假即"此 kind 在此 target 下不被渲染"——checker 据此报 warning(见 +`Spec.Courseware.Diagnostic.renderIgnored`)。语义与 ADR-0005 连续,只是判定基底从 +"有无 RenderRule"换成"覆盖声明是否含此 kind"(ADR-0011 废 RenderRule 载荷)。`P` 隐式 +以便点记法。 -/ def RenderConfig.covers {P : Primitives} (c : RenderConfig P) (k : P.KindId) (t : P.TargetId) : Prop := match c.spec t with | none => False - | some s => (s.renders k).isSome + | some s => s.covers k end Spec.Courseware