forked from EduCraft/curriculum-project-hub
feat(spec): build out System layer and element schema model
Picture the whole framework, then pin the element-kind language layer. System platform layer — rebuild the semantics likec4 can't draw (ADR-0001..0004): - Prelude: opaque Identifiers carrier (ProjectId/RunId/SessionId/Principal) - System/Run: RunState + Terminal subset (set completeness left OPEN, no invented pending) - System/Lock: lock owner=run (typed), LockTable exclusivity, WellFormed invariant (a lock holder must be a non-terminal run — couples Lock and Run) - System/Permission: read<edit<manage role lattice, capability derivation, can_mono monotonicity theorem; force-release sits outside the lattice (admin-only) - System/Audit: intentionally thin (mostly plumbing, OPEN) Courseware product layer — split the single Lesson file into focused modules and fix doc tautology: Primitives / Element / Lesson / Render / Diagnostic, plus QuestionBank and Course skeletons (core relations OPEN, not invented). Diagnostic upgrades WarnsIgnored into a severity-tagged checker rule. Element schema + rich-content model (ADR-0006, ADR-0007): - docs/adr/0006: kind schema is declarative JSON Schema; field types are built-in scalars plus a `content` extension; a `content` value is typst source taken as module body; rich content must carry a VirtualPath (else click-to-jump and relative import break — verified against typst source); import boundary = within the engineering file + @package - docs/adr/0007: on-disk form is a real directory tree (agent/grep friendly); VirtualPath = real relative path; layout conventions deferred - spec/Courseware/RichContent: prose anchor for rich content (opaque VPath, RichContentRef); ElementData kept abstract — JSON/typst internals are implementation detail, not contract lake build green (18 jobs), no sorry, toolchain v4.31.0. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This commit is contained in:
@@ -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.
|
||||||
@@ -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".
|
||||||
@@ -1,3 +1,5 @@
|
|||||||
-- This module serves as the root of the `Spec` library.
|
-- This module serves as the root of the `Spec` library.
|
||||||
-- Import modules here that should be built as part of the library.
|
-- Import modules here that should be built as part of the library.
|
||||||
|
import Spec.Prelude
|
||||||
|
import Spec.System
|
||||||
import Spec.Courseware
|
import Spec.Courseware
|
||||||
|
|||||||
@@ -1,9 +1,26 @@
|
|||||||
|
import Spec.Courseware.Primitives
|
||||||
|
import Spec.Courseware.RichContent
|
||||||
|
import Spec.Courseware.Element
|
||||||
import Spec.Courseware.Lesson
|
import Spec.Courseware.Lesson
|
||||||
|
import Spec.Courseware.Render
|
||||||
|
import Spec.Courseware.Diagnostic
|
||||||
|
import Spec.Courseware.QuestionBank
|
||||||
|
import Spec.Courseware.Course
|
||||||
|
|
||||||
/-!
|
/-!
|
||||||
# Courseware —— 产品层契约(课程工程文件)
|
# Courseware —— 产品层契约(课程工程文件)
|
||||||
|
|
||||||
本层是护城河:课程"工程文件"的语义母本与合法性规则。当前只有 lesson 骨架
|
护城河:课程"工程文件"的语义母本与合法性规则。决策出处 ADR-0005 / 0006 / 0007。
|
||||||
(见 `Spec.Courseware.Lesson`,ADR-0005);题库、course 编排、完整合法性判定
|
|
||||||
等仍 `OPEN`,待各自 ADR 落定后逐个加入。
|
已填实(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 编排的规则。
|
||||||
-/
|
-/
|
||||||
|
|||||||
@@ -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。本文件当前不引入任何
|
||||||
|
承诺性声明。
|
||||||
|
-/
|
||||||
@@ -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
|
||||||
@@ -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
|
||||||
@@ -1,115 +1,21 @@
|
|||||||
|
import Spec.Courseware.Element
|
||||||
|
|
||||||
/-!
|
/-!
|
||||||
# Lesson —— 课程工程文件的母本模型(单节课)
|
# Lesson —— 单节课工程文件
|
||||||
|
|
||||||
本文件固定 ADR-0005 的骨架共识:一个**工程文件 = 一节课(lesson)**,
|
ADR-0005:一个工程文件 = 一节课,是 element 实例的**有序序列**。课程/单元不是工程
|
||||||
lesson 是**有类型 element 实例的有序序列**;element 实例 = kind 标签 + 符合该
|
文件,而是 lesson 的编排(见 `Spec.Courseware.Course`,OPEN)。
|
||||||
kind schema 的数据;export target 是对 lesson 的投影;渲染由一份
|
|
||||||
**(kind × target) 配置矩阵**承载。
|
|
||||||
|
|
||||||
本轮**只承诺关系结构**。所有尚未决定的基元(schema 怎么表示、kind 怎么定义、
|
|
||||||
render rule 的载荷长什么样)都收口进 `Primitives`,以抽象类型留白(`OPEN`),
|
|
||||||
契约因此对未定之物**零承诺**,同时仍 type-check 通过。完整的"合法 lesson"判定
|
|
||||||
亦未定;本轮只落 checker 的第一颗种子(缺渲染 ⇒ warning)。
|
|
||||||
-/
|
-/
|
||||||
|
|
||||||
namespace Spec.Courseware
|
namespace Spec.Courseware
|
||||||
|
|
||||||
/--
|
/--
|
||||||
契约基元载体(`PINNED` 关系结构 / `OPEN` 基元留白,`ADR-0005`)。
|
一节课(`PINNED`, ADR-0005)。
|
||||||
|
|
||||||
把本轮**尚未决定**的基元收口到一处,使 lesson 模型在其上参数化。每个字段都是
|
用 `List` 而非 `Multiset`/`Finset`,因为 **element 的先后次序承载教学语义**(讲义/
|
||||||
一个 `OPEN` 点:契约只声明它**存在**、以及它在关系中扮演的角色,绝不假设其内部
|
PPT 式的内容流,先讲定义再举例不同于反过来)。**不建模时长**:ADR-0005 决定 lesson
|
||||||
表示。具体表示待后续各自的 ADR 落定后再 refine。
|
是内容编排而非时间轴,故这里没有"每块多少分钟"这类字段——序是结构,时长不是。
|
||||||
-/
|
-/
|
||||||
structure Primitives where
|
abbrev Lesson (P : Primitives) := List (Element P)
|
||||||
/--
|
|
||||||
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
|
|
||||||
|
|
||||||
end Spec.Courseware
|
end Spec.Courseware
|
||||||
|
|||||||
@@ -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
|
||||||
@@ -0,0 +1,17 @@
|
|||||||
|
import Spec.Courseware.Element
|
||||||
|
|
||||||
|
/-!
|
||||||
|
# QuestionBank —— 题库(骨架,核心关系 OPEN)
|
||||||
|
|
||||||
|
题库是整个方案里与工程文件并列的资产(讨论里类比 DAW 的 sample library):有自身
|
||||||
|
结构的被建模实体,又是最典型的可复用单元,lesson 会引用它。
|
||||||
|
|
||||||
|
但**题库与 element 的关系尚未决策**,且用户明确指出"纯引用可能不够":
|
||||||
|
- element 内联题目数据(如交互教具那样),还是
|
||||||
|
- lesson 持一个指向题库条目的**引用**,还是
|
||||||
|
- 两者并存?
|
||||||
|
|
||||||
|
这是一个 `OPEN` 分歧点。按宪法第 2 条,本模块**不替它选解**——不建 `QuestionRef`
|
||||||
|
也不建内联结构,只在此 surface 该问题。待专门的 ADR 落定后再填。本文件当前只承载
|
||||||
|
这条说明,不引入任何承诺性声明。
|
||||||
|
-/
|
||||||
@@ -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
|
||||||
@@ -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
|
||||||
@@ -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
|
||||||
@@ -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。
|
||||||
|
-/
|
||||||
@@ -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
|
||||||
@@ -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
|
||||||
@@ -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
|
||||||
@@ -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
|
||||||
Reference in New Issue
Block a user