Files
curriculum-project-hub/spec
sjfhsjfh f1dce07789 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>
2026-06-22 00:31:14 +08:00
..

spec —— Lean 语义母本

这是本 monorepo 的契约:产品各部件语义的上游参照,用 Lean 编写。它的定位与约束见仓库根 README.md 的"宪法"5 条——本文件只讲怎么往这份契约里写东西

现状

刚初始化的 Lean 工程(lake init),目前只有占位内容(Spec/Basic.lean)。实质领域内容(System 平台层、Courseware 产品层)将逐个概念加入,每个都遵循下面的规范。

构建

cd spec
lake build

工具链锁定在 lean-toolchain(leanprover/lean4:v4.31.0)。无外部依赖——Mathlib / Batteries 等留待第一个真正需要它的定理出现时再引入(依赖碰到再加)。

写作规范

双半契约:prose + type

每个 top-level 声明必须/-- … -/ doc 注释,用自然语言陈述其语义意图。两半缺一不可:

  • prose 半给人读——说清"这在领域里是什么、为什么"。
  • type 半给机器读、给 type checker 把关——保证结构无洞。

agent 不得用预训练先验脑补本领域(领域很新,无先验);prose 是 agent 理解语义的唯一权威来源。

标签分类法

在 doc 注释里用以下标签标注每条语义的状态:

  • PINNED —— 已解决的分歧点,契约在此处权威,双方据此对齐。
  • OPEN —— 故意未规定。双方均不得假设其解;实现遇到时必须 surface 出来讨论,而不是擅自决定。
  • ADR-NNNN —— 链接到根 docs/adr/ 下的对应决策记录(如 ADR-0002),交代该语义的决策出处。

分歧点测试(写之前先过一遍)

新增任何概念前,先问:"不写明,开发者与 agent 会不会各自做出不同假设?"

  • 会 → 它是分歧点,入契约。
  • 不会(显然的东西 / 纯 plumbing / 普通 CRUD 字段)→ 不入。

详见根 README 宪法第 5 条。

不用 sorry

无法陈述清楚的东西,用 OPEN 在 prose 里标注,而不是sorry 留一个假装成立的定理。sorry 会让 lake build 仍然变绿,却在契约里埋一个谎——这与"契约自包含、无洞"直接冲突。

命名

  • 模块 / 命名空间:PascalCase,对应分层,如 Spec.System.RunSpec.Courseware.Validity
  • 类型:PascalCase。
  • 谓词 / Prop:用意图清晰的命名,如 Legal…ValidTransitionCan…
  • 文件粒度:原则上"一个带独立不变式的概念一个文件"。