# curriculum-project-hub

教研生产的数字化解决方案。核心思路:课程像 DAW / 剪辑软件那样有一个结构化的工程文件;
LLM assistant 协助编辑它;一个 rule-based checker 校验其合法性并给出有用的诊断。

LLM 提效,但判不了一节课合不合法(它不能真去跑 typst、不能可靠地断言数据合不合
schema);checker 真跑工具、给确定性诊断,补上这块。两者一起才是完整闭环。目标是把教研
从一次性的文档,变成可累积、可校验、可复用的资产。

这是一个 monorepo。组织方式本身就表达了一条原则:`spec/` 是上游的语义母本,其余部件是
向它对齐的实现。

## 安装 `cph`

从源码安装(本仓库根目录):

```sh
cargo install --path crates/cph-cli --locked
```

`render` 包已嵌入二进制,装好后无需任何环境变量、不依赖源码树即可用。开发时可设
`CPH_RENDER_DIR` 指向 live `render/` 目录覆盖。

```sh
cph check <工程目录>                              # 校验合法性
cph build <工程目录> --target student -o build/student.pdf   # 渲讲义 PDF
cph completions zsh > ~/.zfunc/_cph               # shell 补全(可选)
```

工程文件根放一个 `.cph-version` 文件,声明它面向的 cph 版本;`cph` 加载时比对自身版本,
不相容则拒绝(版本契约,ADR-0016)。

## 仓库布局

`spec/` 是 Lean 语义母本(自包含 Lean 工程,见 `spec/README.md`);`crates/` 是实现
(rule-based checker,向 spec 对齐,见 `crates/README.md`);`render/` 是 typst 渲染包;
`examples/` 是样例工程文件;`docs/adr/` 是架构决策记录,被 spec 引用。

`spec/` 与实现部件物理分离、平级共存:谁是上游、谁向谁对齐,一眼可见。实现部件共用一个
仓库根的 cargo workspace,使基础 crate 能被未来部件复用。

## 宪法

这 5 条是 `spec/` 这份语义母本的定位与约束,是本仓库一切工作的前提。

1. **角色——Lean 是研发侧的上游参照。**
   `spec/` 用 Lean 写,是开发者和 coding assistant 共用的 spec 工具,用来沉淀产品各部件
   的语义。它不进产品运行时——运行时那个 checker 用什么技术实现还没定,但它的语义先在
   `spec/` 里固定下来。

2. **对齐机制——Lean 只做上游参照。**
   不做 extract / codegen,不派生 conformance test,CI 里没有 spec→实现的 gate。实现对齐
   spec,靠开发者 review 和 agent 巡逻 diff 这个人肉环节承载。(CI 里的 spec check 只验
   spec 自身能否 type-check,即契约内部良构,不是 spec↔实现对齐检查。)

3. **资产性——由核对纪律承载,无机器兜底。**
   这份仓库给的是精确、自洽、机器验过内部良构的语义共识,不是实现正确性的保证。spec 与
   实现是否一致,没有自动闸门,要靠人工或 coding assistant 不定期(或每次改动后)核对;
   坚持核对,它就是有用的参照,否则只会变成过期的文档。

4. **形态——它是人机共识的契约。**
   契约必须自包含:凡契约未明文规定的,开发者与 agent 双方都不该假设。这比"文档"严格——
   type checker 会逼这份契约在结构上无洞。

5. **深度判据——只收录分歧点。**
   一条语义该不该写进 Lean,取决于一句话:不写明,开发者与 agent 会不会各自做出不同
   假设?会,就进契约;显然的东西、纯基础设施、普通 CRUD 字段,不进(写进去只稀释信噪比、
   增加维护面)。深度上限不是 Lean 的表达力,而是你愿意在每次实现变更时手动回头同步的量。
   进了之后钉到多细,见 `spec/README.md` 的取舍判据。

## CI

每次 push / PR 在 `spec/` 下跑 `lake build`,确保契约始终 type-check 通过。这是良构 gate,
见宪法第 2 条。