curriculum-project-hub/spec

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.Agent.Run、Spec.Courseware.Validity。
• 类型:PascalCase。
• 谓词 / Prop:用意图清晰的命名,如 Legal…、ValidTransition、Can…。
• 文件粒度:原则上"一个带独立不变式的概念一个文件"。