forked from bai/curriculum-project-hub
sjfhsjfh
3a22669f0a
- spec/: freshly initialized Lean library project (lake init, v4.31.0), no deps - .gitea/workflows/spec-check.yml: CI running lake build on spec/ (well-formedness gate, not a spec-to-impl gate) - README.md: monorepo overview + the 5 "constitution" rules positioning spec/ as upstream semantic master - CLAUDE.md: global agent manual - spec/README.md: contract writing conventions (prose+type, PINNED/OPEN/ADR tags, no sorry) - docs/adr/0001-0004: system-level decision records (retrieved from main) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
56 lines
2.4 KiB
Markdown
56 lines
2.4 KiB
Markdown
# spec —— Lean 语义母本
|
|
|
|
这是本 monorepo 的**契约**:产品各部件语义的上游参照,用 Lean 编写。它的定位与约束见仓库根 `README.md` 的"宪法"5 条——本文件只讲**怎么往这份契约里写东西**。
|
|
|
|
## 现状
|
|
|
|
刚初始化的 Lean 工程(`lake init`),目前只有占位内容(`Spec/Basic.lean`)。实质领域内容(System 平台层、Courseware 产品层)将逐个概念加入,每个都遵循下面的规范。
|
|
|
|
## 构建
|
|
|
|
```sh
|
|
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.Run`、`Spec.Courseware.Validity`。
|
|
- **类型**:PascalCase。
|
|
- **谓词 / `Prop`**:用意图清晰的命名,如 `Legal…`、`ValidTransition`、`Can…`。
|
|
- **文件粒度**:原则上"一个带独立不变式的概念一个文件"。
|