diff --git a/docs/adr/0006-element-schema-and-rich-content.md b/docs/adr/0006-element-schema-and-rich-content.md new file mode 100644 index 0000000..a3c79b3 --- /dev/null +++ b/docs/adr/0006-element-schema-and-rich-content.md @@ -0,0 +1,116 @@ +# ADR 0006: Element Schema Is Declarative, Rich Content Is Typst + +## Status + +Accepted — for the decisions below. Several sub-decisions are deliberately left +open; see *Open Questions / Deferred*. + +Builds on ADR-0005, which fixed that an element instance = a kind tag + data +conforming to that kind's schema, and that a kind's minimal contract to the +framework is its **data schema only**. This ADR fixes **how that schema is +expressed** and **what the schema's "rich content" leaves actually are**. + +## Context + +ADR-0005 left the schema representation and the kind-definition mechanism as the +largest OPEN items — and they are the foundation the rule-based checker stands +on (the checker validates "does this data conform to its kind's schema?"). The +domain is formula-heavy and content-structured: a worked example has a problem +statement, options, a solution; a theorem has a statement, a proof, prerequisite +lemmas. These fields are not bare strings — they are *rich content*. + +Two facts about Typst were verified against its source +(`/Users/sjfhsjfh/Typst/typst`) and drive the decisions below: + +- A `.typ` file evaluates to a `Module` that carries **both** a `scope` of + `#let` exports **and** a body `Content` (the rendered top-level markup). + `Content` retains a `Span` that resolves back to a `FileId` + byte range, so + click-to-jump from rendered content to source is possible. +- `Content` has no `Deserialize`; and Typst's `Source::new` **requires** a + `FileId`. Source evaluated with a detached span loses its file identity: + `span.id()` becomes `None` (click-to-jump breaks) and a relative + `import "../x"` fails with *"cannot access file system from here"*. Relative + imports and click-to-jump only work when the source is a real file (with a + `VirtualPath`) in the compiler's `World`. + +## Decision + +### The data schema is declarative — a JSON Schema + +A kind declares its data shape as a **declarative JSON Schema** (field names, +types, constraints), not as a program and not as a bespoke schema DSL. The +checker reads the schema and validates instance data structurally against it. +Whether stdlib kinds author their schema by hand-written JSON or via a host- +language builder is an implementation detail, not part of this contract. + +### Field types: built-in scalars plus a `content` leaf type + +Schema field types are the built-in scalars (string / number / boolean / enum / +list / object, as in ordinary JSON Schema) **plus one extension type: +`content`**. JSON Schema has no native notion of "typst content", so this is a +deliberate **extension** of JSON Schema (a custom type / `format`). Any +implementation must honor the same `content` extension rather than inventing its +own — this is the seam between the schema layer (A) and the rich-content layer. + +### A `content` value is a Typst source; its meaning is the module's body content + +The value of a `content` field is a **Typst source**. Its denotation is the +**body content** of that source evaluated as a module (Typst's `Module.content`) +— not its `#let` exports. The canonical stored form is the **source text**, not +a serialized `Content`: `Content` cannot be deserialized and its spans are only +meaningful with the source present, so content is re-evaluated from source when +needed, never round-tripped as data. + +### Rich content is never free-floating — it has a virtual path + +Because detached Typst source loses click-to-jump and cannot do relative +imports, a `content` value is **not** an anonymous text blob. It is a first-class +file in the compiler's `World`, carrying a **virtual path**. This is what makes +its spans resolve (click-to-jump) and its relative imports anchor. Concretely, +the engineering file constitutes a **virtual file system with internal path +structure**; each rich-content field sits at a path within it. + +(This ADR commits only to *"there is a path structure"*. Its concrete on-disk +form — that the engineering file is a real directory tree — is fixed separately +in ADR-0007. ADR-0006 does not assume the path structure is a disk directory.) + +### Import boundary: within the engineering file, plus packages + +A relative `import` inside a rich-content source may resolve only to other paths +**within the same engineering file's path structure** (reusing definitions local +to this lesson), plus Typst **`@package`** ecosystem imports. It may **not** +reach into other engineering files. Cross-lesson reuse, if any, goes through a +separate mechanism (question bank / reuse — still OPEN, see ADR-0005 Deferred), +not through raw cross-file imports. + +## Consequences + +- The checker can introspect a rendered `Content` (its element type, fields, + downcasts) to validate rich content beyond "is it present", and can use spans + to point diagnostics back at the offending source location. +- Canonical state is source text; `Content` is a transient product of + evaluation. Storage, diffing, and agent edits all operate on source, not on + serialized content. +- Extending JSON Schema with `content` means conformance has a shared extension + point: implementations align on one `content` semantics instead of each + inventing a rich-text encoding. +- Rich content requiring a virtual path means the engineering file is inherently + a path-structured container, not a bag of anonymous snippets — which is what + ADR-0007 then grounds on disk. +- The import boundary keeps an engineering file self-contained: it depends only + on itself and on published packages, never on a sibling lesson's internals. + +## Open Questions / Deferred + +- **Content element constraints (Y)** — whether a `content` field may be further + constrained to admit only certain Typst element kinds (e.g. "inline only, no + figure", "exactly one final expression"). Deferred: we will know which + constraints are needed only once real stdlib kinds exist. Until then a + `content` field means "a block of content", inner element shape unconstrained. +- **stdlib kind set** — the first batch of framework-provided kinds and their + individual schemas (each is later, per-kind work). +- **JSON Schema dialect** — which draft, and exactly which keywords are + permitted in a kind schema (a subset/profile is likely, to keep the checker + tractable). Not pinned here. +- **On-disk form** — fixed in ADR-0007 (directory tree); layout conventions + (manifest, element ordering) deferred beyond that. diff --git a/docs/adr/0007-engineering-file-as-directory-tree.md b/docs/adr/0007-engineering-file-as-directory-tree.md new file mode 100644 index 0000000..a752d57 --- /dev/null +++ b/docs/adr/0007-engineering-file-as-directory-tree.md @@ -0,0 +1,73 @@ +# ADR 0007: The Engineering File Is A Directory Tree On Disk + +## Status + +Accepted — for the on-disk decision below. The concrete layout conventions are +deliberately left open; see *Open Questions / Deferred*. + +Grounds the abstract premise ADR-0006 relied on. ADR-0006 established that rich +content needs a **virtual path** and that the engineering file therefore +constitutes a path-structured virtual file system — but it deliberately did not +say what that path structure *is* physically. This ADR fixes that: it is a real +directory tree on a real file system. + +## Context + +ADR-0006 showed that a rich-content (`content`) value cannot be free-floating +Typst source: it must be a first-class file with a virtual path so that +click-to-jump (spans) and relative imports work. That leaves a choice for the +physical form of the engineering file: a packed/opaque archive, a database blob, +or a plain directory tree. + +The decisive constraint is **who edits the engineering file**: a coding agent +(Claude) collaboratively with teachers (ADR-0005's premise), and ordinary tools. +An agent works best when it can read and modify files directly and use existing +tooling (`grep`, `find`, diff, version control) over plain files in plain +directories. A packed or database form would force a custom access layer for +every such operation. + +The developer's earlier prototype already had this shape implicitly — +`segments/`, `examples/`, `lemmas/` directories with per-item files — which is +the directory tree in embryo, not a crude stand-in. + +## Decision + +The on-disk form of an engineering file is a **directory tree** on a real file +system. + +- A `content` field's **virtual path** (ADR-0006) is a **real relative path** + within that directory tree. The compiler's `World` maps virtual paths to the + actual files in the tree; no synthetic/in-memory file system is needed. +- Relative imports inside rich content resolve relative to the importing file's + real position in the tree — which is exactly the import boundary ADR-0006 + pinned ("within the engineering file, plus `@package`"). This ADR gives that + boundary its physical basis: "within the engineering file" = "within this + directory tree". + +This keeps the engineering file legible to agents and to off-the-shelf tooling, +and makes the relationship between content fields and their sources directly +inspectable on disk. + +## Consequences + +- The engineering file is a directory of plain text/Typst files: directly + greppable, diffable, version-controllable, and editable by an agent without a + bespoke access layer. +- `World` is a thin mapping from the directory tree; virtual path = relative path + removes any need to invent or maintain a separate virtual file system. +- The engineering file remains self-contained on disk: its import closure is the + tree itself plus published packages (ADR-0006), so it can be moved, copied, or + archived as a directory without dangling references to sibling lessons. +- This is the **physical representation** of ADR-0005's abstract `Lesson` (an + ordered sequence of typed elements); how that ordered structure is encoded into + the directory is a separate question (below), not implied by "it's a tree". + +## Open Questions / Deferred + +- **Layout conventions** — the concrete directory layout is *not* fixed here. + Specifically deferred: the manifest file (name, location, what it holds); how + element instances are arranged in the tree and how their **order** (ADR-0005's + `Lesson` is an ordered sequence) is encoded; naming/organization of + rich-content `.typ` files. This is the on-disk encoding of ADR-0005's `Lesson` + and warrants its own ADR — kept separate so this one fixes only "it is a + directory tree", not "how the tree is arranged". diff --git a/spec/Spec.lean b/spec/Spec.lean index 9f7d538..46dd4a3 100644 --- a/spec/Spec.lean +++ b/spec/Spec.lean @@ -1,3 +1,5 @@ -- This module serves as the root of the `Spec` library. -- Import modules here that should be built as part of the library. +import Spec.Prelude +import Spec.System import Spec.Courseware diff --git a/spec/Spec/Courseware.lean b/spec/Spec/Courseware.lean index 866e466..a3369f7 100644 --- a/spec/Spec/Courseware.lean +++ b/spec/Spec/Courseware.lean @@ -1,9 +1,26 @@ +import Spec.Courseware.Primitives +import Spec.Courseware.RichContent +import Spec.Courseware.Element import Spec.Courseware.Lesson +import Spec.Courseware.Render +import Spec.Courseware.Diagnostic +import Spec.Courseware.QuestionBank +import Spec.Courseware.Course /-! # Courseware —— 产品层契约(课程工程文件) -本层是护城河:课程"工程文件"的语义母本与合法性规则。当前只有 lesson 骨架 -(见 `Spec.Courseware.Lesson`,ADR-0005);题库、course 编排、完整合法性判定 -等仍 `OPEN`,待各自 ADR 落定后逐个加入。 +护城河:课程"工程文件"的语义母本与合法性规则。决策出处 ADR-0005 / 0006 / 0007。 + +已填实(PINNED): +- `Primitives` —— 基元载体(表示留给实现;schema 形态见 ADR-0006)。 +- `RichContent` —— 富内容 = 带虚拟路径的 typst 源(ADR-0006 的 prose 母本)。 +- `Element` —— kind 标签 + 依赖 schema 的数据。 +- `Lesson` —— element 的有序序列(序载教学语义、不建模时长)。 +- `Render` —— (kind × target) 渲染配置矩阵 + covers。 +- `Diagnostic` —— Severity + checker 第一条诊断(缺渲染 ⇒ warning)。 + +留白骨架(核心关系 OPEN,已 surface 不臆造): +- `QuestionBank` —— 题库与 element 的关系(引用 vs 内联)。 +- `Course` —— course = lesson 编排的规则。 -/ diff --git a/spec/Spec/Courseware/Course.lean b/spec/Spec/Courseware/Course.lean new file mode 100644 index 0000000..30a165c --- /dev/null +++ b/spec/Spec/Courseware/Course.lean @@ -0,0 +1,16 @@ +import Spec.Courseware.Lesson + +/-! +# Course —— 课程编排(骨架,规则 OPEN) + +ADR-0005:工程文件的粒度是**单节课**;course / 单元**不是**工程文件,而是 lesson +的**编排**。 + +但"编排"的具体规则未决策:course 是 lesson 的有序列表,还是带层级(单元 → 课)的 +树?编排里 lesson 是被引用还是被包含?跨 lesson 有无约束(目标覆盖、前后置)?这些 +都是 `OPEN`。 + +按宪法第 2 条,本模块**不臆造**编排结构——不建 `Course := List Lesson`(那会偷偷 +承诺"扁平有序、无层级")。只在此 surface:课程编排待专门 ADR。本文件当前不引入任何 +承诺性声明。 +-/ diff --git a/spec/Spec/Courseware/Diagnostic.lean b/spec/Spec/Courseware/Diagnostic.lean new file mode 100644 index 0000000..2f75329 --- /dev/null +++ b/spec/Spec/Courseware/Diagnostic.lean @@ -0,0 +1,45 @@ +import Spec.Courseware.Lesson +import Spec.Courseware.Render + +/-! +# Diagnostic —— checker 诊断(种子) + +产品里"站在 Lean 位置"的那个 rule-based checker,语义在此沉淀。它对 lesson 提诊断, +每条诊断有**严重级别**。本模块固定级别类型,并落第一条规则——ADR-0005 钉死的"缺 +渲染 ⇒ warning"。完整的"合法 lesson"判定仍 OPEN,本模块只是它的起点。 +-/ + +namespace Spec.Courseware + +/-- +诊断的严重级别(`PINNED` 二分, ADR-0005 区分 warning 与阻断)。 + +`error` 阻断(产物不合法),`warning` 不阻断(产物仍可导出,只是有损/有忽略)。 +ADR-0005 已用到这个区分:缺渲染是 warning 而非 error。更细的级别(info/hint)未 +决策,故只二分。 +-/ +inductive Severity where + | warning + | error + +variable (P : Primitives) + +/-- +**缺渲染诊断**:lesson 在 target `t` 下存在无法渲染的 element(`PINNED`, ADR-0005)。 + +成立 ⟺ 存在某 element,其 kind 在 `t` 下未配渲染规则。这条对应 checker 的第一条 +诊断;其级别由下面的 `renderIgnoredSeverity` 钉死为 **warning**。 +-/ +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-0005 明确:某 (kind, target) 无渲染规则时,checker 报 warning 说该 element 在 +该 target 被忽略,**不阻断导出**。把这条决策固定为一个常量,使"它是 warning 不是 +error"成为契约里可被引用、可被对齐的事实,而不是散落在 prose 里的口头约定。 +-/ +def renderIgnoredSeverity : Severity := .warning + +end Spec.Courseware diff --git a/spec/Spec/Courseware/Element.lean b/spec/Spec/Courseware/Element.lean new file mode 100644 index 0000000..d1bb7f9 --- /dev/null +++ b/spec/Spec/Courseware/Element.lean @@ -0,0 +1,32 @@ +import Spec.Courseware.Primitives + +/-! +# Element —— 课程内容的原子单位 + +ADR-0005:element 实例 = 一个 kind 标签 + 符合该 kind schema 的数据。本模块把这条 +编码成一个依赖结构,使"数据必须匹配其 kind"成为类型层面的事实而非运行时校验。 +-/ + +namespace Spec.Courseware + +variable (P : Primitives) + +/-- +element 实例(`PINNED`, ADR-0005)。 + +`data` 的类型 `P.ElementData kind` **由 `kind` 决定**——这意味着无法构造一个数据与 +其 kind 不符的 element:schema 合规由类型系统而非 checker 保证。 + +ADR-0005 的 (a) 类信息(逐字稿、重点圈划等"语义性但只在某些 target 浮现"的字段) +属于具体 kind 的 schema,落在 `P.ElementData` 内,不出现在这个通用结构上;(b) 类 +信息(html 交互、build/npm)按 ADR-0005 不进 element。交互教具是一种"重型 kind", +其 `ElementData` 只承载题目/配置数据,重实现在模型之外——它在此结构里与例题、定理 +同构,仅 `kind` 不同。 +-/ +structure Element where + /-- 该 element 的 kind。 -/ + kind : P.KindId + /-- 符合 `kind` schema 的数据(类型随 `kind` 而变)。 -/ + data : P.ElementData kind + +end Spec.Courseware diff --git a/spec/Spec/Courseware/Lesson.lean b/spec/Spec/Courseware/Lesson.lean index 99d2330..01564c9 100644 --- a/spec/Spec/Courseware/Lesson.lean +++ b/spec/Spec/Courseware/Lesson.lean @@ -1,115 +1,21 @@ +import Spec.Courseware.Element + /-! -# Lesson —— 课程工程文件的母本模型(单节课) +# Lesson —— 单节课工程文件 -本文件固定 ADR-0005 的骨架共识:一个**工程文件 = 一节课(lesson)**, -lesson 是**有类型 element 实例的有序序列**;element 实例 = kind 标签 + 符合该 -kind schema 的数据;export target 是对 lesson 的投影;渲染由一份 -**(kind × target) 配置矩阵**承载。 - -本轮**只承诺关系结构**。所有尚未决定的基元(schema 怎么表示、kind 怎么定义、 -render rule 的载荷长什么样)都收口进 `Primitives`,以抽象类型留白(`OPEN`), -契约因此对未定之物**零承诺**,同时仍 type-check 通过。完整的"合法 lesson"判定 -亦未定;本轮只落 checker 的第一颗种子(缺渲染 ⇒ warning)。 +ADR-0005:一个工程文件 = 一节课,是 element 实例的**有序序列**。课程/单元不是工程 +文件,而是 lesson 的编排(见 `Spec.Courseware.Course`,OPEN)。 -/ namespace Spec.Courseware /-- -契约基元载体(`PINNED` 关系结构 / `OPEN` 基元留白,`ADR-0005`)。 +一节课(`PINNED`, ADR-0005)。 -把本轮**尚未决定**的基元收口到一处,使 lesson 模型在其上参数化。每个字段都是 -一个 `OPEN` 点:契约只声明它**存在**、以及它在关系中扮演的角色,绝不假设其内部 -表示。具体表示待后续各自的 ADR 落定后再 refine。 +用 `List` 而非 `Multiset`/`Finset`,因为 **element 的先后次序承载教学语义**(讲义/ +PPT 式的内容流,先讲定义再举例不同于反过来)。**不建模时长**:ADR-0005 决定 lesson +是内容编排而非时间轴,故这里没有"每块多少分钟"这类字段——序是结构,时长不是。 -/ -structure Primitives where - /-- - element 的**种类标识**(`PINNED` 开放宇宙 / `OPEN` 表示,`ADR-0005`)。 - - kind 构成一个**开放、可扩展的宇宙**(stdlib default + 远期第三方),因此**刻意 - 用一个抽象类型,而非封闭 `inductive`/枚举**——把"kind 集合不封闭"这条 PINNED - 直接编码进类型。`KindId` 的具体表示是 `OPEN`。 - -/ - KindId : Type - /-- - 某 kind 的**合法数据**类型(`PINNED` 依赖关系 / `OPEN` schema 表示,`ADR-0005`)。 - - 以 `KindId` 为索引的**依赖类型**,精确表达"element 数据必须**符合该 kind 的 - schema**":不同 kind 的合法数据类型不同。kind 对框架的最小契约**就是**这份 - schema(渲染不在其中)。schema 自身**怎么表示**是 `OPEN`,故此处只给出 - `KindId → Type` 这一依赖,不触碰其内部。 - -/ - ElementData : KindId → Type - /-- - **导出目标标识**(`PINNED` 角色 / `OPEN` 表示,`ADR-0005`)。 - - 一个 target(学生讲义 / 教师教案 / PPT / 第三方平台 archive / html 教具平台…) - 是对同一 lesson 的一种投影。target 同样是开放集合;其具体表示 `OPEN`。 - -/ - TargetId : Type - /-- - **渲染规则的载荷**(`OPEN` 表示,`ADR-0005`)。 - - "某 kind 在某 target 下如何呈现"的那条规则的**内容**。其表示完全 `OPEN`(typst - 只是渲染后端之一,不是定义语言)——本轮只关心规则**在不在**(见 `RenderConfig`), - 不关心它**是什么**。 - -/ - RenderRule : Type - -variable (P : Primitives) - -/-- -**element 实例**:一个 kind 标签 + 符合该 kind schema 的数据(`PINNED`,`ADR-0005`)。 - -`data` 的类型由 `kind` 决定(`P.ElementData kind`),从类型上保证"数据符合该 kind -的 schema"——构造一个 `Element` 时不可能给出与其 kind 不匹配的数据。 - -注:ADR-0005 的 (a) 类信息(逐字稿、重点圈划等"语义性但 target-specific"的字段) -属于具体 kind 的 schema 范畴,故落在 `P.ElementData` 内,不在此通用结构上出现; -(b) 类信息(html 交互、build/npm)不进 element。 --/ -structure Element where - /-- 该 element 的种类(`PINNED`,`ADR-0005`)。 -/ - kind : P.KindId - /-- 符合 `kind` schema 的数据(`PINNED`,`ADR-0005`)。 -/ - data : P.ElementData kind - -/-- -**lesson = element 实例的有序序列**(`PINNED`,`ADR-0005`)。 - -用 `List` 编码"有序":**次序是有意义的**。**时长不建模**——lesson 是内容编排 -(讲义/PPT 式的内容流),不是时间轴。课程/单元不是 lesson,而是 lesson 的编排 -(`OPEN`,见 ADR-0005 Deferred),不在本文件。 --/ -abbrev Lesson := List (Element P) - -/-- -**渲染配置矩阵**:(kind × target) → 可选的渲染规则(`PINNED`,`ADR-0005`)。 - -这份矩阵**住在工程文件里**:框架给好 default,文件可逐项 override。`rule k t = none` -表示该 (kind, target) 对**尚无渲染规则**(此处只建模规则的**有无**,不建模其内容)。 --/ -structure RenderConfig where - /-- (kind, target) ↦ 该对是否配了渲染规则及其载荷(`PINNED`,`ADR-0005`)。 -/ - rule : P.KindId → P.TargetId → Option P.RenderRule - -/-- -kind `k` 在 target `t` 下**已配渲染规则**(`PINNED`,`ADR-0005`)。 - -即矩阵在该 (kind, target) 处非空。"覆盖"= 有规则可用;`covers` 为假即"缺渲染"。 --/ -def RenderConfig.covers {P : Primitives} (c : RenderConfig P) (k : P.KindId) (t : P.TargetId) : Prop := - (c.rule k t).isSome - -/-- -**checker 种子规则**:lesson 在 target `t` 下**存在被忽略的 element**(`PINNED`,`ADR-0005`)。 - -成立 ⟺ lesson 里**存在**某 element,其 kind 在 `t` 下没有渲染规则。 - -ADR-0005 PIN 住该情形的**严重级别 = warning,而非 error**:它**不阻断**导出,只提示 -"这些 element 在该 target 下被忽略了"。这是 checker(产品里"站在 Lean 位置"的那个 -东西)的第一颗诊断种子;完整的"合法 lesson"判定仍 `OPEN`。 --/ -def WarnsIgnored (l : Lesson P) (c : RenderConfig P) (t : P.TargetId) : Prop := - ∃ e ∈ l, ¬ c.covers e.kind t +abbrev Lesson (P : Primitives) := List (Element P) end Spec.Courseware diff --git a/spec/Spec/Courseware/Primitives.lean b/spec/Spec/Courseware/Primitives.lean new file mode 100644 index 0000000..ff91b45 --- /dev/null +++ b/spec/Spec/Courseware/Primitives.lean @@ -0,0 +1,54 @@ +/-! +# Primitives —— Courseware 契约的留白基元 + +课程工程文件模型(ADR-0005)依赖一组基元:element kind 怎么标识、某 kind 的数据 +schema 是什么、export target 怎么标识、渲染规则的载荷长什么样。 + +把它们收口成一个载体 `Primitives`,让 lesson 模型在其上参数化——契约因此能谈 +element / lesson / 渲染**之间的关系**,而把每个基元的**内部表示**留给实现。注意: +"某基元的语义已 PINNED"与"其表示进 Lean"是两回事——schema 的**形态**已由 ADR-0006 +钉死(声明式 JSON Schema + 富内容叶子 = typst content),但那是 JSON / typst 的内部 +结构、属实现细节,**不入 Lean**;Lean 只锚定"数据符合 kind schema"这条关系,故这些 +基元在此仍以抽象类型承载。富内容这一新概念的 prose 母本见 `Courseware.RichContent`。 +-/ + +namespace Spec.Courseware + +/-- +Courseware 契约基元载体(关系 `PINNED`, ADR-0005;各基元表示留给实现, ADR-0006)。 +-/ +structure Primitives where + /-- + element kind 的标识(`PINNED` 开放宇宙, ADR-0005;表示 `OPEN`)。 + + **刻意用抽象类型而非 `inductive`**:ADR-0005 决定 kind 是开放可扩展宇宙(stdlib + default + 第三方),封闭枚举会直接违背它。这与 `RunState` 的"未封闭"不同——此处 + 开放是**已决策的**。 + -/ + KindId : Type + /-- + 某 kind 的合法数据类型(`PINNED` 依赖关系, ADR-0005;schema 形态 `PINNED` ADR-0006, + 表示仍抽象)。 + + 以 kind 为索引:不同 kind 的合法数据类型不同。这正是 ADR-0005"kind 的最小契约 + = 数据 schema"的载体——`ElementData k` 即"符合 `k` 之 schema 的数据"。 + + schema 的**形态**已由 ADR-0006 定:声明式 **JSON Schema**,字段类型 = 内置标量 + + 一个 `content` 扩展类型;`content` 字段的值是一段 **typst 源**(canonical 存为带 + 虚拟路径的源,语义取其 module body)。但这些是 JSON / typst 的内部结构——**实现 + 细节,非分歧点**,不进 Lean。故 `ElementData` 在此**仍是抽象类型**:契约只承诺 + "存在一个由 kind 决定的合法数据类型",不复刻 JSON Schema / typst Content 的形状。 + -/ + ElementData : KindId → Type + /-- export target 的标识(`PINNED` 角色, ADR-0005;表示 `OPEN`)。一个 target 是对 lesson 的一种投影(讲义/教案/PPT/平台 archive…)。 -/ + TargetId : Type + /-- + 渲染规则的载荷(表示 `OPEN`, ADR-0005)。 + + "某 kind 在某 target 下如何呈现"那条规则的**内容**。typst 是渲染后端之一(`PINNED`, + ADR-0005)、不是定义语言;但渲染管线/规则载荷的具体表示仍 `OPEN`。契约只关心规则 + **在不在**(见 `Render`),不碰它是什么。 + -/ + RenderRule : Type + +end Spec.Courseware diff --git a/spec/Spec/Courseware/QuestionBank.lean b/spec/Spec/Courseware/QuestionBank.lean new file mode 100644 index 0000000..f0450be --- /dev/null +++ b/spec/Spec/Courseware/QuestionBank.lean @@ -0,0 +1,17 @@ +import Spec.Courseware.Element + +/-! +# QuestionBank —— 题库(骨架,核心关系 OPEN) + +题库是整个方案里与工程文件并列的资产(讨论里类比 DAW 的 sample library):有自身 +结构的被建模实体,又是最典型的可复用单元,lesson 会引用它。 + +但**题库与 element 的关系尚未决策**,且用户明确指出"纯引用可能不够": +- element 内联题目数据(如交互教具那样),还是 +- lesson 持一个指向题库条目的**引用**,还是 +- 两者并存? + +这是一个 `OPEN` 分歧点。按宪法第 2 条,本模块**不替它选解**——不建 `QuestionRef` +也不建内联结构,只在此 surface 该问题。待专门的 ADR 落定后再填。本文件当前只承载 +这条说明,不引入任何承诺性声明。 +-/ diff --git a/spec/Spec/Courseware/Render.lean b/spec/Spec/Courseware/Render.lean new file mode 100644 index 0000000..76a5895 --- /dev/null +++ b/spec/Spec/Courseware/Render.lean @@ -0,0 +1,36 @@ +import Spec.Courseware.Primitives + +/-! +# Render —— 渲染配置矩阵 + +ADR-0005:某 kind 在某 target 下如何呈现,由一份 **(kind × target) 配置矩阵**决定; +矩阵住在工程文件里,框架给 default、文件可 override。本模块只建矩阵结构与"是否已 +配置"的判定;规则的**内容**(`RenderRule`)是 OPEN,不碰。 +-/ + +namespace Spec.Courseware + +variable (P : Primitives) + +/-- +渲染配置矩阵(`PINNED`, ADR-0005)。 + +`rule k t = none` 表示 (kind `k`, target `t`) 这一对**尚无渲染规则**;`some _` 表示 +有。框架默认与文件 override 最终都坍缩成这一个映射——契约不区分"默认值"与"用户改 +过的值",只看最终矩阵在每一格的有无。 +-/ +structure RenderConfig where + /-- (kind, target) ↦ 该对的渲染规则(无则 `none`)。 -/ + rule : P.KindId → P.TargetId → Option P.RenderRule + +/-- +kind `k` 在 target `t` 下**已配渲染规则**(`PINNED`, ADR-0005)。 + +即矩阵该格非空。`covers` 为假即"此 kind 在此 target 下无从渲染"——checker 据此报 +警(见 `Spec.Courseware.Diagnostic`)。`P` 隐式,以便 `c.covers k t` 点记法可用。 +-/ +def RenderConfig.covers {P : Primitives} (c : RenderConfig P) + (k : P.KindId) (t : P.TargetId) : Prop := + (c.rule k t).isSome + +end Spec.Courseware diff --git a/spec/Spec/Courseware/RichContent.lean b/spec/Spec/Courseware/RichContent.lean new file mode 100644 index 0000000..eadc61e --- /dev/null +++ b/spec/Spec/Courseware/RichContent.lean @@ -0,0 +1,39 @@ +/-! +# RichContent —— 富内容(ADR-0006 的 prose 母本) + +ADR-0006 给 element schema 的"叶子"定了形:一个字段可以是 `content` 类型,其值是 +**一段 typst 源**,语义上取该源作为 module 求值后的 **body content**。 + +关键约束(均 ADR-0006,源自 typst 源码事实):富内容**不可无主**——typst 的源必须 +有 `FileId`,否则 span 脱锚(`span.id() = none`,点击跳转失效)且相对 `import` 报 +"cannot access file system from here"。故每段富内容是 World 里的一等文件,坐落在一个 +**虚拟路径**上;相对 import 限本工程路径结构内 + `@package`(不跨工程)。 + +本模块只为这个概念立一个 prose 锚点 + 一个**最小抽象签名**。typst 的 `Content` / +`Module` 内部结构、JSON Schema 的形状都是**实现细节、非分歧点**,不进 Lean——这里 +不复刻它们,只承诺"富内容由一个虚拟路径定位"这一条 ADR-0006 钉死的关系。 +-/ + +namespace Spec.Courseware + +/-- +富内容在工程文件路径结构中的**虚拟路径**(`OPEN` 表示, ADR-0006)。 + +它把一段富内容定位为 World 里的一等文件(span 可解析、相对 import 可锚定)。其具体 +表示——以及它落到磁盘后就是真实相对路径(ADR-0007)——不在本层承诺,故 opaque。 +-/ +opaque VPath : Type + +/-- +对一段富内容的**引用**:它坐落在某个虚拟路径上(`PINNED` 关系, ADR-0006)。 + +契约层面,一段 `content` 字段值由其虚拟路径标识(canonical 存储是该路径下的 typst +源文本,而非序列化的 `Content`——后者不可反序列化)。这里**刻意不**建模源文本、 +不建模求值出的 `Content`:那是实现侧的事。此结构只钉死"富内容经由一个 `VPath` +定位"这一条关系,作为 `Primitives.ElementData` 里 `content` 叶子的语义锚点。 +-/ +structure RichContentRef where + /-- 该富内容所在的虚拟路径(ADR-0006;落盘后为真实相对路径, ADR-0007)。 -/ + vpath : VPath + +end Spec.Courseware diff --git a/spec/Spec/Prelude.lean b/spec/Spec/Prelude.lean new file mode 100644 index 0000000..5c96fdf --- /dev/null +++ b/spec/Spec/Prelude.lean @@ -0,0 +1,37 @@ +/-! +# Prelude —— System 层共享标识符 + +平台层(`Spec.System`)反复引用一组**标识符**(项目、run、session、principal)。 +它们在 likec4 / ADR 里只作为引用键出现,**内部表示从未被决策**(是 UUID 还是 +复合键、principal 怎么分类),也不构成语义分歧点。 + +故把它们收口成一个 opaque 载体 `Identifiers`,System 各模块在其上参数化。这样 +契约谈得了"锁的 owner 是哪个 run""grant 授给哪个 principal"这类**关系**,却 +不对标识符的表示作任何承诺。 +-/ + +namespace Spec.System + +/-- +System 层标识符载体(`OPEN` 表示,关系结构 `PINNED`)。 + +每个字段是一个 opaque 类型:契约只用它做引用键,绝不假设其内部表示。System 各 +模块 `variable (I : Identifiers)` 后即可引用 `I.ProjectId` 等。 +-/ +structure Identifiers where + /-- 课程项目的标识(`OPEN` 表示;聚合根,见 likec4 `Project`)。 -/ + ProjectId : Type + /-- 一次 Claude 处理任务的标识(`OPEN` 表示;锁的 owner、审计主体,见 `AgentRun`)。 -/ + RunId : Type + /-- 长生命周期 Claude 会话的标识(`OPEN` 表示;跨多 run 复用,ADR-0002)。 -/ + SessionId : Type + /-- + 权限主体的标识(`OPEN` 表示及其**子类型学**)。 + + ADR-0004 列出 principal 可以是 user / feishu_chat / department / user_group / + app。这套子类型学本身**未定且非本层分歧点**(纯 plumbing),故此处只留 opaque + 键,不展开为 `inductive`。 + -/ + Principal : Type + +end Spec.System diff --git a/spec/Spec/System.lean b/spec/Spec/System.lean new file mode 100644 index 0000000..5659c01 --- /dev/null +++ b/spec/Spec/System.lean @@ -0,0 +1,19 @@ +import Spec.System.Run +import Spec.System.Lock +import Spec.System.Permission +import Spec.System.Audit + +/-! +# System —— Hub 平台层契约 + +协作与执行的平台:项目、飞书群、AgentRun、锁、权限、审计。`main` 分支的 likec4 +(`docs/architecture/likec4/`)已画出这一层的**结构**(9 实体 + 容器 + 视图);本层 +只补 likec4 画不出的**语义分歧点**,不重复结构: + +- `Run` —— AgentRun 状态与终止判定(状态集合完整性 OPEN)。 +- `Lock` —— 锁 owner=run(ADR-0002),及"持锁者必为非终止 run"的核心不变式。 +- `Permission` —— read⊂edit⊂manage 角色格、能力推导、单调性;force-release 在格外。 +- `Audit` —— 有意从简(内容多为 plumbing,OPEN)。 + +标识符见 `Spec.Prelude`。决策出处:ADR-0001..0004。 +-/ diff --git a/spec/Spec/System/Audit.lean b/spec/Spec/System/Audit.lean new file mode 100644 index 0000000..93da09d --- /dev/null +++ b/spec/Spec/System/Audit.lean @@ -0,0 +1,27 @@ +import Spec.Prelude + +/-! +# Audit —— 审计日志(有意从简) + +likec4 把 `AuditLog` 列为实体:`AgentRun -> AuditLog 'records lifecycle events'`, +admin 经控制台审计。但**审计记录里装什么**(事件 schema、保留策略、可查询维度) +在任何 ADR / 散文里都未决策,且大多是 plumbing——按分歧点测试**不入契约**:写明 +与否不会让开发者与 agent 各做不同假设。 + +故本模块**刻意几乎为空**:只固定一条已决策的关系——审计以 run 为主体记录其生命 +周期事件——其余 `OPEN`。这里留白本身是契约的一部分(承诺"此处尚无答案,勿填")。 +-/ + +namespace Spec.System + +/-- +审计条目的最小骨架(关系 `PINNED` / 内容 `OPEN`, likec4 `records lifecycle events`)。 + +只承诺"一条审计记录关联到某个 run"。事件类型、时间、actor、详情等字段**未定** +(`OPEN`),待出现真实分歧点(如"取消必须记录 actor")时再由对应 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 new file mode 100644 index 0000000..db26b85 --- /dev/null +++ b/spec/Spec/System/Lock.lean @@ -0,0 +1,51 @@ +import Spec.Prelude +import Spec.System.Run + +/-! +# Lock —— 项目锁与排他不变式 + +ADR-0002 的核心:防止并发 Claude 执行同时改一个项目,而锁的 **owner 是当前 +`AgentRun`**(不是 teacher / chat / session)。本模块把这条决策编码进类型,并钉死 +likec4 画不出的那条语义不变式——**持锁者必为非终止 run**。 +-/ + +namespace Spec.System + +variable (I : Identifiers) + +/-- +项目级锁(`PINNED`, ADR-0002)。 + +`owner` 的类型是 `RunId` 而非 `SessionId`/`Principal`——这从类型上编码 ADR-0002 +"lock owner = run_id":锁不可能被一个 session 或 teacher 持有。`scope` 为项目级 +(一个项目一把锁,见 `LockTable`)。 +-/ +structure ProjectAgentLock where + /-- 锁的作用域:项目级(`PINNED`, ADR-0002 `scope = project_id`)。 -/ + scope : I.ProjectId + /-- 锁的持有者:一个 run(`PINNED`, ADR-0002 `owner = run_id`)。 -/ + owner : I.RunId + +/-- +锁表:每个项目当前的持锁 run(`PINNED` 排他性, ADR-0002)。 + +`Option` 编码"每项目至多一把锁":`none` = 无活动 run 占用,`some r` = run `r` +正持有。这个 `ProjectId → Option RunId` 的结构**本身**即排他——不可能为同一项目 +登记两个并发 owner。 +-/ +def LockTable := I.ProjectId → Option I.RunId + +/-- +锁表良构:**持锁者必为非终止 run**(`PINNED` 平台核心不变式, ADR-0002)。 + +ADR-0002 说锁在 run 终止时释放。其逻辑等价物:任何时刻,若项目 `p` 的锁被 `r` +持有,则 `r` 不在终止态。`statusOf` 给出每个 run 的当前状态。 + +这条不变式把 **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 + +end Spec.System diff --git a/spec/Spec/System/Permission.lean b/spec/Spec/System/Permission.lean new file mode 100644 index 0000000..9edf44a --- /dev/null +++ b/spec/Spec/System/Permission.lean @@ -0,0 +1,99 @@ +import Spec.Prelude + +/-! +# Permission —— 角色、能力与授权 + +ADR-0004:权限走"飞书云文档式"——**协作者授权(grant)与操作设置(settings) +分离**;grant 是 `resource + principal + role`,role 取自封闭的 `read / edit / +manage`,且 **read ⊂ edit ⊂ manage** 累积赋能;强制释放锁是 **admin-only**,在 +role 体系之外。本模块把这套结构与"高 role 含低 role 全部能力"的单调性钉死。 +-/ + +namespace Spec.System + +/-- +协作者角色(`PINNED` 封闭, ADR-0004 逐字 "roles are read, edit, or manage")。 + +与 element-kind / RunState 不同,这里 ADR **明示**只有三个 role,故 `inductive` +是封闭授权,不是"尚未封闭"。 +-/ +inductive Role where + | read + | edit + | manage + +/-- +角色的**赋能层级**(`PINNED` 序, ADR-0004 read⊂edit⊂manage)。 + +把 ADR-0004 的累积包含关系数值化:read=0 ⊂ edit=1 ⊂ manage=2。它只服务于下面的 +`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-0004 对各 role 的展开:`view`(read);`discussComment` / +`editArtifact` / `triggerAgent` / `answerChoiceCard`(edit);`manageCollaborators` +/ `projectSettings` / `groupBinding` / `normalCancel`(manage)。 + +⚠ **完整性 OPEN**:这是 ADR 当前点名的能力,不保证穷尽;新增产品操作时可能扩。 +注意 **force-release 不在此列**——它是 admin-only override,见 `RequiresAdmin`。 +-/ +inductive Capability where + | view + | discussComment + | editArtifact + | triggerAgent + | answerChoiceCard + | manageCollaborators + | projectSettings + | groupBinding + | normalCancel + +/-- +某能力所**要求的最低角色**(`PINNED`, ADR-0004 各 role 的能力展开)。 + +read 级仅 `view`;edit 级是讨论/评论、编辑产物、触发 Claude、应答 choice card; +manage 级是协作者管理、项目设置、群绑定、常规取消。授权判定 `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 的累积性: +manage 自动具备所有 edit / read 能力,无需逐条列举。 +-/ +def Role.can (r : Role) (c : Capability) : Prop := c.requiredRole |>.le r + +/-- +**单调性**:角色越高,能力只增不减(`PINNED` 定理, ADR-0004 累积赋能)。 + +这是 read⊂edit⊂manage 的形式化保证:若 `r₁ ≤ r₂` 且 `r₁` 能做 `c`,则 `r₂` 也能。 +证明即偏序传递性——之所以成立得这么干净,正因为 `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)。 + +ADR-0004 明确:force release 卡住的锁是异常操作,不是任何协作者 role 的能力—— +即便 `manage` 也不经由 `Role.can` 获得它。故它不是一个 `Capability`,而是这样一个 +独立谓词:仅当主体是 admin 时成立。`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 new file mode 100644 index 0000000..ba7c1c8 --- /dev/null +++ b/spec/Spec/System/Run.lean @@ -0,0 +1,47 @@ +/-! +# Run —— AgentRun 状态机 + +一次 `@Claude` 创建一个 `AgentRun`(ADR-0001),它在生命周期里经历若干状态,并在 +**终止时释放项目锁**(ADR-0002)。本模块固定 run 的**状态**与**终止判定**——后者 +是 Lock 排他不变式(见 `Spec.System.Lock`)的依赖。 + +完整的合法转移关系**未在任何 ADR / likec4 散文里定下**,故本模块不臆造转移边, +只刻画状态本身与"何为终止"。 +-/ + +namespace Spec.System + +/-- +AgentRun 的运行状态(状态名 `PINNED` 取自 ADR-0001..0003 + likec4 散文; +**集合完整性 `OPEN`**)。 + +各状态来源:`active`(run 进行中)、`waitingForUser`(likec4 Run Orchestrator +"等待用户")、`completed` / `failed` / `timedOut` / `canceled`(ADR-0002 列出的 +释放锁时机)。 + +⚠ **完整性是 OPEN**:散文从未声明"状态恰好这些"。这里用 `inductive` 是为了能 +谈终止判定与不变式,**不等于**封闭授权——若实现侧发现还需要别的状态(如排队中 +的 pending),那是一个待 surface 的分歧点,**不得**默认本枚举已穷尽。这与 +element-kind 那种**明示开放**的宇宙性质不同:那里"开放"是决策,这里"未封闭"是 +尚未决策。 +-/ +inductive RunState where + | active + | waitingForUser + | completed + | failed + | timedOut + | canceled + +/-- +run 处于**终止态**(`PINNED`, ADR-0002)。 + +ADR-0002 钉死:锁在 run `completes / fails / times out / is canceled` 时释放。 +这四个状态即终止态;锁的释放时机由它定义(见 `Spec.System.Lock.LockTable.WellFormed`)。 +`active` 与 `waitingForUser` 非终止——后者虽在等待,run 仍占用项目(锁未释放)。 +-/ +def RunState.Terminal : RunState → Prop + | .completed | .failed | .timedOut | .canceled => True + | .active | .waitingForUser => False + +end Spec.System