From 09b026f5989b9db4bc64b71f6988871a18f4475d Mon Sep 17 00:00:00 2001 From: sjfhsjfh Date: Mon, 22 Jun 2026 08:36:29 +0800 Subject: [PATCH] feat(spec): backfill Export terminology + diagnostics/legality/pipeline (ADR-0009/0010) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Lift the business decisions the MVP made into the Lean master, per constitution rule 5. lake build green (20 jobs), no sorry. - Artifact.lean: `inductive Artifact | singleFile | fileTree` — product shape is part of a target's value (ADR-0009); it determines the assemble/reduce step. - Render.lean reworked target-centric (ADR-0009, amends ADR-0005's matrix): `TargetSpec` carries `artifact` + a per-kind `renders` map (field visibility lives in this map); `RenderConfig.spec : TargetId → Option TargetSpec`; `covers` rewritten (target must exist AND its map covers the kind) — semantics continuous with ADR-0005 so renderIgnored still typechecks. `BuildStepForm` (declarative | shell) is a structural anchor for the build form (shell hatch = ADR-0005's medium-only category b) without replicating the schema. - Diagnostic.lean extended: `DiagKind` (7 classes) + `DiagKind.severity` (six error, renderIgnored warning); `Oracle` makes external-facility verdicts (compiles/refsResolve/dataConforms/contentFilesPresent) an explicit implementation boundary; `Legal` = no error-level diagnostic (backfills ADR-0005's deferred full-legality), with renderIgnored deliberately excluded (it's a warning). - Pipeline.lean: the 5 phases (load→structural→schema→compile→coverage) as structure — order + the compile gate (compile runs only on zero prior errors) + load halts the pipeline. Algorithms stay out of Lean (depth ceiling). Co-Authored-By: Claude Opus 4.8 (1M context) --- spec/Spec/Courseware.lean | 13 ++- spec/Spec/Courseware/Artifact.lean | 30 ++++++ spec/Spec/Courseware/Diagnostic.lean | 133 +++++++++++++++++++++++---- spec/Spec/Courseware/Pipeline.lean | 72 +++++++++++++++ spec/Spec/Courseware/Render.lean | 80 +++++++++++++--- 5 files changed, 293 insertions(+), 35 deletions(-) create mode 100644 spec/Spec/Courseware/Artifact.lean create mode 100644 spec/Spec/Courseware/Pipeline.lean diff --git a/spec/Spec/Courseware.lean b/spec/Spec/Courseware.lean index a3369f7..ab5c799 100644 --- a/spec/Spec/Courseware.lean +++ b/spec/Spec/Courseware.lean @@ -1,24 +1,31 @@ import Spec.Courseware.Primitives import Spec.Courseware.RichContent +import Spec.Courseware.Artifact import Spec.Courseware.Element import Spec.Courseware.Lesson import Spec.Courseware.Render import Spec.Courseware.Diagnostic +import Spec.Courseware.Pipeline import Spec.Courseware.QuestionBank import Spec.Courseware.Course /-! # Courseware —— 产品层契约(课程工程文件) -护城河:课程"工程文件"的语义母本与合法性规则。决策出处 ADR-0005 / 0006 / 0007。 +护城河:课程"工程文件"的语义母本与合法性规则。决策出处 ADR-0005 / 0006 / 0007 / 0008 +/ 0009 / 0010。 已填实(PINNED): - `Primitives` —— 基元载体(表示留给实现;schema 形态见 ADR-0006)。 - `RichContent` —— 富内容 = 带虚拟路径的 typst 源(ADR-0006 的 prose 母本)。 +- `Artifact` —— export 产物形状(单文件 / 文件树),target 值的一部分(ADR-0009)。 - `Element` —— kind 标签 + 依赖 schema 的数据。 - `Lesson` —— element 的有序序列(序载教学语义、不建模时长)。 -- `Render` —— (kind × target) 渲染配置矩阵 + covers。 -- `Diagnostic` —— Severity + checker 第一条诊断(缺渲染 ⇒ warning)。 +- `Render` —— export target = 一次 build(map + reduce):target-中心的 `TargetSpec` + 携产物形状 + per-kind map;`covers` 判定;build 形态结构锚点(ADR-0009,修订 ADR-0005)。 +- `Diagnostic` —— Severity + 7 类诊断的含义与级别 + **合法 lesson = 无 error 级诊断**; + 模型外设施诊断以抽象谓词 + `Oracle` 实现边界表示(ADR-0010)。 +- `Pipeline` —— 检查管线的 5 阶段、执行序、compile 门控(ADR-0010)。 留白骨架(核心关系 OPEN,已 surface 不臆造): - `QuestionBank` —— 题库与 element 的关系(引用 vs 内联)。 diff --git a/spec/Spec/Courseware/Artifact.lean b/spec/Spec/Courseware/Artifact.lean new file mode 100644 index 0000000..2f7ca52 --- /dev/null +++ b/spec/Spec/Courseware/Artifact.lean @@ -0,0 +1,30 @@ +/-! +# Artifact —— export target 的产物形状 + +ADR-0009:一个 export target 是**一次 build**,产出一个**有类型的产物**(artifact)。 +产物的**形状**是 target 值的一部分——"产出单个文件还是一棵文件树"是真分歧点,因为它 +改变 `cph build` 到底吐出什么、消费方期待什么,故进契约。 + +本模块只钉**形状**这一层。具体后端/格式(用哪个 PDF 引擎、哪种 markdown 方言)是 +ADR-0009 显式 OPEN 的,不在此承诺。 +-/ + +namespace Spec.Courseware + +/-- +export 产物的形状(`PINNED`, ADR-0009)。 + +- `singleFile` —— 一份打包文档(讲义 PDF、教案 PDF)。 +- `fileTree` —— 一棵文件树 + 索引(第三方平台 archive)。 + +**为什么这是分歧点而非实现细节**:产物是单件还是多件,决定 reduce/assemble 这一步 +怎么折叠(见 `Render`:`singleFile` 按 lesson 序拼成一份文档再编译——这也是交叉引用 +`@ref` 与 例题N 计数器能工作的前提;`fileTree` 每 part 一文件 + 索引),也决定 +`cph build` 写一个文件还是一个目录。后端/格式(typst→PDF、markdown 方言…)仍 OPEN, +故此处**只枚举形状**,不带后端标签。 +-/ +inductive Artifact where + | singleFile + | fileTree + +end Spec.Courseware diff --git a/spec/Spec/Courseware/Diagnostic.lean b/spec/Spec/Courseware/Diagnostic.lean index 2f75329..f57bdc6 100644 --- a/spec/Spec/Courseware/Diagnostic.lean +++ b/spec/Spec/Courseware/Diagnostic.lean @@ -2,44 +2,143 @@ import Spec.Courseware.Lesson import Spec.Courseware.Render /-! -# Diagnostic —— checker 诊断(种子) +# Diagnostic —— checker 诊断:分类、严重级别、合法 lesson -产品里"站在 Lean 位置"的那个 rule-based checker,语义在此沉淀。它对 lesson 提诊断, -每条诊断有**严重级别**。本模块固定级别类型,并落第一条规则——ADR-0005 钉死的"缺 -渲染 ⇒ warning"。完整的"合法 lesson"判定仍 OPEN,本模块只是它的起点。 +产品里"站在 Lean 位置"的那个 rule-based checker,语义在此沉淀(ADR-0010)。它对 lesson +提诊断,每条诊断有**分类**(`DiagKind`)与**严重级别**(`Severity`)。本模块: + +1. 钉级别类型(二分,ADR-0005)。 +2. 钉 7 类诊断各自的含义与级别(ADR-0010),并把"**合法 lesson = 无 error 级诊断**" + 建成判定——这是 ADR-0005 deferred 的"完整合法判定"的回填。 +3. 对**模型外设施**型诊断(typst 能否编过、引用悬否、数据合 schema 否),用**抽象谓词 + + 显式实现边界**表示:契约说"存在这样一条诊断、它什么意思、什么级别",但其**真值由 + 实现(checker)提供**,不在 Lean 内计算——保持契约诚实(不内嵌 typst 编译器)。 -/ namespace Spec.Courseware /-- -诊断的严重级别(`PINNED` 二分, ADR-0005 区分 warning 与阻断)。 +诊断的严重级别(`PINNED` 二分, ADR-0005)。 -`error` 阻断(产物不合法),`warning` 不阻断(产物仍可导出,只是有损/有忽略)。 -ADR-0005 已用到这个区分:缺渲染是 warning 而非 error。更细的级别(info/hint)未 -决策,故只二分。 +`error` 阻断(产物不合法),`warning` 不阻断(产物仍可导出,只是有损/有忽略)。更细的 +级别(info/hint)未决策,故只二分。 -/ inductive Severity where | warning | error +/-- +诊断的**分类**(`PINNED` 7 类, ADR-0010)。每类含义见下;级别见 `DiagKind.severity`。 + +按"谁来判定"分三层(ADR-0010 的边界): +- **结构型**(模型自身可判):`partPathMissing` / `unknownKind`。 +- **schema / 外部设施型**(判定靠实现 oracle):`missingContentFile` / `schemaViolation` + / `danglingReference` / `typstCompile`。 +- **语义型**(coverage 规则):`renderIgnored`。 +-/ +inductive DiagKind where + /-- manifest 的 part 指向不存在的文件夹(或经 `..` 逃出根)。结构型。 -/ + | partPathMissing + /-- part 声明了未知 kind(含 part 与 element.toml 的 kind 不一致)。结构型。 -/ + | unknownKind + /-- kind schema 要求的某 `content` 字段缺对应 `.typ`。结构/schema 型。 -/ + | missingContentFile + /-- 实例数据不合其 kind 的 JSON Schema(标量类型错/缺必填/多余键);亦作 manifest/ + element.toml 畸形的兜底。schema / 外部设施型。 -/ + | schemaViolation + /-- 引用不解析:越界的相对 import,或悬空的交叉引用。外部设施型。 -/ + | danglingReference + /-- 拼装出的 typst 源编译失败(语法错、`@ref` 未解析…)。外部设施型。 -/ + | typstCompile + /-- 某被用到的 kind 在某声明的 target 下无渲染规则,该 element 被该 target 忽略。语义型。 -/ + | renderIgnored + +/-- +每类诊断的**严重级别**(`PINNED`, ADR-0010)。 + +六类为 `error`(阻断);**唯 `renderIgnored` 为 `warning`**——即 ADR-0005 的种子规则 +"缺渲染 ⇒ warning,不阻断导出"。把级别钉成一个全函数,使"哪类阻断、哪类不阻断"成为 +契约里可引用、可对齐的事实(实现侧 `DiagCode` 的级别据此对齐)。 +-/ +def DiagKind.severity : DiagKind → Severity + | .partPathMissing => .error + | .unknownKind => .error + | .missingContentFile => .error + | .schemaViolation => .error + | .danglingReference => .error + | .typstCompile => .error + | .renderIgnored => .warning + +/-- 缺渲染诊断的级别 = **warning**(`PINNED`, ADR-0005/0010,**非 error**)。 + +保留为具名常量,使"它是 warning 不是 error"可被实现侧 grep 对齐(实现里同名常量 +`RENDER_IGNORED_SEVERITY` 引用本定义)。等价于 `DiagKind.severity .renderIgnored`。 -/ +def renderIgnoredSeverity : Severity := DiagKind.renderIgnored.severity + variable (P : Primitives) /-- -**缺渲染诊断**:lesson 在 target `t` 下存在无法渲染的 element(`PINNED`, ADR-0005)。 +**缺渲染诊断**:lesson 在 target `t` 下存在无法渲染的 element(`PINNED`, ADR-0005/0009)。 -成立 ⟺ 存在某 element,其 kind 在 `t` 下未配渲染规则。这条对应 checker 的第一条 -诊断;其级别由下面的 `renderIgnoredSeverity` 钉死为 **warning**。 +成立 ⟺ 存在某 element,其 kind 在 `t` 下未配渲染规则(`covers` 为假,见 `Render`)。这条 +是 checker 的**语义型**诊断,级别由 `renderIgnoredSeverity` 钉为 warning。`covers` 已随 +ADR-0009 下沉到 target 的 build 规格,但本判定式不变。 -/ def renderIgnored (l : Lesson P) (c : RenderConfig P) (t : P.TargetId) : Prop := ∃ e ∈ l, ¬ c.covers e.kind t -/-- -缺渲染诊断的级别 = **warning**(`PINNED`, ADR-0005,**非 error**)。 +/-! +## 模型外设施型诊断:抽象谓词 + 实现边界(ADR-0010) -ADR-0005 明确:某 (kind, target) 无渲染规则时,checker 报 warning 说该 element 在 -该 target 被忽略,**不阻断导出**。把这条决策固定为一个常量,使"它是 warning 不是 -error"成为契约里可被引用、可被对齐的事实,而不是散落在 prose 里的口头约定。 +`typstCompile` / `danglingReference` / `schemaViolation`(的 schema-合规面)断言的是 +**模型自身无法判定**的事实——要跑 typst 编译器、要跑 schema 校验器。契约因此把它们建成 +**抽象谓词**,真值由一个**实现提供的 oracle** 给出。Lean 只说"这条诊断存在、什么意思、 +什么级别",**不**在 Lean 内计算其真假。 + +下面用一个 `Oracle` 结构收口这些实现侧判定。它**不是**要在 Lean 里实现 checker,而是 +把"这些事实来自模型外"这件事显式化、类型化:谁想谈论一节 lesson 合不合法,就得先有一个 +oracle 提供这些外部判定。 -/ -def renderIgnoredSeverity : Severity := .warning + +/-- +**实现侧判定 oracle**(`PINNED` 实现边界, ADR-0010)。 + +收口那些"模型外设施"才能回答的判定。每个字段是一个谓词,**真值由实现(checker)提供**: + +- `compiles` —— 该 lesson 在 target `t` 下拼装出的 typst 源能否编译通过(否 ⇒ `typstCompile`)。 +- `refsResolve` —— 该 lesson 的引用(相对 import / 交叉引用)是否全部解析(否 ⇒ `danglingReference`)。 +- `dataConforms` —— 每个 element 的数据是否合其 kind schema(否 ⇒ `schemaViolation`)。 +- `contentFilesPresent` —— schema 要求的 `content` 文件是否齐备(否 ⇒ `missingContentFile`)。 + +把它们作为参数,正是"显式实现边界":契约能据此**定义**合法性,却不假装自己能算出这些 +外部事实。结构型诊断(part 路径、未知 kind)不入此 oracle——那些模型自身可判。 +-/ +structure Oracle (l : Lesson P) (c : RenderConfig P) where + /-- target `t` 下拼装源可编译。 -/ + compiles : P.TargetId → Prop + /-- 引用全部解析。 -/ + refsResolve : Prop + /-- 每个 element 数据合 schema。 -/ + dataConforms : Prop + /-- schema 要求的 content 文件齐备。 -/ + contentFilesPresent : Prop + +/-- +**合法 lesson**(`PINNED`, ADR-0010;回填 ADR-0005 deferred 的"完整合法判定")。 + +一节 lesson 合法 ⟺ 检查管线产出**零条 error 级诊断**。warning(如 `renderIgnored`) +不影响合法性——带 warning 的 lesson 仍合法、仍可(有损)导出。 + +这里把"无 error 级诊断"展开为:模型外设施判定(经 `Oracle`)全部为真,**且**每个声明的 +target 都编译通过。结构型诊断(part 路径、未知 kind、kind 不一致)由 `cph-model` 在加载 +期判定;能走到这一步谈合法性,意味着已加载成功,故此处聚焦 schema/外部设施层。注意 +`renderIgnored` 是 warning,**不**进合法性合取——这正是 ADR-0005 种子规则的体现。 + +`targets` 是该工程文件声明的 target 列表(`RenderConfig.spec t` 非 `none` 者);为保持 +本层抽象、不绑定 `TargetId` 的可枚举性,这里用"对所有满足前提的 t"的全称式表达。 +-/ +def Legal (l : Lesson P) (c : RenderConfig P) (o : Oracle P l c) : Prop := + o.refsResolve ∧ o.dataConforms ∧ o.contentFilesPresent ∧ + (∀ t : P.TargetId, (c.spec t).isSome → o.compiles t) end Spec.Courseware diff --git a/spec/Spec/Courseware/Pipeline.lean b/spec/Spec/Courseware/Pipeline.lean new file mode 100644 index 0000000..16bf937 --- /dev/null +++ b/spec/Spec/Courseware/Pipeline.lean @@ -0,0 +1,72 @@ +import Spec.Courseware.Diagnostic + +/-! +# Pipeline —— checker 检查管线的阶段与序(ADR-0010) + +checker 的 `check` 按**固定顺序**跑五个阶段,逐阶段收集诊断;`compile` 阶段有**门控**。 +顺序与门控是契约——它决定用户看到哪些诊断(藏在缺文件背后的语法错,在文件补齐前不显示, +这是**有意**的)。每阶段的**算法**不进 Lean(宪法第 5 条深度上限):本模块只钉**阶段、序、 +门控**,不形式化每步怎么算。 + +阶段与上游模块的对应:`load` ← `cph-model`;`structural` ← part 路径/未知 kind;`schema` +← `cph-schema`;`compile` ← `cph-typst`(模型外设施,见 `Diagnostic.Oracle`);`coverage` +← `Diagnostic.renderIgnored`。 +-/ + +namespace Spec.Courseware + +/-- +检查管线的**阶段**(`PINNED` 5 阶段, ADR-0010)。 + +- `load` —— 解析 manifest + 各 element.toml。硬失败(无可解析 lesson)则**停**整条管线。 +- `structural` —— part 路径存在、无 `..`、kind 已知、part 与 element kind 一致。此处已被 + 判缺的 part,在后续阶段**跳过**(不在同一根因上堆诊断)。 +- `schema` —— 每个"存在且 kind 已知"的 part 的数据按其 kind schema 校验(标量 + content 文件)。 +- `compile` —— 模型外设施阶段(typst 编译)。**门控:仅当 `load`/`structural`/`schema` 零 + error 才跑**(否则在已知坏输入上编译只是噪声)。跑时对每个声明的 target 编译(ADR-0009)。 +- `coverage` —— 语义型 warning 规则(`renderIgnored`);**不**受门控,总跑。 +-/ +inductive Phase where + | load + | structural + | schema + | compile + | coverage +deriving DecidableEq + +/-- +管线阶段的**执行序**(`PINNED`, ADR-0010)。`order p` 越小越先跑。 + +序是契约:`compile`(3)排在 `structural`(1)/`schema`(2)之后,正因前者门控于后者无 error。 +`coverage`(4)排最后但不门控(见 `gated`)。 +-/ +def Phase.order : Phase → Nat + | .load => 0 + | .structural => 1 + | .schema => 2 + | .compile => 3 + | .coverage => 4 + +/-- +某阶段是否**受"前序零 error"门控**(`PINNED`, ADR-0010)。 + +唯 `compile` 受门控:前序(load/structural/schema)出任何 error 则跳过它——藏在结构/schema +错背后的编译错,在前者修好前不显示,这是有意的降噪。其余阶段不门控:`load` 是入口, +`structural`/`schema` 是门控的**依据**(自身得先跑),`coverage` 产 warning 故无条件跑。 +-/ +def Phase.gated : Phase → Bool + | .compile => true + | _ => false + +/-- +管线在 `load` 硬失败时**停**(`PINNED`, ADR-0010)。 + +`load` 拿不到可解析的 lesson(`cph-model` 返回 `none`)时,没有 lesson 可喂给下游, +整条管线就此终止——这是唯一会"截断"后续所有阶段的情形(区别于 `compile` 的门控只跳过 +自己)。 +-/ +def Phase.haltsPipelineOnFailure : Phase → Bool + | .load => true + | _ => false + +end Spec.Courseware diff --git a/spec/Spec/Courseware/Render.lean b/spec/Spec/Courseware/Render.lean index 76a5895..5f50941 100644 --- a/spec/Spec/Courseware/Render.lean +++ b/spec/Spec/Courseware/Render.lean @@ -1,11 +1,23 @@ import Spec.Courseware.Primitives +import Spec.Courseware.Artifact /-! -# Render —— 渲染配置矩阵 +# Render —— export target = 一次 build(ADR-0009,修订 ADR-0005) -ADR-0005:某 kind 在某 target 下如何呈现,由一份 **(kind × target) 配置矩阵**决定; -矩阵住在工程文件里,框架给 default、文件可 override。本模块只建矩阵结构与"是否已 -配置"的判定;规则的**内容**(`RenderRule`)是 OPEN,不碰。 +ADR-0005 曾把渲染建成被动的 (kind × target) 查表矩阵。ADR-0009 **修订**之:一个 export +target 是**一次 build**,消费整节 lesson、产出一个有类型的 `Artifact`。一次 build = +**map + reduce**: + +- **map(per-kind)**:每个 kind 如何变成中间片段——声明式、按 kind 索引;`RenderRule` + 是这张 map 的载荷。**字段可见性**(student 隐 `solution`/`proof`,teacher 全显)就住在 + 这张 per-kind map 里,不是独立概念、也不在 element 上。 +- **reduce/assemble**:有序片段如何折叠成产物——**由 `Artifact` 形状决定**(见 + `Courseware.Artifact`),框架按形状提供 assembler,build 只挑形状。 + +本模块建 target-中心的结构与"某 kind 在某 target 下是否已配规则"的判定(`covers`, +`Diagnostic` 依赖它)。`RenderRule` 的载荷仍由 `Primitives` 抽象承载(ADR-0009 显式 +OPEN);build 形态(声明式 + shell 口子)以一个**结构锚点** `BuildStepForm` 体现——钉 +"该有的结构"而**不**复刻具体 schema(宪法第 5 条)。 -/ namespace Spec.Courseware @@ -13,24 +25,62 @@ namespace Spec.Courseware variable (P : Primitives) /-- -渲染配置矩阵(`PINNED`, ADR-0005)。 +build 步骤的**形态**(结构锚点, ADR-0009;具体 schema 字段 `OPEN`)。 -`rule k t = none` 表示 (kind `k`, target `t`) 这一对**尚无渲染规则**;`some _` 表示 -有。框架默认与文件 override 最终都坍缩成这一个映射——契约不区分"默认值"与"用户改 -过的值",只看最终矩阵在每一格的有无。 +ADR-0009 定 build 的表达形态 = **声明式 schema + 一个 `run`-shell 逃生口**(近似 +GitHub Actions、**非** Makefile)。这里只把这个二分立成一个具名结构,让"build 要么声明 +式、要么走 shell 口子"成为契约里可引用的事实: + +- `declarative` —— 声明式步骤(per-kind map 的常规情形)。 +- `shell` —— shell 逃生口。ADR-0005 的 (b) 类 medium-only 信息(HTML 交互、npm build) + 正是落在这里——它属于 target 的 build,**不**上 element。 + +**刻意不**把 schema 的字段、shell 命令的内部结构写进来:那是实现细节(ADR-0009 OPEN), +此锚点只承诺"build 步骤分声明式与 shell 两形态"这一骨架。 -/ -structure RenderConfig where - /-- (kind, target) ↦ 该对的渲染规则(无则 `none`)。 -/ - rule : P.KindId → P.TargetId → Option P.RenderRule +inductive BuildStepForm where + | declarative + | shell /-- -kind `k` 在 target `t` 下**已配渲染规则**(`PINNED`, ADR-0005)。 +一个 export target 的 build 规格(`PINNED` target-中心结构, ADR-0009)。 -即矩阵该格非空。`covers` 为假即"此 kind 在此 target 下无从渲染"——checker 据此报 -警(见 `Spec.Courseware.Diagnostic`)。`P` 隐式,以便 `c.covers k t` 点记法可用。 +- `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);契约只看最终每格的有无,不区分"默认"与"改过"。 +-/ +structure TargetSpec where + /-- 该 target 产物的形状(decides assemble, ADR-0009)。 -/ + artifact : Artifact + /-- per-kind map:kind ↦ 该 kind 在此 target 下的渲染规则(无则 `none`)。 -/ + renders : P.KindId → Option P.RenderRule + +/-- +渲染配置(`PINNED` target-中心, ADR-0009;修订 ADR-0005 的矩阵)。 + +`spec t = none` 表示 target `t` **未声明**(此工程文件不导出该 target);`some s` 给出该 +target 的 build 规格 `s`。注意这比旧矩阵多了一层:旧矩阵默认每个 (kind,target) 格都在, +现在先要 target **存在**,其 build 规格再各自决定每个 kind 渲不渲。 +-/ +structure RenderConfig where + /-- target ↦ 该 target 的 build 规格(未声明则 `none`)。 -/ + spec : P.TargetId → Option (TargetSpec P) + +/-- +kind `k` 在 target `t` 下**已配渲染规则**(`PINNED`, ADR-0009;承接 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` 隐式以便点记法。 -/ def RenderConfig.covers {P : Primitives} (c : RenderConfig P) (k : P.KindId) (t : P.TargetId) : Prop := - (c.rule k t).isSome + match c.spec t with + | none => False + | some s => (s.renders k).isSome end Spec.Courseware