From 73e9d258d6b4db0cb57a704b10c829e524e05829 Mon Sep 17 00:00:00 2001 From: sjfhsjfh Date: Thu, 25 Jun 2026 03:22:59 +0800 Subject: [PATCH] =?UTF-8?q?docs(spec):=20=E9=87=8D=E5=86=99=20spec/=20?= =?UTF-8?q?=E4=B8=8E=E6=A0=B9=20README=20=E7=9A=84=E8=AF=AD=E8=A8=80?= =?UTF-8?q?=E4=B8=8E=E5=8F=96=E8=88=8D?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 按新文风(简洁书面中文)重写 spec/ 全部 Lean doc 注释、spec/README, 并顺根 README。核心:讲清产品逻辑、去伪术语、去 ADR 黑话、DRY。 语言:砍钉死/留痕/实现侧/将就/脑补/刻意等伪术语;短句;不复述文件系统 能看到的东西;typst 考据移出 spec 指向 ADR。 内容取舍(动结构): - System 层大改:删 can_mono 形式化定理、Capability 9 项枚举与 requiredRole 映射、RunState 6 构造子;Audit.lean 删除并入 System 顶部。 Hub 未建的部分一律 prose 占位,只留 Lock 的 owner=run 与 WellFormed。 - 澄清两个"检查":产品 checker(LLM 判不了合法性,checker 真跑工具补这块) vs 开发时 spec↔impl 一致性检查(无自动闸门)。Oracle 重新定位为 "checker 得委托外部工具才能判的事实",不是"Lean 没写形式化"。 - spec/README 补取舍判据 checklist(自顶向下逐步细化、不在 Lean 里验证实现)。 - 根 README 去 DRY:删硬编码版本号、cache 路径细节;宪法第 3 条吸收 "人/coding assistant 核对"修正;第 5 条与 spec/README 判据去重。 保留:Export/Render 执行语义、Info 的 raw→canonical 设计模式(产品语义, 只顺文风不砍结构);renderIgnoredSeverity(实现对齐依赖)。 lake build 通过(24 jobs)。 Co-Authored-By: Claude --- README.md | 86 ++++++++-------- spec/README.md | 89 +++++++++------- spec/Spec/Courseware.lean | 13 +-- spec/Spec/Courseware/Check.lean | 2 +- spec/Spec/Courseware/Check/Diagnostic.lean | 106 ++++++++++--------- spec/Spec/Courseware/Check/Pipeline.lean | 35 +++---- spec/Spec/Courseware/Export.lean | 2 +- spec/Spec/Courseware/Export/Artifact.lean | 21 ++-- spec/Spec/Courseware/Export/Render.lean | 107 ++++++++++---------- spec/Spec/Courseware/Model.lean | 4 +- spec/Spec/Courseware/Model/Element.lean | 17 ++-- spec/Spec/Courseware/Model/Info.lean | 48 +++++---- spec/Spec/Courseware/Model/Lesson.lean | 8 +- spec/Spec/Courseware/Model/Primitives.lean | 36 +++---- spec/Spec/Courseware/Model/RichContent.lean | 47 ++++----- spec/Spec/Courseware/Open.lean | 6 +- spec/Spec/Courseware/Open/Course.lean | 12 +-- spec/Spec/Courseware/Open/QuestionBank.lean | 12 +-- spec/Spec/Prelude.lean | 19 ++-- spec/Spec/System.lean | 20 ++-- spec/Spec/System/Audit.lean | 22 ---- spec/Spec/System/Lock.lean | 29 +++--- spec/Spec/System/Permission.lean | 61 ++--------- spec/Spec/System/Run.lean | 34 +++---- 24 files changed, 381 insertions(+), 455 deletions(-) delete mode 100644 spec/Spec/System/Audit.lean diff --git a/README.md b/README.md index c72ae67..d0991dc 100644 --- a/README.md +++ b/README.md @@ -1,74 +1,74 @@ # curriculum-project-hub -教研生产的数字化解决方案。核心思路:课程像 DAW / 剪辑软件那样有一个**结构化的工程文件**;coding agent 协助编辑它;一个 rule-based checker(类编译器)校验其合法性并给出 helpful fix hint。目标是把教研从一次性的文档,沉淀成**可累积、可校验、可复用的资产**。 +教研生产的数字化解决方案。核心思路:课程像 DAW / 剪辑软件那样有一个结构化的工程文件; +LLM assistant 协助编辑它;一个 rule-based checker 校验其合法性并给出有用的诊断。 -这是一个 **monorepo**。它的组织方式本身就表达了一条原则:**`spec/` 是上游的语义母本,其余部件是向它对齐的实现。** +LLM 提效,但判不了一节课合不合法(它不能真去跑 typst、不能可靠地断言数据合不合 +schema);checker 真跑工具、给确定性诊断,补上这块。两者一起才是完整闭环。目标是把教研 +从一次性的文档,变成可累积、可校验、可复用的资产。 -## 安装 `cph` 命令行 +这是一个 monorepo。组织方式本身就表达了一条原则:`spec/` 是上游的语义母本,其余部件是 +向它对齐的实现。 -当前版本 **0.0.2**。从源码安装(本仓库根目录): +## 安装 `cph` + +从源码安装(本仓库根目录): ```sh cargo install --path crates/cph-cli --locked ``` -`render` 包已嵌入二进制(build.rs 编译期拷入 + `include_dir!`),所以装好后**无需任何环境变量、不依赖源码树**即可用。渲染包按版本解压到 per-user cache(`~/.cache/cph/render-/` 或 macOS `~/Library/Caches/cph/...`);开发时可设 `CPH_RENDER_DIR` 指向 live `render/` 目录覆盖。 +`render` 包已嵌入二进制,装好后无需任何环境变量、不依赖源码树即可用。开发时可设 +`CPH_RENDER_DIR` 指向 live `render/` 目录覆盖。 ```sh -cph --version # cph 0.0.2 -cph check <工程目录> # 校验合法性(7 类诊断) +cph check <工程目录> # 校验合法性 cph build <工程目录> --target student -o build/student.pdf # 渲讲义 PDF +cph completions zsh > ~/.zfunc/_cph # shell 补全(可选) ``` -**版本契约(ADR-0016):** 教研工程文件根放一个 `.cph-version` 文件,内容为它面向的 cph 版本(如 `0.0.2`)。`cph` 加载时比对自身版本,不相容则报 `E-CPH-VERSION` error 并拒绝(当前判定为版本完全相等;后续可放宽为 semver 区间,只改一处谓词)。`examples/` 与本仓 fixture 已带该文件作为迁移起点;缺文件的工程暂时跳过此检查(OPEN)。 - -Shell 补全(可选): - -```sh -cph completions zsh > ~/.zfunc/_cph # 或 bash/fish/powershell/elvish -``` +工程文件根放一个 `.cph-version` 文件,声明它面向的 cph 版本;`cph` 加载时比对自身版本, +不相容则拒绝(版本契约,ADR-0016)。 ## 仓库布局 -``` -README.md ← 本文件:总览 + 宪法(下面 5 条) -CLAUDE.md ← 全局 agent 操作手册(管整个 repo) -docs/adr/ ← 系统级架构决策记录(跨部件,被 spec 契约引用) -spec/ ← Lean 语义母本(自包含的 Lean 工程)。见 spec/README.md -Cargo.toml ← 仓库级 cargo workspace(实现部件共用,便于跨部件复用 crate) -crates/ ← 实现:rule-based checker(向 spec 对齐)。见 crates/README.md - cph-diag / cph-model / cph-schema / cph-typst ← 可复用基础(模型/校验/typst 引擎) - cph-check / cph-cli ← checker 本体 + `cph` 命令行 -render/ ← typst 渲染包 cph-render(母本的渲染后端之一,ADR-0005) -examples/ ← 样例工程文件(如 TH-141),流水线的真实输入 -(hub/ exporter/ …) ← 将来的其他部件,平级于 spec/。尚未创建 -``` +`spec/` 是 Lean 语义母本(自包含 Lean 工程,见 `spec/README.md`);`crates/` 是实现 +(rule-based checker,向 spec 对齐,见 `crates/README.md`);`render/` 是 typst 渲染包; +`examples/` 是样例工程文件;`docs/adr/` 是架构决策记录,被 spec 引用。 -`spec/` 与实现部件**物理分离、平级共存**:谁是上游、谁向谁对齐,一眼可见。 -实现部件共用一个仓库根的 cargo workspace,使基础 crate(模型、typst 引擎)能被 -未来部件(如 exporter)复用,而非各自重造。 +`spec/` 与实现部件物理分离、平级共存:谁是上游、谁向谁对齐,一眼可见。实现部件共用一个 +仓库根的 cargo workspace,使基础 crate 能被未来部件复用。 ## 宪法 这 5 条是 `spec/` 这份语义母本的定位与约束,是本仓库一切工作的前提。 -1. **角色 —— Lean 是研发侧的上游参照。** - `spec/` 用 Lean 编写,是开发者(领域专家)与 coding agent **共用**的 spec 工具,用来沉淀产品各部件的**语义**。它**不进入产品运行时**——产品里"站在 Lean 这个位置"的那个 checker 用什么技术实现,尚未决定;但那个东西的语义,先在 `spec/` 里固定下来。 +1. **角色——Lean 是研发侧的上游参照。** + `spec/` 用 Lean 写,是开发者和 coding assistant 共用的 spec 工具,用来沉淀产品各部件 + 的语义。它不进产品运行时——运行时那个 checker 用什么技术实现还没定,但它的语义先在 + `spec/` 里固定下来。 -2. **对齐机制 —— Lean 只做上游参照。** - 不做 extract / codegen,不派生 conformance test,CI 里**没有** spec→实现的 gate。实现对齐 spec,由"开发者 review + agent 巡逻 diff"这个人肉环节承载。 - (CI 里的 `spec check` 只验 spec **自身**能否 type-check,即契约内部良构,不是 spec↔实现的对齐检查。) +2. **对齐机制——Lean 只做上游参照。** + 不做 extract / codegen,不派生 conformance test,CI 里没有 spec→实现的 gate。实现对齐 + spec,靠开发者 review 和 agent 巡逻 diff 这个人肉环节承载。(CI 里的 spec check 只验 + spec 自身能否 type-check,即契约内部良构,不是 spec↔实现对齐检查。) -3. **资产性 —— 由 review 纪律承载,无机器兜底。** - 这份仓库给你的是"精确、自洽、机器验内部良构的语义共识",**不是**"实现正确性保证"。spec 与实现之间那道缝,是我们自愿用人来守的——清醒地守,它就是资产;放任实现漂移而不回头同步,它就退化成最贵的过期文档。 +3. **资产性——由核对纪律承载,无机器兜底。** + 这份仓库给的是精确、自洽、机器验过内部良构的语义共识,不是实现正确性的保证。spec 与 + 实现是否一致,没有自动闸门,要靠人工或 coding assistant 不定期(或每次改动后)核对; + 坚持核对,它就是有用的参照,否则只会变成过期的文档。 -4. **形态 —— 它是人机共识的契约。** - 契约必须**自包含**:凡契约未明文规定的,开发者与 agent 双方都不该假设。这比"文档"严格——type checker 会逼这份契约在结构上无洞。 +4. **形态——它是人机共识的契约。** + 契约必须自包含:凡契约未明文规定的,开发者与 agent 双方都不该假设。这比"文档"严格—— + type checker 会逼这份契约在结构上无洞。 -5. **深度判据 —— 只收录分歧点。** - 一条语义该不该写进 Lean,取决于一句话:**"不写明,开发者与 agent 会不会各自做出不同假设?"** 会 → 进契约;显然的东西 / 纯 plumbing / 普通 CRUD 字段 → 不进(写进去只稀释信噪比、增加维护面)。 - 深度上限不是 Lean 的表达力,而是**你愿意在每次实现变更时手动回头同步的量**——写得比你能维护的更深,多出来的部分会率先过期、反过来误导实现。 +5. **深度判据——只收录分歧点。** + 一条语义该不该写进 Lean,取决于一句话:不写明,开发者与 agent 会不会各自做出不同 + 假设?会,就进契约;显然的东西、纯基础设施、普通 CRUD 字段,不进(写进去只稀释信噪比、 + 增加维护面)。深度上限不是 Lean 的表达力,而是你愿意在每次实现变更时手动回头同步的量。 + 进了之后钉到多细,见 `spec/README.md` 的取舍判据。 ## CI -`.gitea/workflows/spec-check.yml` 在每次 push / PR 时于 `spec/` 下跑 `lake build`,确保契约始终 type-check 通过(从第一天起就是"绿"的)。这是良构 gate,见宪法第 2 条。 +每次 push / PR 在 `spec/` 下跑 `lake build`,确保契约始终 type-check 通过。这是良构 gate, +见宪法第 2 条。 diff --git a/spec/README.md b/spec/README.md index 851b345..f8508e3 100644 --- a/spec/README.md +++ b/spec/README.md @@ -1,55 +1,74 @@ -# spec —— Lean 语义母本 +# spec —— 语义契约 -这是本 monorepo 的**契约**:产品各部件语义的上游参照,用 Lean 编写。它的定位与约束见仓库根 `README.md` 的"宪法"5 条——本文件只讲**怎么往这份契约里写东西**。 +## 这个项目在解决什么 -## 现状 +教研产出现在是一摞一次性的文档:写完就躺着,改一次要同步很多地方,没法校验、 +没法复用、没法追溯。这个项目想把教研产出变成可校验、可复用、能派生多种成品 +(讲义、教案、课件、归档)的工程化文件。 -刚初始化的 Lean 工程(`lake init`),目前只有占位内容(`Spec/Basic.lean`)。实质领域内容(System 平台层、Courseware 产品层)将逐个概念加入,每个都遵循下面的规范。 +但光有工程文件还不够。它要变成一个能卖钱的产品,还得: -## 构建 +- 工程文件这种形式,正好适合现在大热的 LLM assistant 来改,从而提效; +- 但 LLM 判不了一节课合不合法(它不能真去跑 typst 编译器、不能可靠地断言数据合不合 + schema),所以产品里还有一个 rule-based checker:它真跑工具、给确定性的诊断,补上 + LLM 判不了的这块。LLM 提效 + checker 兜底,两者一起才是完整的产品闭环。 +- 加上一些提升体验的小功能:飞书/企业微信集成、自动化提醒之类; +- 如果要做 SaaS,还要有基本的管理概念:权限、LLM API 的配置和用量、费用等。 -```sh -cd spec -lake build -``` +工程文件是起点,不是终点。 -工具链锁定在 `lean-toolchain`(`leanprover/lean4:v4.31.0`)。无外部依赖——Mathlib / Batteries 等留待第一个真正需要它的定理出现时再引入(依赖碰到再加)。 +## spec 是什么 -## 写作规范 +spec/ 是产品语义的契约,用 Lean 写。它定义产品各部件"是什么意思"。 -### 双半契约:prose + type +- 它是开发者和 coding assistant 共同的语义依据:两边对某个东西的理解,以这里为准。 +- 它不进产品运行时。运行时真正做校验的那个东西用什么技术实现,还没定;但它的语义, + 先在这里固定下来。 +- 它精确、自洽,机器能校验它内部结构没有漏洞。它不保证实现一定符合它—— + 实现和它是否一致,没有自动检查,要靠人工或 coding assistant 不定期(或每次改动后)核对。 -每个 top-level 声明**必须**带 `/-- … -/` doc 注释,用自然语言陈述其语义意图。两半缺一不可: +## 人机怎么一起干活 -- **prose 半**给人读——说清"这在领域里是什么、为什么"。 -- **type 半**给机器读、给 type checker 把关——保证结构无洞。 +- 凭语义,不凭经验。这个领域新,coding assistant 在这里没有可靠的既有经验, + 所以语义以 spec 的注释为准,不要凭训练先验臆测。 +- 契约没写的,就是不存在的。遇到没定的点,提出来让开发者定,不要替它选答案。 +- 改了实现或 spec 之后,两边是否还对得上,要核对一下;这一致性没有自动闸门。 -agent 不得用预训练先验脑补本领域(领域很新,无先验);prose 是 agent 理解语义的唯一权威来源。 +## 怎么往 spec 里写 -### 标签分类法 +### 一条东西要不要进 spec -在 doc 注释里用以下标签标注每条语义的状态: +不写它,开发者和 coding assistant 会不会各自做出不同假设?会,就进;不会 +(显然的事、纯基础设施、普通 CRUD 字段),就不进。 -- **`PINNED`** —— 已解决的分歧点,契约在此处权威,双方据此对齐。 -- **`OPEN`** —— 故意未规定。双方均**不得假设**其解;实现遇到时必须 surface 出来讨论,而不是擅自决定。 -- **`ADR-NNNN`** —— 链接到根 `docs/adr/` 下的对应决策记录(如 `ADR-0002`),交代该语义的决策出处。 +### 进了之后,钉到多细 -### 分歧点测试(写之前先过一遍) +- 现在想清楚的,用 Lean 固定(声明、类型、关系)。 +- 没想清楚的,两三句话 prose 占位,标 `OPEN`。等讨论或业务反馈后再细化, + 细化结果可以再用 Lean 固定。 +- 不在 Lean 里验证实现真的做了这些事。spec 只讲"要做什么、判什么";实现有没有真做, + 不形式化证明。 +- 形式化定理:不用写;写了不是坏事,但现在很少有能写的定理。定理本身得是产品语义, + 不是"实现该满足的性质"。 -新增任何概念前,先问:**"不写明,开发者与 agent 会不会各自做出不同假设?"** +### 写的时候 -- 会 → 它是分歧点,入契约。 -- 不会(显然的东西 / 纯 plumbing / 普通 CRUD 字段)→ 不入。 - -详见根 README 宪法第 5 条。 - -### 不用 `sorry` - -无法陈述清楚的东西,用 `OPEN` 在 prose 里标注,而**不是**用 `sorry` 留一个假装成立的定理。`sorry` 会让 `lake build` 仍然变绿,却在契约里埋一个谎——这与"契约自包含、无洞"直接冲突。 +- 每个顶层声明要带 doc 注释,用 `/-- ... -/` 写自然语言,说清这在领域里是什么、为什么。 + 注释是语义的依据,Lean 类型保证结构,两者缺一不可。 +- 在注释里标这条语义的状态: + - `PINNED`:已定,契约在此处权威。 + - `OPEN`:故意没定。不要假设它的解,遇到要提出来讨论。 + - `ADR-NNNN`:指向 `docs/adr/` 下的决策记录。 +- 不用 `sorry`。没想清楚的,用 `OPEN` 标在注释里,不要用 `sorry` 假装成立—— + 那会让构建通过,却在契约里埋一个谎。 +- 不复述文件系统上能直接看到的东西(目录结构、文件名)。文件系统应当自描述,文档讲 context。 +- 不写变更史(进 git/ADR)。不搬 ADR 内部黑话,要表达就直说。 + 不为设计选择辩护("刻意用 X 而非 Y"),只说是什么。 +- "为什么"的背景考据(如某工具的内部机制)不进 spec,指向 ADR;但产品行为和设计模式要钉。 ### 命名 -- **模块 / 命名空间**:PascalCase,对应分层,如 `Spec.System.Run`、`Spec.Courseware.Validity`。 -- **类型**:PascalCase。 -- **谓词 / `Prop`**:用意图清晰的命名,如 `Legal…`、`ValidTransition`、`Can…`。 -- **文件粒度**:原则上"一个带独立不变式的概念一个文件"。 +- 模块/命名空间:PascalCase,按分层,如 `Spec.System.Run`。 +- 类型:PascalCase。 +- 谓词(`Prop`):用意图清楚的词,如 `Legal…`、`ValidTransition`、`Can…`。 +- 文件粒度:一个带独立不变式的概念一个文件。 diff --git a/spec/Spec/Courseware.lean b/spec/Spec/Courseware.lean index 684b20f..f7c53f6 100644 --- a/spec/Spec/Courseware.lean +++ b/spec/Spec/Courseware.lean @@ -6,16 +6,5 @@ import Spec.Courseware.Open /-! # Courseware —— 产品层契约(课程工程文件) -护城河:课程"工程文件"的语义母本与合法性规则。决策出处 ADR-0005..0016。按四组组织: - -- **`Model`** —— 工程文件的内容模型:基元 `Primitives`、富内容 `RichContent`、原子 - 单位 `Element`、单节课 `Lesson`(element 的有序序列)。 -- **`Export`** —— export target = artifact + 有序 typed steps:产物 ADT `Artifact` - (`singleFile` / `fileTree`),build 规格 `TargetSpec`(artifact + steps + 覆盖声明 - `covers`)与 `RenderConfig`。 -- **`Check`** —— checker 语义:`Severity` + 6 类诊断 + **合法 lesson = 无 error 级 - 诊断**(模型外设施诊断以抽象谓词 + `Oracle` 表示);检查管线的 5 阶段、序、compile - 门控。 -- **`Open`** —— 留白骨架(核心关系 OPEN,已 surface 不臆造):题库 `QuestionBank`、 - 课程编排 `Course`。 +课程"工程文件"的语义母本与合法性规则。决策出处 ADR-0005..0016。 -/ diff --git a/spec/Spec/Courseware/Check.lean b/spec/Spec/Courseware/Check.lean index b326f16..e82114b 100644 --- a/spec/Spec/Courseware/Check.lean +++ b/spec/Spec/Courseware/Check.lean @@ -2,7 +2,7 @@ import Spec.Courseware.Check.Diagnostic import Spec.Courseware.Check.Pipeline /-! -# Courseware.Check —— checker 语义 +# Courseware.Check —— 产品 checker 语义 诊断分类与合法 lesson(`Diagnostic`)、检查管线的阶段与序(`Pipeline`)。决策出处 ADR-0010。 diff --git a/spec/Spec/Courseware/Check/Diagnostic.lean b/spec/Spec/Courseware/Check/Diagnostic.lean index 60885cd..1685cae 100644 --- a/spec/Spec/Courseware/Check/Diagnostic.lean +++ b/spec/Spec/Courseware/Check/Diagnostic.lean @@ -2,30 +2,39 @@ import Spec.Courseware.Model.Lesson import Spec.Courseware.Export.Render /-! -# Diagnostic —— checker 诊断:分类、严重级别、合法 lesson +# Diagnostic —— 产品 checker 的诊断 -产品里"站在 Lean 位置"的 rule-based checker,语义在此沉淀(ADR-0010,经 ADR-0012 -修订)。它对 lesson 提诊断,每条有**分类**(`DiagKind`)与**严重级别**(`Severity`)。 -本模块:钉级别类型(二分);钉 7 类诊断各自的含义与级别,并把"**合法 lesson = 无 -error 级诊断**"建成判定(ADR-0005 deferred 的"完整合法判定"的回填);对**模型外设施** -型诊断(typst 编过否、数据合 schema 否)用**抽象谓词 + `Oracle` 实现边界**表示——契约 -说"存在这条诊断、什么意思、什么级别",真值由实现提供,不在 Lean 内计算(不内嵌 typst -编译器)。引用解析(`@ref`、相对 import)不另设诊断:它们都是 typst 编译期失败,归 -`typstCompile`(ADR-0012)。版本契约诊断 `cphVersionMismatch`(ADR-0016)是第 7 类。 +这个 codebase 是要拿去卖的产品。LLM 辅助操作提效是它的核心卖点之一——但 LLM 判不了 +一节课合不合法:它不能真的去跑 typst 编译器、不能可靠地断言一段数据合不合 schema、 +也不能可靠地检查文件齐不齐。所以产品里有一个 rule-based checker 来做这件事:它真跑 +工具、给确定性的诊断,补上 LLM 判不了的这块。这个 checker 的语义在这里(ADR-0010, +经 ADR-0012、ADR-0016 修订)。它对 lesson 提诊断,每条有一个分类(`DiagKind`)和一 +个严重级别(`Severity`)。 + +注意区分两个"检查":这里的 checker 是**产品功能**——用户把教研工程文件喂给 `cph`, +检查这个工程文件合不合法。它和"开发时 spec 与实现是否一致"是两回事,后者没有自动 +闸门,靠核对。 + +本模块钉三件事:严重级别二分;7 类诊断各自的含义和级别;"合法 lesson = 无 error 级 +诊断"这条判定。其中有些诊断是 LLM 判不了、得 checker 真跑工具才能判的(typst 编不编 +得过、数据合不合 schema、content 文件齐不齐)——这些用抽象谓词加 `Oracle` 表示:契约 +说"存在这条诊断、什么意思、什么级别",真值由 checker 给(契约不在 Lean 里内嵌 typst +编译器去算)。引用解析(`@ref`、相对 import)不单列:它们都是 typst 编译期失败,归 +`typstCompile`(ADR-0012)。版本契约 `cphVersionMismatch`(ADR-0016)是第 7 类。 -/ namespace Spec.Courseware -/-- 诊断严重级别(`PINNED` 二分, ADR-0005)。`error` 阻断(产物不合法),`warning` 不 -阻断(产物仍可导出,只是有损)。更细级别(info/hint)未决策,故只二分。 -/ +/-- 诊断严重级别(ADR-0005)。`error` 阻断(产物不合法),`warning` 不阻断(产物仍可导出, + 只是有损)。更细级别(info/hint)未决策,故只二分。 -/ inductive Severity where | warning | error -/-- 诊断**分类**(`PINNED` 7 类, ADR-0010,经 ADR-0012 修订为 6 类,经 ADR-0016 增至 7 -类)。按"谁来判定"分三层:**结构型**(模型自身可判):`partPathMissing`/`unknownKind`/ -`cphVersionMismatch`;**schema/外部设施型**(靠实现 oracle): -`missingContentFile`/`schemaViolation`/`typstCompile`;**语义型**:`renderIgnored`。 -/ +/-- 诊断分类(ADR-0010,经 ADR-0012 折并为 6 类、ADR-0016 增至 7 类)。按 checker 怎么判分三层: + 结构型(checker 自己按结构判):`partPathMissing`/`unknownKind`/`cphVersionMismatch`; + schema/外部工具型(得真跑工具):`missingContentFile`/`schemaViolation`/`typstCompile`; + 语义型:`renderIgnored`。 -/ inductive DiagKind where /-- manifest 的 part 指向不存在的文件夹(或经 `..` 逃出根)。结构型。 -/ | partPathMissing @@ -36,21 +45,19 @@ inductive DiagKind where /-- 实例数据不合其 kind 的 JSON Schema;亦作 manifest/element.toml 畸形的兜底。 -/ | schemaViolation /-- 拼装出的 typst 源编译失败:语法错、未解析的交叉引用 `@ref`、越界或缺失的相对 - `import`/`include`(后两者即旧 `danglingReference` 的两种情形——typst 在编译期 - 检出,故归此类,ADR-0012)。外部设施型。 -/ + `import`/`include`。后两者 typst 在编译期检出,故归此类(ADR-0012)。外部工具型。 -/ | typstCompile /-- 某被用到的 kind 在某声明的 target 下无渲染规则,该 element 被忽略。语义型。 -/ | renderIgnored - /-- 工程文件的 `.cph-version` 与 CLI(cph)版本不相容(ADR-0016)。**结构型**(加载期 - 判)。工程文件根的 `.cph-version` 声明它所面向的 cph 版本;CLI 加载时按**兼容性判 - 定**比对自身版本(实现侧 `CARGO_PKG_VERSION`),不相容即产此类。**当前判定为版本 - 完全相等才相容**(MVP;后续可放宽为 semver 区间,判定逻辑可逐步修改而不动本分类)。 - `error` 级——版本不相容的工程文件不应被该 CLI 处理。 -/ + /-- 工程文件的 `.cph-version` 与 CLI(cph)版本不相容(ADR-0016)。结构型(加载期判)。 + 工程文件根的 `.cph-version` 声明它所面向的 cph 版本;CLI 加载时比对自身版本,不相容 + 即产此类。当前判定为版本完全相等才相容(MVP;后续可放宽为 semver 区间,判定逻辑可 + 逐步改而不动本分类)。`error` 级——版本不相容的工程文件不应被该 CLI 处理。 -/ | cphVersionMismatch -/-- 每类诊断的**严重级别**(`PINNED`, ADR-0010)。六类 `error`(阻断);**唯 -`renderIgnored` 为 `warning`**——ADR-0005 种子规则"缺渲染 ⇒ warning,不阻断导出"。 -钉成全函数使"哪类阻断"成为可引用、可对齐的事实(实现侧 `DiagCode` 级别据此对齐)。 -/ +/-- 每类诊断的严重级别(ADR-0010)。六类 `error`(阻断);唯 `renderIgnored` 为 `warning` + ——ADR-0005 种子规则"缺渲染 ⇒ warning,不阻断导出"。钉成全函数使"哪类阻断"成为可 + 引用、可对齐的事实。 -/ def DiagKind.severity : DiagKind → Severity | .partPathMissing => .error | .unknownKind => .error @@ -60,46 +67,51 @@ def DiagKind.severity : DiagKind → Severity | .renderIgnored => .warning | .cphVersionMismatch => .error -/-- 缺渲染诊断的级别 = **warning**(`PINNED`, ADR-0005/0010,**非 error**)。具名常量, -使"它是 warning"可被实现侧 grep 对齐(实现里同名常量 `RENDER_IGNORED_SEVERITY` 引用 -本定义)。等价于 `DiagKind.renderIgnored.severity`。 -/ +/-- 缺渲染诊断的级别 = warning(ADR-0005/0010,非 error)。具名常量,使"它是 warning" + 可被实现 grep 对齐(实现里同名常量 `RENDER_IGNORED_SEVERITY` 引用本定义)。 + 等价于 `DiagKind.renderIgnored.severity`。 -/ def renderIgnoredSeverity : Severity := DiagKind.renderIgnored.severity variable (P : Primitives) -/-- **缺渲染诊断**:lesson 在 target `t` 下存在无法渲染的 element(`PINNED`, -ADR-0005/0009)。成立 ⟺ 存在某 element,其 kind 在 `t` 下 `covers` 为假。语义型诊断, -级别 warning。 -/ +/-- 缺渲染诊断:lesson 在 target `t` 下存在无法渲染的 element(ADR-0005/0009)。成立 ⟺ + 存在某 element,其 kind 在 `t` 下 `covers` 为假。语义型诊断,级别 warning。 -/ def renderIgnored (l : Lesson P) (c : RenderConfig P) (t : P.TargetId) : Prop := ∃ e ∈ l, ¬ c.covers e.kind t /-! -## 模型外设施型诊断:抽象谓词 + 实现边界(ADR-0010) +## 要真跑工具才能判的诊断:抽象谓词 + Oracle -`typstCompile`/`schemaViolation`(的 schema-合规面)断言的是模型自身无法判定的事实—— -要跑 typst 编译器、schema 校验器。契约把它们建成**抽象谓词**,真值由实现提供的 oracle -给出。下面用 `Oracle` 收口这些判定:它不是要在 Lean 里实现 checker,而是把"这些事实 -来自模型外"显式化、类型化。 +诊断分两类(按 checker 怎么判):有些 checker 自己按工程文件结构就能判(part 路径 +在不在、kind 知不知道、某 kind 在某 target 下有没有被覆盖);有些 checker 自己也判 +不了,得真跑外部工具——typst 编不编得过(要跑 typst 编译器)、数据合不合 schema(要 +跑 schema 校验器)、content 文件齐不齐(要看磁盘)。后者就是 `Oracle` 收口的。 + +`Oracle` 把这些"得 checker 委托外部工具才能判"的事实建成抽象谓词,真值由 checker 给。 +它不是要在 Lean 里实现 checker,而是把"这几件事 checker 自己算不了、得委托出去"显式 +表达、类型化。它只收 Legal 需要的、得委托外部工具的事实;checker 自己能判的(如 +`renderIgnored`)不进 Oracle。 + +(这两类 checker 都判得了;但 LLM 两类都判不了——这正是产品里要有个 rule-based +checker 的理由,见本模块顶部。) -/ -/-- **实现侧判定 oracle**(`PINNED` 实现边界, ADR-0010)。每个字段是一个谓词,真值由 -实现(checker)提供。结构型诊断(part 路径、未知 kind)不入此 oracle——那些模型自身可判。 -/ +/-- checker 委托外部工具才能判的那些事实(ADR-0010)。每个字段是一个谓词,真值由 + checker 提供。checker 自己按结构就能判的诊断(part 路径、未知 kind)不入此 oracle。 -/ structure Oracle (l : Lesson P) (c : RenderConfig P) where - /-- target `t` 下拼装源可编译(否 ⇒ `typstCompile`)。**含引用解析**:源能编译即蕴含 - 其 `@ref`、相对 import 全部解析(ADR-0012 已把引用诊断并入 `typstCompile`)。 -/ + /-- target `t` 下拼装源可编译(否 ⇒ `typstCompile`)。含引用解析:源能编译即蕴含其 + `@ref`、相对 import 全部解析(ADR-0012)。 -/ compiles : P.TargetId → Prop /-- 每个 element 数据合 schema(否 ⇒ `schemaViolation`)。 -/ dataConforms : Prop /-- schema 要求的 content 文件齐备(否 ⇒ `missingContentFile`)。 -/ contentFilesPresent : Prop -/-- **合法 lesson**(`PINNED`, ADR-0010;回填 ADR-0005 deferred 的"完整合法判定")。 - -合法 ⟺ 检查管线产出**零条 error 级诊断**。展开为:模型外设施判定(经 `Oracle`)全为真, -**且**每个声明的 target 都编译通过。结构型诊断由 `cph-model` 在加载期判定;能走到这步 -谈合法性意味着已加载成功,故此处聚焦 schema/外部设施层。引用解析不单列——已被 -`compiles` 蕴含(ADR-0012)。`renderIgnored` 是 warning,**不**进合取——ADR-0005 种子 -规则的体现。`targets` 用全称式表达以不绑定 `TargetId` 的可枚举性。 -/ +/-- 合法 lesson(ADR-0010)。合法 ⟺ 检查管线产出零条 error 级诊断。展开为:得委托外部 + 工具的判定(经 `Oracle`)全为真,且每个声明的 target 都编译通过。checker 自己按结构 + 能判的诊断(part 路径、未知 kind)在加载期已判;能走到这步谈合法性意味着那些已过, + 故此处聚焦 schema/外部工具层。`renderIgnored` 是 warning,不进合取(ADR-0005 种子 + 规则)。`targets` 用全称式表达以不绑定 `TargetId` 的可枚举性。 -/ def Legal (l : Lesson P) (c : RenderConfig P) (o : Oracle P l c) : Prop := o.dataConforms ∧ o.contentFilesPresent ∧ (∀ t : P.TargetId, (c.spec t).isSome → o.compiles t) diff --git a/spec/Spec/Courseware/Check/Pipeline.lean b/spec/Spec/Courseware/Check/Pipeline.lean index fa9beaf..35c184b 100644 --- a/spec/Spec/Courseware/Check/Pipeline.lean +++ b/spec/Spec/Courseware/Check/Pipeline.lean @@ -1,26 +1,24 @@ import Spec.Courseware.Check.Diagnostic /-! -# Pipeline —— checker 检查管线的阶段与序(ADR-0010) +# Pipeline —— 检查管线的阶段与序 -checker 的 `check` 按**固定顺序**跑五个阶段,逐阶段收集诊断;`compile` 阶段有**门控**。 -顺序与门控是契约——它决定用户看到哪些诊断(藏在缺文件背后的语法错,在文件补齐前不 -显示,这是有意的)。每阶段的**算法**不进 Lean(宪法第 5 条深度上限):只钉**阶段、序、 -门控**。阶段对应上游模块:`load`←`cph-model`;`structural`←part 路径/未知 kind; -`schema`←`cph-schema`;`compile`←`cph-typst`(模型外设施);`coverage`←`renderIgnored`。 +checker 的 `check` 按固定顺序跑五个阶段,逐阶段收集诊断;`compile` 阶段有门控。顺序和 +门控是契约——它决定用户看到哪些诊断(藏在缺文件背后的语法错,在文件补齐前不显示,这是 +有意的)。每阶段的算法不进 Lean(宪法第 5 条深度上限):只钉阶段、序、门控。 -/ namespace Spec.Courseware -/-- 检查管线的**阶段**(`PINNED` 5 阶段, ADR-0010)。 +/-- 检查管线的阶段(ADR-0010)。 -- `load` —— 解析 manifest + 各 element.toml。**含 `.cph-version` 兼容性判定** - (ADR-0016:工程根 `.cph-version` 与 CLI 版本不相容 ⇒ `cphVersionMismatch` error)。 - 硬失败(无法解析 lesson)则**停**整条管线。 +- `load` —— 解析 manifest + 各 element.toml。含 `.cph-version` 兼容性判定(ADR-0016: + 工程根 `.cph-version` 与 CLI 版本不相容 ⇒ `cphVersionMismatch` error)。硬失败(无法 + 解析 lesson)则停整条管线。 - `structural` —— part 路径存在、无 `..`、kind 已知且一致。此处判缺的 part 后续跳过。 - `schema` —— 每个"存在且 kind 已知"的 part 按其 kind schema 校验。 -- `compile` —— 模型外设施阶段(typst 编译)。**门控:仅当前序零 error 才跑**。 -- `coverage` —— 语义型 warning(`renderIgnored`);**不**受门控,总跑。 -/ +- `compile` —— 跑外部工具的阶段(typst 编译)。门控:仅当前序零 error 才跑。 +- `coverage` —— 语义型 warning(`renderIgnored`);不受门控,总跑。 -/ inductive Phase where | load | structural @@ -29,8 +27,8 @@ inductive Phase where | coverage deriving DecidableEq -/-- 管线阶段的**执行序**(`PINNED`, ADR-0010)。`order p` 越小越先跑。序是契约: -`compile`(3)排在 `structural`(1)/`schema`(2)之后,正因前者门控于后者无 error。 -/ +/-- 管线阶段的执行序(ADR-0010)。`order p` 越小越先跑。序是契约:`compile`(3)排在 + `structural`(1)/`schema`(2)之后,正因前者门控于后者无 error。 -/ def Phase.order : Phase → Nat | .load => 0 | .structural => 1 @@ -38,15 +36,14 @@ def Phase.order : Phase → Nat | .compile => 3 | .coverage => 4 -/-- 某阶段是否**受"前序零 error"门控**(`PINNED`, ADR-0010)。唯 `compile` 受门控:藏在 -结构/schema 错背后的编译错,在前者修好前不显示——有意降噪。 -/ +/-- 某阶段是否受"前序零 error"门控(ADR-0010)。唯 `compile` 受门控:藏在结构/schema 错 + 背后的编译错,在前者修好前不显示——有意降噪。 -/ def Phase.gated : Phase → Bool | .compile => true | _ => false -/-- 管线在 `load` 硬失败时**停**(`PINNED`, ADR-0010)。`load` 拿不到可解析 lesson 时, -无 lesson 可喂下游,整条管线终止——唯一会截断后续所有阶段的情形(区别于 `compile` -门控只跳过自己)。 -/ +/-- 管线在 `load` 硬失败时停(ADR-0010)。`load` 拿不到可解析 lesson 时,无 lesson 可喂 + 下游,整条管线终止——唯一会截断后续所有阶段的情形(区别于 `compile` 门控只跳过自己)。 -/ def Phase.haltsPipelineOnFailure : Phase → Bool | .load => true | _ => false diff --git a/spec/Spec/Courseware/Export.lean b/spec/Spec/Courseware/Export.lean index 7788bd6..6585043 100644 --- a/spec/Spec/Courseware/Export.lean +++ b/spec/Spec/Courseware/Export.lean @@ -4,5 +4,5 @@ import Spec.Courseware.Export.Render /-! # Courseware.Export —— export target = artifact + 有序 typed steps -产物 ADT(`Artifact`)、build 规格与渲染覆盖(`Render`)。决策出处 ADR-0009 / 0011。 +产物 ADT、build 规格与渲染覆盖。决策出处 ADR-0009 / 0011。 -/ diff --git a/spec/Spec/Courseware/Export/Artifact.lean b/spec/Spec/Courseware/Export/Artifact.lean index 4e202a6..e4a49e2 100644 --- a/spec/Spec/Courseware/Export/Artifact.lean +++ b/spec/Spec/Courseware/Export/Artifact.lean @@ -1,23 +1,22 @@ /-! -# Artifact —— export target 的产物(ADR-0009 / 0011) +# Artifact —— export target 的产物 -ADR-0009:一个 export target 是**一次 build**,产出一个**有类型的产物**。ADR-0011 -钉死:产物是**带字段的 ADT**——"产物到底指什么"(单文件落在哪 / 一棵树产出哪些文件) -是不好猜的领域语义,必须写进字段 + doc,而非抹成两个空构造子。路径/glob 用 `String` -承载并由 doc 赋义(它们就是文本),不复刻文件系统类型。 +一个 export target 是一次 build,产出一个有类型的产物(ADR-0009、ADR-0011)。产物是 +带字段的 ADT:"产物到底指什么"(单文件落在哪 / 一棵树产出哪些文件)是不好猜的领域 +语义,要写进字段 + doc,而不是抹成两个空构造子。路径、glob 用 `String` 承载并由 doc +赋义(它们就是文本),不复刻文件系统类型。 -/ namespace Spec.Courseware -/-- export 产物(`PINNED` 带字段 ADT, ADR-0011)。产物形状决定 `cph build` 吐文件还是 -目录、reduce 怎么折叠(`singleFile` 把有序片段拼成一份再编译——交叉引用 `@ref`、例题 -计数器能工作的前提;`fileTree` 每 part 落一文件)。后端/格式仍 OPEN(ADR-0009)。 -/ +/-- export 产物(ADR-0011)。产物形状决定 `cph build` 吐文件还是目录、reduce 怎么折叠 + (`singleFile` 把有序片段拼成一份再编译——交叉引用 `@ref`、例题计数器能工作的 + 前提;`fileTree` 每 part 落一文件)。后端、格式仍 OPEN(ADR-0009)。 -/ inductive Artifact where /-- 单文件产物,落在 `filepath`(相对工程根)。讲义/教案 PDF 即此。 -/ | singleFile (filepath : String) - /-- 多文件产物:`root` 目录下匹配 `outputs` **glob** 的文件集(第三方平台 archive - 即此)。用 glob 而非显式清单:轻,又让消费方/checker 知道该产出哪些文件、可校验 - 完整性。 -/ + /-- 多文件产物:`root` 目录下匹配 `outputs` glob 的文件集(第三方平台归档即此)。 + 用 glob 而非显式清单:轻,又让消费方/checker 知道该产出哪些文件、可校验完整性。 -/ | fileTree (root : String) (outputs : String) end Spec.Courseware diff --git a/spec/Spec/Courseware/Export/Render.lean b/spec/Spec/Courseware/Export/Render.lean index ed71d5c..7291e52 100644 --- a/spec/Spec/Courseware/Export/Render.lean +++ b/spec/Spec/Courseware/Export/Render.lean @@ -2,88 +2,89 @@ import Spec.Courseware.Model.Primitives import Spec.Courseware.Export.Artifact /-! -# Render —— export target = artifact + 有序 typed steps(ADR-0009 / 0011) +# Render —— export target = artifact + 有序 typed steps -ADR-0009:export target 是一次 build,产出一个有类型的 `Artifact`。ADR-0011 钉死 build -的**形状**:一个 target 是 `artifact` + 一串**有序 typed step**。 +一个 export target 是一次 build,产出一个有类型的 `Artifact`(ADR-0009)。build 的形状 +是:一个 target = `artifact` + 一串有序的 typed step(ADR-0011)。 -- `typstCompile template` —— 把**模板文件**(如 `exports/student.typ`)编译成产物。它是 - *typed* 而非裸 shell,正因框架要把 **manifest 注入**模板(经 `--input manifest=…`), - 裸字符串表达不了这个 wiring。presentation(编号、样式)住模板里,不在 manifest。 -- `shell run` —— 逃生口,给难以声明的步骤(ADR-0005 的 (b) 类 medium-only)。 -- `assembleMarkdown field` —— 按 parts 顺序把每个 element 的 `field`(markdown content 叶子, - ADR-0015)拼成**单文件 markdown** 产物。typed 而非 `cat`,因为按 manifest `[[parts]]` 顺序读取 + - 跳过缺失项 + 写到单文件产物路径这件事,框架 own 比裸 shell 稳。 +- `typstCompile template` —— 把模板文件(如 `exports/student.typ`)编译成产物。它是 + typed 而非裸 shell,因为框架要把 manifest 注入模板(经 `--input manifest=…`),裸 + 字符串表达不了这个 wiring。presentation(编号、样式)住模板里,不在 manifest。 +- `shell run` —— 逃生口,给难以声明的步骤。 +- `assembleMarkdown field` —— 按 parts 顺序把每个 element 的 `field`(markdown content + 叶子,ADR-0015)拼成单文件 markdown 产物。typed 而非裸 `cat`:按 manifest `[[parts]]` + 顺序读取 + 跳过缺失项 + 写到单文件产物路径,框架自己来比裸 shell 稳。 -**渲染覆盖**:ADR-0011 废止了 per-target `RenderRule` 载荷——渲染的"how"已移进模板。 -契约只保留覆盖声明 `covers`(该 target 渲染哪些 kind),供种子诊断用。 +渲染覆盖:契约只保留覆盖声明 `covers`(该 target 渲染哪些 kind),供种子诊断用;渲染的 +"how"住模板里(ADR-0011)。 -**shell step 的执行语义(ADR-0013)。** `shell` 不再只是占位:它**会被执行**,语义是把 -`run` 交给平台 shell、以**工程根为工作目录**运行,产物由被调外部工具自己写出(框架不装配 -内容)。三条边界是真分歧点,故钉契约: -1. **opt-in by construction** —— 任意命令执行只在用户**显式** build 一个 shell target 时发生, - 绝不在 `check` 里跑。`check` 只校验结构(lesson 是否合法),不执行外部工具、不验其产物。 -2. **失败归属** —— shell step 退出非零是一次 **build-过程失败**,不是 lesson 的合法性缺陷; - 因此它**不**进 `Diagnostic` 的 6 类(那 6 类是 lesson 自身的诊断,见 `Check/Diagnostic.lean`), - 而由 build 执行层报告。诊断分类保持 6 类不变(ADR-0013 显式拒绝新增 `ShellStep` 诊断码)。 -3. **非-typst target 不过 typst 编译** —— 一个只含 `shell` step 的 target(教具包即此)由 +shell step 的执行语义(ADR-0013):`shell` 会被执行,语义是把 `run` 交给平台 shell、以 +工程根为工作目录运行,产物由被调外部工具自己写出(框架不装配内容)。三条边界: + +1. opt-in:命令执行只在用户显式 build 一个 shell target 时发生,绝不在 `check` 里跑。 + `check` 只校验结构,不执行外部工具、不验其产物。 +2. 失败归属:shell step 退出非零是一次 build 过程失败,不是 lesson 的合法性缺陷;因此 + 它不进 `Diagnostic` 的 7 类(那 7 类是 lesson 自身的诊断,见 `Check/Diagnostic.lean`), + 而由 build 执行层报告。诊断分类保持 7 类不变。 +3. 非-typst target 不过 typst 编译:一个只含 `shell` step 的 target(教具包即此)由 执行器跑命令,而非走 typst 引擎;`check` 的 compile 阶段跳过它。 -**assembleMarkdown step 的执行语义(ADR-0015)。** 与 `shell` 同属"非-typst target":框架 own -读取每个 element 的 `.md`、按 `[[parts]]` 顺序拼接、写到单文件产物路径(产物是 markdown, -不经 typst 引擎)。同 shell 的三条边界:① 只在显式 `build --target` 跑,`check` 不跑;② 装配失败 -(如写盘失败、引用图缺失)是 build-过程错误,不入 6 类诊断;③ 非-typst target,`check` 的 compile -阶段跳过它。**单文件产物**(现):装配器注入课程级标题为文档 h1(课程元数据,非 element 内容), -每份 `slides.md`/`transcript.md` 贡献其 `##` part 与 `###` 小节(presentation 在内容里, ADR-0011), -按 `[[parts]]` 顺序拼接(分隔符空行)。**自包含**:装配器扫描产物里的 `![](rel)` 图引用,把引用到的 -本地图从工程根按原相对路径复制进产物所在 build 根,使该 build 目录可独立交付;引用图在工程根缺失属 -build-过程错误(不入 6 类)。外部 URL(`http(s)://`/`data:`)不复制。结构化 FileTree 产物延后 -(待 parts 树形重组, ADR-0015 OPEN)。 +assembleMarkdown step 的执行语义(ADR-0015):与 `shell` 同属"非-typst target"。框架 +自己读每个 element 的 `.md`、按 `[[parts]]` 顺序拼接、写到单文件产物路径(产物 +是 markdown,不经 typst 引擎)。同 shell 的三条边界:① 只在显式 `build --target` 跑, +`check` 不跑;② 装配失败(如写盘失败、引用图缺失)是 build 过程错误,不入 7 类诊断; +③ 非-typst target,`check` 的 compile 阶段跳过它。 + +单文件产物(现):装配器注入课程级标题为文档 h1(课程元数据,非 element 内容),每份 +`slides.md`/`transcript.md` 贡献其 `##` part 与 `###` 小节(presentation 在内容里, +ADR-0011),按 `[[parts]]` 顺序拼接(分隔符空行)。自包含:装配器扫描产物里的 `![](rel)` +图引用,把引用到的本地图从工程根按原相对路径复制进产物所在 build 根,使该 build 目录 +可独立交付;引用图在工程根缺失属 build 过程错误(不入 7 类)。外部 URL(`http(s)://`、 +`data:`)不复制。结构化 FileTree 产物延后(待 parts 树形重组,ADR-0015 OPEN)。 -/ namespace Spec.Courseware variable (P : Primitives) -/-- 一个 build **step**(`PINNED` typed, ADR-0011;可扩展)。MVP 仅一个 `typstCompile`; -`steps` 是 list 因为 FileTree / 第三方 build 会需多步。刻意不把模板内部、shell 命令的 -解析结构写进来(实现细节, ADR-0011 OPEN)。 -/ +/-- 一个 build step(ADR-0011;可扩展)。MVP 仅一个 `typstCompile`;`steps` 是 list 因为 + FileTree、第三方 build 会需多步。不把模板内部、shell 命令的解析结构写进来(实现细节, + ADR-0011 OPEN)。 -/ inductive Step where /-- 编译模板文件 `template`(相对工程根)成产物;框架注入 manifest。typed 的理由: 注入这件事裸 shell 写不出。 -/ | typstCompile (template : String) - /-- shell 逃生口:执行命令 `run`(ADR-0005 (b) 类落这)。**已实现**(ADR-0013):以工程根 - 为 cwd 执行,opt-in(只在显式 build 该 target 时跑,`check` 不跑),失败属 build-过程错误 - 而非 lesson 诊断。教具包(如 KenKen 交互 HTML 由外部 `kendoku` 生成)即走此 step。 -/ + /-- shell 逃生口:执行命令 `run`(ADR-0013)。以工程根为 cwd 执行,opt-in(只在显式 + build 该 target 时跑,`check` 不跑),失败属 build 过程错误而非 lesson 诊断。 + 教具包(如 KenKen 交互 HTML 由外部 `kendoku` 生成)即走此 step。 -/ | shell (run : String) /-- 装配 markdown:按 `[[parts]]` 顺序读取每个 element 的 `field`(markdown content 叶子, - ADR-0015),注入课程 h1 后拼接成**单文件 markdown** 产物,并收集 `![](rel)` 引用的本地图进 - build 根使产物自包含。typed 而非 `cat`:按序读取+跳过缺失+注入标题+写盘+收集图由框架 own。 - **已实现**(ADR-0015):非-typst target(`check` 不跑,失败属 build-过程错误不入 6 类诊断)。 - slides 大纲面 / 逐字稿口播面即走此 step(直接 markdown+KaTeX 撰写,绕开 typst→md 公式转换, - ADR-0014 R2)。 -/ + ADR-0015),注入课程 h1 后拼接成单文件 markdown 产物,并收集 `![](rel)` 引用的本地图 + 进 build 根使产物自包含。typed 而非 `cat`:按序读取+跳过缺失+注入标题+写盘+收集图由 + 框架自己来。非-typst target(`check` 不跑,失败属 build 过程错误不入 7 类诊断)。 + slides 大纲、逐字稿口播即走此 step(直接 markdown+KaTeX 撰写,绕开 typst→md 公式转换, + ADR-0014)。 -/ | assembleMarkdown (field : String) -/-- 一个 export target 的 build 规格(`PINNED` artifact + 有序 steps, ADR-0011)。 -/ +/-- 一个 export target 的 build 规格(ADR-0011:artifact + 有序 steps)。 -/ structure TargetSpec where - /-- 产物(带字段, ADR-0011)。决定 build 折叠成单文件还是文件树。 -/ + /-- 产物(带字段,ADR-0011)。决定 build 折叠成单文件还是文件树。 -/ artifact : Artifact - /-- **有序** build steps。按序执行;MVP 仅一个 `typstCompile`。 -/ + /-- 有序 build steps。按序执行;MVP 仅一个 `typstCompile`。 -/ steps : List Step - /-- **覆盖声明**:`covers k` 表示此 target 渲染 kind `k`。ADR-0011 把旧 - `renders : KindId → Option RenderRule` 降级后的产物——契约只声明"渲染哪些 kind" - (种子诊断 `renderIgnored` 用),"how"由 `steps` 的模板实现。 -/ + /-- 覆盖声明:`covers k` 表示此 target 渲染 kind `k`。契约只声明"渲染哪些 kind" + (种子诊断 `renderIgnored` 用),"how"由 `steps` 的模板实现(ADR-0011)。 -/ covers : P.KindId → Prop -/-- 渲染配置(`PINNED` target-中心, ADR-0009/0011)。`spec t = none` 表示 target `t` -未声明(不导出);`some s` 给出其 build 规格。 -/ +/-- 渲染配置(ADR-0009/0011)。`spec t = none` 表示 target `t` 未声明(不导出); + `some s` 给出其 build 规格。 -/ structure RenderConfig where /-- target ↦ 该 target 的 build 规格(未声明则 `none`)。 -/ spec : P.TargetId → Option (TargetSpec P) -/-- kind `k` 在 target `t` 下**被渲染**(`PINNED`, ADR-0009/0011;承接 ADR-0005)。成立 -⟺ `t` 已声明(`spec t = some s`)**且** `s.covers k`。为假即"此 kind 在此 target 下不 -被渲染"——checker 据此报 warning(见 `Diagnostic.renderIgnored`)。`P` 隐式以便点记法。 -/ +/-- kind `k` 在 target `t` 下被渲染(ADR-0009/0011)。成立 ⟺ `t` 已声明 + (`spec t = some s`)且 `s.covers k`。为假即"此 kind 在此 target 下不被渲染"—— + checker 据此报 warning(见 `Diagnostic.renderIgnored`)。 -/ def RenderConfig.covers {P : Primitives} (c : RenderConfig P) (k : P.KindId) (t : P.TargetId) : Prop := match c.spec t with diff --git a/spec/Spec/Courseware/Model.lean b/spec/Spec/Courseware/Model.lean index 31df449..ed5062c 100644 --- a/spec/Spec/Courseware/Model.lean +++ b/spec/Spec/Courseware/Model.lean @@ -7,7 +7,5 @@ import Spec.Courseware.Model.Info /-! # Courseware.Model —— 工程文件的内容模型 -留白基元(`Primitives`)、富内容锚点(`RichContent`)、原子单位(`Element`)、单节课 -(`Lesson`)、课时元信息(`Info`:canonical author 为列表 vs `RawInfo` 撰写态)。 -决策出处 ADR-0005 / 0006 / 0008。 +基元、富内容、element、lesson、课时元信息。决策出处 ADR-0005 / 0006 / 0008。 -/ diff --git a/spec/Spec/Courseware/Model/Element.lean b/spec/Spec/Courseware/Model/Element.lean index 19bc8ac..b73e665 100644 --- a/spec/Spec/Courseware/Model/Element.lean +++ b/spec/Spec/Courseware/Model/Element.lean @@ -1,24 +1,23 @@ import Spec.Courseware.Model.Primitives /-! -# Element —— 课程内容的原子单位 +# Element —— 课程内容的最小单位 -ADR-0005:element 实例 = 一个 kind 标签 + 符合该 kind schema 的数据。本模块把它编码成 -依赖结构,使"数据必须匹配其 kind"成为类型层面的事实而非运行时校验。 +一个 element = 一个 kind 标签 + 符合该 kind schema 的数据(ADR-0005)。 +用依赖结构编码,使"数据必须匹配 kind"成为类型层面的事实,不是运行时校验。 -/ namespace Spec.Courseware variable (P : Primitives) -/-- element 实例(`PINNED`, ADR-0005)。`data : P.ElementData kind` 由 `kind` 决定—— -无法构造数据与 kind 不符的 element,schema 合规由类型系统保证。ADR-0005 的 (a) 类 -字段(逐字稿、重点圈划)落在具体 kind 的 `ElementData` 内,不出现在此通用结构上; -交互教具等"重型 kind"在此与例题、定理同构,仅 `kind` 不同,重实现在模型之外。 -/ +/-- 一个 element 实例(ADR-0005)。data 的类型由 kind 决定,所以没法造出数据和 kind + 不符的 element——schema 合规由类型保证。逐字稿、重点圈划这类跟具体 kind 强相关 + 的字段,落在该 kind 的 ElementData 里,不放在这个通用结构上。 -/ structure Element where - /-- 该 element 的 kind。 -/ + /-- 这个 element 的 kind。 -/ kind : P.KindId - /-- 符合 `kind` schema 的数据(类型随 `kind` 而变)。 -/ + /-- 符合 kind schema 的数据,类型随 kind 变。 -/ data : P.ElementData kind end Spec.Courseware diff --git a/spec/Spec/Courseware/Model/Info.lean b/spec/Spec/Courseware/Model/Info.lean index c900220..e28aaed 100644 --- a/spec/Spec/Courseware/Model/Info.lean +++ b/spec/Spec/Courseware/Model/Info.lean @@ -1,56 +1,54 @@ /-! -# Info —— 课时元信息:canonical 模型 vs 撰写态(authoring surface) +# Info —— 课时元信息:canonical 模型 vs 撰写态 -`[info]`(标题、作者)大多是 passthrough 元数据(ADR-0008),本不入契约。但**作者的 -基数**是一个真分歧点:一节课可由多人(教研组)署名,故 canonical 模型里 author 是一个 -**有序列表**,不是单值或可选单值。 +`[info]`(标题、作者)大多是 passthrough 元数据(ADR-0008),本不入契约。但作者的 +基数是一个真分歧点:一节课可由多人(教研组)署名,故 canonical 模型里 author 是一个 +有序列表,不是单值或可选单值。 -另有一条值得钉的模式:on-disk 的**撰写态**(用户实际填写的形态)是**语法糖**——单作者可写 -`author = "…"`,多作者写 `author = ["…", "…"]`——但这个"字符串或数组"的二态**只活在加载 -边界**:`RawInfo` 经归一化折叠成 canonical `Info`,其后不再出现。canonical 接收端始终是 -`List String`,raw 形式不泄漏进模型其余部分。这正是 `Info`(canonical)与 `RawInfo` -(撰写态)两个结构存在的理由。 +另有一条值得钉的模式:on-disk 的撰写态(用户实际填写的形态)是语法糖——单作者可写 +`author = "…"`,多作者写 `author = ["…", "…"]`——但这个"字符串或数组"的二态只活在 +加载边界:`RawInfo` 经归一化折叠成 canonical `Info`,其后不再出现。canonical 接收端 +始终是 `List String`,raw 形式不泄漏进模型其余部分。这正是 `Info`(canonical)与 +`RawInfo`(撰写态)两个结构存在的理由。 -/ namespace Spec.Courseware -/-- 作者的**撰写态形式**(`PINNED` 仅填写便利, ADR-0008)。on-disk 单作者可写裸 -字符串、多作者写数组——填写便利,非语义分歧。此 union **只活在加载边界**,经 -`RawAuthor.normalize` 折叠后不再出现。 -/ +/-- 作者的撰写态形式(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`"。 -/ +/-- raw 作者归一化为有序作者列表(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 在此**已**是列表,不再是 -"字符串或数组"。 -/ +/-- 课时元信息的 canonical 模型(ADR-0008)。`authors` 是有序列表:多人署名第一类, + 空列表 = 未署名。`title` 等其余字段是 passthrough 元数据,不在此承诺更多。这是系统 + 其余部分唯一所见的形态——author 在此已是列表,不再是"字符串或数组"。 -/ structure Info where /-- 标题(passthrough 元数据)。 -/ title : String - /-- 作者**有序列表**(空 = 未署名)。canonical 始终是列表。 -/ + /-- 作者有序列表(空 = 未署名)。canonical 始终是列表。 -/ authors : List String -/-- 撰写态的 `[info]`(`PINNED` 仅填写便利, ADR-0008)。`author` 用 `RawAuthor` -(字符串或数组),`author` 缺省即未署名。此结构刻画"为便于填写而存在的 raw 形态", -**不**是模型其余部分流通的形式——它经 `RawInfo.toInfo` 归一化为 canonical `Info`。 -/ +/-- 撰写态的 `[info]`(ADR-0008)。`author` 用 `RawAuthor`(字符串或数组),缺省即未署名。 + 此结构刻画"为便于填写而存在的 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`。 -/ +/-- raw `[info]` 归一化为 canonical `Info`(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 [] } diff --git a/spec/Spec/Courseware/Model/Lesson.lean b/spec/Spec/Courseware/Model/Lesson.lean index 3a3145d..7704d01 100644 --- a/spec/Spec/Courseware/Model/Lesson.lean +++ b/spec/Spec/Courseware/Model/Lesson.lean @@ -3,14 +3,14 @@ import Spec.Courseware.Model.Element /-! # Lesson —— 单节课工程文件 -ADR-0005:一个工程文件 = 一节课,是 element 实例的**有序序列**。课程/单元不是工程 -文件,而是 lesson 的编排(见 `Spec.Courseware.Course`,OPEN)。 +一个工程文件 = 一节课,是 element 实例的有序序列(ADR-0005)。课程、单元不是工程文件, +而是 lesson 的编排(见 `Spec.Courseware.Course`,OPEN)。 -/ namespace Spec.Courseware -/-- 一节课(`PINNED`, ADR-0005)。用 `List` 因为 **element 次序承载教学语义**(先讲 -定义再举例 ≠ 反过来);**不建模时长**——ADR-0005 决定 lesson 是内容编排而非时间轴。 -/ +/-- 一节课(ADR-0005)。用 `List` 因为 element 的次序承载教学语义(先讲定义再举例, ≠ 反过来)。 + 不建模时长——lesson 是内容编排,不是时间轴(ADR-0005)。 -/ abbrev Lesson (P : Primitives) := List (Element P) end Spec.Courseware diff --git a/spec/Spec/Courseware/Model/Primitives.lean b/spec/Spec/Courseware/Model/Primitives.lean index 656ae8b..2df6103 100644 --- a/spec/Spec/Courseware/Model/Primitives.lean +++ b/spec/Spec/Courseware/Model/Primitives.lean @@ -1,34 +1,26 @@ /-! -# Primitives —— Courseware 契约的留白基元 +# 基元 -课程工程文件模型(ADR-0005)依赖一组基元:element kind 怎么标识、某 kind 的数据 -schema 是什么、export target 怎么标识。收口成载体 `Primitives`,让模型在其上参数化 -——契约谈得了 element / lesson / 渲染**之间的关系**,而把每个基元的**内部表示**留给 -实现。注意:某基元语义已 PINNED(如 schema 形态由 ADR-0006 钉死)与其表示进 Lean -是两回事——JSON Schema / typst 的内部结构属实现细节,不入 Lean,故基元在此仍以抽象 -类型承载。富内容的 prose 母本见 `Courseware.RichContent`。 +课程模型要谈"element、lesson、target 之间的关系",但每个基元本身(element kind +怎么标识、kind 的数据 schema 长什么样、target 怎么标识)的内部表示是实现的事。 +这里把它们收成一组抽象基元,让模型在它们之上参数化。 + +契约只钉基元之间的关系;基元内部用什么表示,留给实现。 -/ namespace Spec.Courseware -/-- Courseware 契约基元载体(关系 `PINNED`, ADR-0005;各基元表示留给实现, ADR-0006)。 -/ +/-- 课程模型的一组抽象基元:关系已定,内部表示留给实现(ADR-0005、ADR-0006)。 -/ structure Primitives where - /-- element kind 标识(`PINNED` **开放宇宙**, ADR-0005;表示 `OPEN`)。刻意用抽象 - 类型而非 `inductive`:ADR-0005 决定 kind 是开放可扩展宇宙(stdlib + 第三方), - 封闭枚举会违背它——此处开放是**已决策的**(区别于 `RunState` 的"尚未封闭")。 -/ + /-- element kind 的标识。kind 是开放宇宙:stdlib 加第三方都可加,不是封闭枚举 + (ADR-0005)。表示方式留给实现。 -/ KindId : Type - /-- 某 kind 的合法数据类型(`PINNED` 依赖关系, ADR-0005;schema 形态 `PINNED` - ADR-0006,表示仍抽象)。以 kind 为索引:`ElementData k` 即"符合 `k` schema 的 - 数据"。schema 形态(声明式 JSON Schema + `content` 叶子 = typst 源)是 ADR-0006 - 钉死的,但属 JSON/typst 内部结构、实现细节,不进 Lean;契约只锚定"数据符合 - kind schema"这条关系,故此处仍是抽象类型。 -/ + /-- 某 kind 的合法数据类型,以 kind 为索引:`ElementData k` 就是"符合 k 的 schema + 的数据"。schema 用声明式 JSON Schema,带 content 叶子(ADR-0006);JSON Schema + 的内部结构是实现细节,不进契约,契约只钉"数据要符合 kind 的 schema"这条关系。 -/ ElementData : KindId → Type - /-- export target 标识(`PINNED` 角色, ADR-0005;表示 `OPEN`)。一个 target 是一次 - build,产出对 lesson 的一种投影(讲义/教案/PPT/平台 archive…),见 `Render`。 -/ + /-- export target 的标识。一个 target 是一次 build,产出对 lesson 的一种投影 + (讲义、教案、PPT、平台归档等),见 Render。 -/ TargetId : 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/Model/RichContent.lean b/spec/Spec/Courseware/Model/RichContent.lean index d1a8899..9f27140 100644 --- a/spec/Spec/Courseware/Model/RichContent.lean +++ b/spec/Spec/Courseware/Model/RichContent.lean @@ -1,44 +1,41 @@ /-! -# RichContent —— 富内容(ADR-0006 的 prose 母本) +# 富内容 -ADR-0006:element schema 的"叶子"可以是 `content` 类型,其值是一段**源文本**, -按其 **format** 决定语义(ADR-0015)。两种 format: -- **typst** —— 一段 typst 源,语义取该源作为 module 求值后的 body content(讲义/教案面)。 -- **markdown** —— 一段**原样**的 markdown + KaTeX 源,**不经 typst 求值**(slides 大纲面 / 逐字稿口播面; - ADR-0015)。直接以 markdown 撰写**绕开** typst→markdown 的公式转换难题(ADR-0014 R2):公式一开始就是 - KaTeX 源(`$…$`),没有"把 typst 公式转成 md"这一步。 +element schema 的叶子可以是 content 类型:一段源文本,按 format 决定语义 +(ADR-0006、ADR-0015)。 -关键约束(均 ADR-0006,源自 typst 源码事实):**typst** format 的富内容**不可无主**——typst 的源必须有 -`FileId`,否则 span 脱锚、相对 import 报"cannot access file system from here"。故每段 typst 富内容是 World 里 -的一等文件,坐落在一个**虚拟路径**上;相对 import 限本工程路径结构内 + `@package`(不跨工程)。markdown format -的富内容不参与 typst 求值,但同样由一个虚拟路径定位(供 markdown 装配 step 按序读取,见 `Export/Render`)。 +两种 format: -本模块只立 prose 锚点 + 最小抽象签名:typst 的 `Content`/`Module` 内部结构、JSON Schema 形状、format 的 -具体判别属实现细节,不进 Lean,只承诺"富内容由一个虚拟路径定位"+"叶子带 format"这两条关系。 +- typst:一段 typst 源,求值后得到讲义/教案用的内容。 +- markdown:一段 markdown + KaTeX 源,原样保留,不经 typst 求值(slides 大纲、 + 逐字稿口播)。直接用 markdown 写,公式一开始就是 KaTeX(`$…$`),绕开了 + typst→markdown 的公式转换这个难题(ADR-0014)。 + +约束:typst 内容必须挂在一个虚拟路径上(原因见 ADR-0006 的考据)。markdown 内容 +不经 typst 求值,但同样用虚拟路径定位,供 markdown 装配按序读取。 + +本模块只钉两条关系:富内容由一个虚拟路径定位、叶子带 format。typst 的 Content/Module +内部结构、JSON Schema 形状、format 怎么判别,都是实现细节,不进契约。 -/ namespace Spec.Courseware -/-- 富内容在工程文件路径结构中的**虚拟路径**(`OPEN` 表示, ADR-0006)。把一段富内容 -定位为 World 里的一等文件(span 可解析、相对 import 可锚定)。落盘后即真实相对路径 -(ADR-0007),不在本层承诺,故 opaque。 -/ +/-- 富内容在工程文件里的虚拟路径(ADR-0006)。落盘后是真实相对路径(ADR-0007), + 这层不承诺,所以 opaque。 -/ opaque VPath : Type -/-- 富内容的 **format**(`PINNED`, ADR-0015)。`content` 叶子带 format:typst 叶子被 typst 求值; -markdown 叶子原样保留(markdown+KaTeX 源,不经求值)。 -/ +/-- 富内容的 format(ADR-0015)。 -/ inductive ContentFormat where - /-- typst 源:求值为 typst `Content`(讲义/教案面)。 -/ + /-- typst 源:求值后得到讲义/教案用的内容。 -/ | typst - /-- markdown + KaTeX 源:原样保留,不经 typst 求值(slides 大纲面 / 逐字稿口播面;ADR-0015)。 -/ + /-- markdown + KaTeX 源:原样保留,不经 typst 求值(slides、逐字稿)。 -/ | markdown -/-- 对一段富内容的**引用**:它坐落在某个虚拟路径上(`PINNED` 关系, ADR-0006),并带一个 -**format**(`PINNED`, ADR-0015)。刻意**不**建模源文本、不建模求值出的 `Content`(那是实现侧的事); -只钉"富内容经由一个 `VPath` 定位 + 带 format",作为 `Primitives.ElementData` 里 `content` 叶子的语义锚点。 -/ +/-- 对一段富内容的引用:它挂在一个虚拟路径上(ADR-0006),带一个 format(ADR-0015)。 + 不建模源文本,也不建模求值出的内容——那是实现的事;这里只钉"富内容由虚拟路径定位 + + 带 format",作为 ElementData 里 content 叶子的语义锚点。 -/ structure RichContentRef where - /-- 该富内容所在的虚拟路径(ADR-0006;落盘后为真实相对路径, ADR-0007)。 -/ vpath : VPath - /-- 该富内容的 format(ADR-0015)。 -/ format : ContentFormat end Spec.Courseware diff --git a/spec/Spec/Courseware/Open.lean b/spec/Spec/Courseware/Open.lean index d5f8fcb..121261d 100644 --- a/spec/Spec/Courseware/Open.lean +++ b/spec/Spec/Courseware/Open.lean @@ -2,8 +2,8 @@ import Spec.Courseware.Open.QuestionBank import Spec.Courseware.Open.Course /-! -# Courseware.Open —— 留白骨架(核心关系 OPEN) +# Courseware.Open —— 留白骨架 -题库与 element 的关系(`QuestionBank`)、课程编排规则(`Course`)。两者均为已 surface -但未决策的分歧点,按宪法第 2 条不臆造,待专门 ADR 落定。 +题库与 element 的关系(`QuestionBank`)、课程编排规则(`Course`)。两者都是已提出但 +未决策的分歧点,不臆造,待专门 ADR 落定。 -/ diff --git a/spec/Spec/Courseware/Open/Course.lean b/spec/Spec/Courseware/Open/Course.lean index 50617a4..48826f5 100644 --- a/spec/Spec/Courseware/Open/Course.lean +++ b/spec/Spec/Courseware/Open/Course.lean @@ -1,10 +1,10 @@ /-! -# Course —— 课程编排(骨架,规则 OPEN) +# Course —— 课程编排(OPEN) -ADR-0005:工程文件的粒度是**单节课**;course / 单元**不是**工程文件,而是 lesson 的 -**编排**。但"编排"的具体规则未决策:有序列表还是带层级(单元 → 课)的树?lesson 被 -引用还是被包含?跨 lesson 有无约束(目标覆盖、前后置)?这些都是 `OPEN`。 +工程文件的粒度是单节课(ADR-0005);course / 单元不是工程文件,而是 lesson 的编排。 +但"编排"的具体规则没定:有序列表,还是带层级(单元 → 课)的树?lesson 被引用还是被 +包含?跨 lesson 有无约束(目标覆盖、前后置)?这些都 OPEN。 -按宪法第 2 条本模块**不臆造**编排结构——不建 `Course := List Lesson`(那会偷偷承诺 -"扁平有序、无层级")。只在此 surface:课程编排待专门 ADR。本文件当前不引入任何承诺性声明。 +不臆造编排结构——不建 `Course := List Lesson`(那会偷偷承诺"扁平有序、无层级")。课程 +编排待专门 ADR。本文件不引入任何承诺性声明。 -/ diff --git a/spec/Spec/Courseware/Open/QuestionBank.lean b/spec/Spec/Courseware/Open/QuestionBank.lean index 7270d8d..6bbac70 100644 --- a/spec/Spec/Courseware/Open/QuestionBank.lean +++ b/spec/Spec/Courseware/Open/QuestionBank.lean @@ -1,10 +1,10 @@ /-! -# QuestionBank —— 题库(骨架,核心关系 OPEN) +# QuestionBank —— 题库(OPEN) -题库是与工程文件并列的资产(类比 DAW 的 sample library):有自身结构的实体,又是最 -典型的可复用单元,lesson 会引用它。但**题库与 element 的关系尚未决策**,且用户明确 -指出"纯引用可能不够"——element 内联题目数据 / lesson 持指向题库条目的引用 / 两者并存? +题库是与工程文件并列的资产:有自身结构的实体,又是最典型的可复用单元,lesson 会引用它。 +但题库与 element 的关系没定,用户也指出"纯引用可能不够"——element 内联题目数据?lesson +持指向题库条目的引用?两者并存? -这是一个 `OPEN` 分歧点。按宪法第 2 条本模块**不替它选解**——不建 `QuestionRef` 也不建 -内联结构,只在此 surface。待专门 ADR 落定后再填。本文件当前不引入任何承诺性声明。 +这是 OPEN 分歧点。不替它选解——不建 `QuestionRef` 也不建内联结构,只在此提出。待专门 +ADR 落定后再填。本文件不引入任何承诺性声明。 -/ diff --git a/spec/Spec/Prelude.lean b/spec/Spec/Prelude.lean index df99553..9e2832c 100644 --- a/spec/Spec/Prelude.lean +++ b/spec/Spec/Prelude.lean @@ -1,24 +1,23 @@ /-! # Prelude —— System 层共享标识符 -平台层反复引用一组标识符(项目、run、session、principal)。其内部表示从未被决策 -(UUID / 复合键、principal 子类型学),也非分歧点,故收口成 opaque 载体 -`Identifiers`,System 各模块在其上参数化——契约谈得了"锁 owner 是哪个 run"这类 -**关系**,却不对标识符表示作承诺。 +平台层反复引用一组标识符(项目、run、session、principal)。它们的内部表示从未被决策 +(UUID / 复合键、principal 的子类型学),也不是分歧点,所以收成 opaque 载体 +`Identifiers`,System 各模块在它之上参数化——契约谈得了"锁 owner 是哪个 run"这类关系, +不对标识符表示作承诺。 -/ namespace Spec.System -/-- System 层标识符载体(关系结构 `PINNED`;各字段表示 `OPEN`)。 -/ +/-- System 层标识符载体:关系已定,各字段表示 OPEN。 -/ structure Identifiers where - /-- 课程项目标识(`OPEN` 表示;聚合根,likec4 `Project`)。 -/ + /-- 课程项目标识(聚合根;表示 OPEN)。 -/ ProjectId : Type - /-- 一次 Claude 任务的标识(`OPEN` 表示;锁的 owner、审计主体,`AgentRun`)。 -/ + /-- 一次 Claude 任务的标识(锁的 owner、审计主体;表示 OPEN)。 -/ RunId : Type - /-- 长生命周期 Claude 会话标识(`OPEN` 表示;跨多 run 复用,ADR-0002)。 -/ + /-- 长生命周期 Claude 会话标识(跨多 run 复用,ADR-0002;表示 OPEN)。 -/ SessionId : Type - /-- 权限主体标识(`OPEN` 表示及其子类型学;ADR-0004 的 user/chat/department/… - 子类型学未定且非本层分歧点,纯 plumbing,故只留 opaque 键)。 -/ + /-- 权限主体标识(表示 OPEN)。 -/ Principal : Type end Spec.System diff --git a/spec/Spec/System.lean b/spec/Spec/System.lean index d1ae702..fe0a1b1 100644 --- a/spec/Spec/System.lean +++ b/spec/Spec/System.lean @@ -1,19 +1,21 @@ import Spec.System.Run import Spec.System.Lock import Spec.System.Permission -import Spec.System.Audit /-! # System —— Hub 平台层契约 -协作与执行的平台:项目、飞书群、AgentRun、锁、权限、审计。likec4 -(`docs/architecture/likec4/`)已画出这一层的**结构**;本层只补 likec4 画不出的 -**语义分歧点**: +这一层是产品里的协作与执行平台:项目、飞书群、AgentRun、锁、权限、审计。决策出处 +ADR-0001..0004。 -- `Run` —— AgentRun 状态与终止判定(状态集合完整性 OPEN)。 -- `Lock` —— 锁 owner=run(ADR-0002),及"持锁者必为非终止 run"的核心不变式。 -- `Permission` —— read⊂edit⊂manage 角色格、能力推导、单调性;force-release 在格外。 -- `Audit` —— 有意从简(内容多为 plumbing,OPEN)。 +现状:Hub 还没建、没有业务反馈,所以这一层多为 OPEN 占位,只钉少数已定且有语义分量的 +东西(锁 owner = run、持锁者必为非终止 run、角色三级)。其余等 Hub 真建起来、业务反馈 +来了再细化。做 SaaS 要的权限、LLM API 配置和用量、费用等管理概念,将来也落在这层。 -标识符见 `Spec.Prelude`。决策出处:ADR-0001..0004。 +- `Run` —— AgentRun 的终止判定(状态集合 OPEN)。 +- `Lock` —— 锁 owner = run(ADR-0002),及"持锁者必为非终止 run"的核心不变式。 +- `Permission` —— read ⊂ edit ⊂ manage 角色三级;force-release 在格外。 +- 审计以 run 为主体记录其生命周期事件;审计记录里装什么未定(OPEN)。 + +标识符见 `Spec.Prelude`。 -/ diff --git a/spec/Spec/System/Audit.lean b/spec/Spec/System/Audit.lean deleted file mode 100644 index 114d4d1..0000000 --- a/spec/Spec/System/Audit.lean +++ /dev/null @@ -1,22 +0,0 @@ -import Spec.Prelude - -/-! -# Audit —— 审计日志(有意从简) - -likec4 把 `AuditLog` 列为实体(`AgentRun -> AuditLog 'records lifecycle events'`), -但**审计记录里装什么**(事件 schema、保留策略、可查询维度)在任何 ADR / 散文里都 -未决策,且大多是 plumbing——按分歧点测试不入契约。故本模块刻意几乎为空:只固定 -"审计以 run 为主体记录其生命周期事件"这一条已决策关系,其余 `OPEN`(留白本身是 -契约的一部分:承诺此处尚无答案、勿填)。 --/ - -namespace Spec.System - -/-- 审计条目的最小骨架(关系 `PINNED` / 内容 `OPEN`, likec4)。只承诺"一条审计记录 -关联到某个 run";事件类型、时间、actor、详情等字段 `OPEN`,待真实分歧点出现时由 -对应 ADR 落定。 -/ -structure AuditEntry (I : Identifiers) where - /-- 该审计条目所属的 run(`PINNED` 关系, likec4)。 -/ - run : I.RunId - -end Spec.System diff --git a/spec/Spec/System/Lock.lean b/spec/Spec/System/Lock.lean index 94a0e22..121626b 100644 --- a/spec/Spec/System/Lock.lean +++ b/spec/Spec/System/Lock.lean @@ -4,34 +4,29 @@ import Spec.System.Run /-! # Lock —— 项目锁与排他不变式 -ADR-0002 的核心:防止并发 Claude 同改一个项目,锁的 **owner 是当前 `AgentRun`** -(不是 teacher / chat / session)。本模块把这条决策编码进类型,并钉死那条 -likec4 画不出的语义不变式——**持锁者必为非终止 run**。 +ADR-0002 的核心:防止并发 Claude 同改一个项目,锁的 owner 是当前 AgentRun(不是 +teacher / chat / session)。这条编码进类型,并钉住核心不变式:持锁者必为非终止 run。 -/ namespace Spec.System variable (I : Identifiers) -/-- 项目级锁(`PINNED`, ADR-0002)。`owner : RunId`(非 SessionId/Principal)从类型 -上编码"lock owner = run_id":锁不可能被 session / teacher 持有。 -/ +/-- 项目级锁(ADR-0002)。`owner : RunId`(非 SessionId/Principal)从类型上编码 + "lock owner = run":锁不可能被 session / teacher 持有。 -/ structure ProjectAgentLock where - /-- 作用域:项目级(`PINNED`, ADR-0002 `scope = project_id`)。 -/ + /-- 作用域:项目级(ADR-0002)。 -/ scope : I.ProjectId - /-- 持有者:一个 run(`PINNED`, ADR-0002 `owner = run_id`)。 -/ + /-- 持有者:一个 run(ADR-0002)。 -/ owner : I.RunId -/-- 锁表:每项目当前持锁 run(`PINNED` 排他性, ADR-0002)。`ProjectId → Option RunId` -的结构**本身**即排他——不可能为同一项目登记两个并发 owner。 -/ +/-- 锁表:每项目当前持锁 run(ADR-0002 排他性)。`ProjectId → Option RunId` 的结构本身 + 即排他——不可能为同一项目登记两个并发 owner。 -/ def LockTable := I.ProjectId → Option I.RunId -/-- 锁表良构:**持锁者必为非终止 run**(`PINNED` 平台核心不变式, ADR-0002)。 - -"锁在 run 终止时释放"的逻辑等价物:若 `p` 的锁被 `r` 持有,则 `r` 不在终止态。这条 -把 Lock 与 Run 耦合起来——likec4 能画"run owns lock while running",画不出"终止即 -必须释放"这个约束;它正是契约相对结构图的增量。 -/ -def LockTable.WellFormed - (lt : LockTable I) (statusOf : I.RunId → RunState) : Prop := - ∀ p r, lt p = some r → ¬ (statusOf r).Terminal +/-- 锁表良构:持锁者必为非终止 run(ADR-0002 核心不变式)。"锁在 run 终止时释放" + 的等价物:若 `p` 的锁被 `r` 持有,则 `r` 不在终止态。 -/ +def LockTable.WellFormed (lt : LockTable I) : Prop := + ∀ p r, lt p = some r → ¬ Terminal I r end Spec.System diff --git a/spec/Spec/System/Permission.lean b/spec/Spec/System/Permission.lean index daffb18..b4b94a6 100644 --- a/spec/Spec/System/Permission.lean +++ b/spec/Spec/System/Permission.lean @@ -1,66 +1,23 @@ import Spec.Prelude /-! -# Permission —— 角色、能力与授权 +# Permission —— 协作者角色 -ADR-0004:权限走"飞书云文档式"——grant(`resource + principal + role`)与 settings -分离;role 取自封闭的 `read / edit / manage`,且 **read ⊂ edit ⊂ manage** 累积赋能; -强制释放锁是 **admin-only**,在 role 体系之外。本模块把这套结构与"高 role 含低 -role 全部能力"的单调性钉死。 +ADR-0004:权限走"飞书云文档式"——grant(resource + principal + role)与 settings 分离; +role 取自封闭的 read / edit / manage,且 read ⊂ edit ⊂ manage 累积赋能;强制释放锁是 +admin-only,在 role 体系之外。 + +本模块钉角色三级与累积关系。具体哪些操作归哪级,见 ADR-0004,待业务反馈细化——所以这里 +不钉操作枚举,也不钉"哪个能力要求哪个 role"的映射。 -/ namespace Spec.System -/-- 协作者角色(`PINNED` 封闭, ADR-0004 逐字 "roles are read, edit, or manage")。 -/ +/-- 协作者角色(ADR-0004:read / edit / manage)。read ⊂ edit ⊂ manage,高 role 含低 role + 全部能力。强制释放锁不在这套体系里,是 admin-only override,由平台另行判定。 -/ inductive Role where | read | edit | manage -/-- 角色赋能层级(`PINNED` 序, ADR-0004 read⊂edit⊂manage 数值化)。仅服务于 -`Role.le` 与能力推导,不对外承诺"层级就是 `Nat`"。 -/ -def Role.level : Role → Nat - | .read => 0 - | .edit => 1 - | .manage => 2 - -/-- 角色偏序:`r₁ ≤ r₂` 即 `r₁` 赋能不强于 `r₂`(`PINNED`, ADR-0004)。 -/ -def Role.le (r₁ r₂ : Role) : Prop := r₁.level ≤ r₂.level - -/-- 受 role 调控的操作能力(各项 `PINNED` 取自 ADR-0004;**枚举完整性 `OPEN`**—— -这是 ADR 当前点名的能力,不保证穷尽,新增产品操作时可能扩)。注意 force-release -**不在此列**——它是 admin-only override,见 `RequiresAdmin`。 -/ -inductive Capability where - | view - | discussComment - | editArtifact - | triggerAgent - | answerChoiceCard - | manageCollaborators - | projectSettings - | groupBinding - | normalCancel - -/-- 某能力所**要求的最低角色**(`PINNED`, ADR-0004 各 role 能力展开)。授权判定 -`Role.can` 据此定义,"谁能做什么"只有这一处真相。 -/ -def Capability.requiredRole : Capability → Role - | .view => .read - | .discussComment | .editArtifact | .triggerAgent | .answerChoiceCard => .edit - | .manageCollaborators | .projectSettings | .groupBinding | .normalCancel => .manage - -/-- 角色 `r` **具备**能力 `c`(`PINNED`, ADR-0004)。定义为"`c` 的最低角色 ≤ `r`", -这一处同时编码了 read⊂edit⊂manage 的累积性。 -/ -def Role.can (r : Role) (c : Capability) : Prop := c.requiredRole |>.le r - -/-- **单调性**:`r₁ ≤ r₂` 且 `r₁` 能做 `c` ⇒ `r₂` 也能(`PINNED` 定理, ADR-0004 累积 -赋能的形式化保证)。证明即偏序传递性,得益于 `can` 按"最低角色阈值"定义。 -/ -theorem Role.can_mono {r₁ r₂ : Role} {c : Capability} - (h : r₁.le r₂) (hc : r₁.can c) : r₂.can c := - Nat.le_trans hc h - -/-- **强制释放锁**要求 admin,**在 role 体系之外**(`PINNED`, ADR-0004 admin-only -override)。即便 `manage` 也不经 `Role.can` 获得它,故它不是 `Capability` 而是独立 -谓词;`isAdmin` 由平台另行判定(本层不建 admin 模型)。 -/ -def RequiresAdmin (isAdmin : Prop) : Prop := isAdmin - end Spec.System diff --git a/spec/Spec/System/Run.lean b/spec/Spec/System/Run.lean index 7662200..7fdc96f 100644 --- a/spec/Spec/System/Run.lean +++ b/spec/Spec/System/Run.lean @@ -1,28 +1,22 @@ -/-! -# Run —— AgentRun 状态机 +import Spec.Prelude -一次 `@Claude` 创建一个 `AgentRun`(ADR-0001),它在终止时释放项目锁(ADR-0002)。 -合法转移关系在任何 ADR / likec4 散文里都未定下,故本模块只刻画**状态**与**终止 -判定**(后者是 Lock 排他不变式的依赖),不臆造转移边。 +/-! +# Run —— AgentRun 的终止判定 + +一次 `@Claude` 创建一个 AgentRun(ADR-0001),它在终止时释放项目锁(ADR-0002)。 + +run 的具体状态集合没定(OPEN):ADR-0001..0003 列了一些状态名,但从未声明"状态恰好 +这些",实现若需新状态(如 pending)要提出来,不要默认已穷尽。所以这里不钉状态枚举, +只钉一条契约需要的事实:一个 run 是否处于终止态。终止态由实现判定(状态集合本身未定, +没法在契约里算)。 -/ namespace Spec.System -/-- AgentRun 运行状态(状态名 `PINNED`, ADR-0001..0003 + likec4;**完整性 `OPEN`** -——散文从未声明"状态恰好这些";实现若需新状态(如 pending)须 surface,不得默认 -本枚举已穷尽)。终止态见 `RunState.Terminal`。 -/ -inductive RunState where - | active - | waitingForUser - | completed - | failed - | timedOut - | canceled +variable (I : Identifiers) -/-- run 处于**终止态**(`PINNED`, ADR-0002:锁在 completes/fails/timesOut/canceled -时释放)。`active`/`waitingForUser` 非终止——后者仍占用项目(锁未释放)。 -/ -def RunState.Terminal : RunState → Prop - | .completed | .failed | .timedOut | .canceled => True - | .active | .waitingForUser => False +/-- run 是否处于终止态(ADR-0002)。真值由实现给——状态集合未定(OPEN),故此处不钉 + 具体状态名,只钉"存在终止与否的判定"。锁在 run 终止时释放(见 `Lock`)。 -/ +opaque Terminal : I.RunId → Prop end Spec.System