bai/curriculum-project-hub
1
0
Fork 1
forked from EduCraft/curriculum-project-hub
Code Pull Requests Activity
Files
org-tenant-model
curriculum-project-hub/README.md
T
sjfhsjfh ebcb3a7589 feat(model+spec): .cph-version 契约文件 + CphVersionMismatch 诊断(ADR-0016);bump 0.0.2 
教研工程文件根放 .cph-version(内容=面向的 cph 版本)。cph 加载时比对自身版本
(CARGO_PKG_VERSION),不相容报 CphVersionMismatch error 并拒绝。当前判定为版本完全
相等(MVP);判定逻辑孤立在 versions_compatible 单谓词,后续可放宽为 semver 区间而
不动诊断分类/spec/CLI。

spec(7 类诊断,原 6 类):
- Diagnostic.lean: DiagKind 增 cphVersionMismatch(error 级),分类注释 6→7
- Pipeline.lean: load 阶段含 .cph-version 兼容性判定
- Courseware.lean: ADR 区间 →0016

实现:
- cph-diag: DiagCode::CphVersionMismatch("E-CPH-VERSION")
- cph-model: load() 解析 manifest 成功后 check_cph_version;versions_compatible
  谓词(完全相等);CPH_VERSION const。missing .cph-version 暂跳过(迁移期 OPEN);
  空文件报 error
- examples/TH-141、valid/mini fixture、KenKen 课各加 .cph-version=0.0.2

测试:cph-model 4 个版本门测试;全 workspace 53 passed;lake 25 jobs 绿。
负向验证:9.9.9 .cph-version → E-CPH-VERSION error + check 拒绝(exit 1)。

bump: workspace.package 0.0.1→0.0.2;cph --version 报 cph 0.0.2;README 同步
(含版本契约说明)。

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-23 16:03:54 +08:00

5.0 KiB
Raw Permalink Blame History

curriculum-project-hub

教研生产的数字化解决方案。核心思路:课程像 DAW / 剪辑软件那样有一个结构化的工程文件;coding agent 协助编辑它;一个 rule-based checker(类编译器)校验其合法性并给出 helpful fix hint。目标是把教研从一次性的文档,沉淀成可累积、可校验、可复用的资产。

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

安装 cph 命令行

当前版本 0.0.2。从源码安装(本仓库根目录):

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

render 包已嵌入二进制(build.rs 编译期拷入 + include_dir!),所以装好后无需任何环境变量、不依赖源码树即可用。渲染包按版本解压到 per-user cache(~/.cache/cph/render-<version>/ 或 macOS ~/Library/Caches/cph/...);开发时可设 CPH_RENDER_DIR 指向 live render/ 目录覆盖。

cph --version          # cph 0.0.2
cph check <工程目录>     # 校验合法性(7 类诊断)
cph build <工程目录> --target student -o build/student.pdf   # 渲讲义 PDF

版本契约(ADR-0016): 教研工程文件根放一个 .cph-version 文件,内容为它面向的 cph 版本(如 0.0.2)。cph 加载时比对自身版本,不相容则报 E-CPH-VERSION error 并拒绝(当前判定为版本完全相等;后续可放宽为 semver 区间,只改一处谓词)。examples/ 与本仓 fixture 已带该文件作为迁移起点;缺文件的工程暂时跳过此检查(OPEN)。

Shell 补全(可选):

cph completions zsh > ~/.zfunc/_cph        # 或 bash/fish/powershell/elvish

仓库布局

README.md          ← 本文件:总览 + 宪法(下面 5 条)
CLAUDE.md          ← 全局 agent 操作手册(管整个 repo)
docs/adr/          ← 系统级架构决策记录(跨部件,被 spec 契约引用)
spec/              ← Lean 语义母本(自包含的 Lean 工程)。见 spec/README.md
Cargo.toml         ← 仓库级 cargo workspace(实现部件共用,便于跨部件复用 crate)
crates/            ← 实现:rule-based checker(向 spec 对齐)。见 crates/README.md
  cph-diag / cph-model / cph-schema / cph-typst   ← 可复用基础(模型/校验/typst 引擎)
  cph-check / cph-cli                             ← checker 本体 + `cph` 命令行
render/            ← typst 渲染包 cph-render(母本的渲染后端之一,ADR-0005)
examples/          ← 样例工程文件(如 TH-141),流水线的真实输入
(hub/ exporter/ …) ← 将来的其他部件,平级于 spec/。尚未创建

spec/ 与实现部件物理分离、平级共存:谁是上游、谁向谁对齐,一眼可见。 实现部件共用一个仓库根的 cargo workspace,使基础 crate(模型、typst 引擎)能被 未来部件(如 exporter)复用,而非各自重造。

宪法

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

  1. 角色 —— Lean 是研发侧的上游参照。 spec/ 用 Lean 编写,是开发者(领域专家)与 coding agent 共用的 spec 工具,用来沉淀产品各部件的语义。它不进入产品运行时——产品里"站在 Lean 这个位置"的那个 checker 用什么技术实现,尚未决定;但那个东西的语义,先在 spec/ 里固定下来。

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

  3. 资产性 —— 由 review 纪律承载,无机器兜底。 这份仓库给你的是"精确、自洽、机器验内部良构的语义共识",不是"实现正确性保证"。spec 与实现之间那道缝,是我们自愿用人来守的——清醒地守,它就是资产;放任实现漂移而不回头同步,它就退化成最贵的过期文档。

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

  5. 深度判据 —— 只收录分歧点。 一条语义该不该写进 Lean,取决于一句话:"不写明,开发者与 agent 会不会各自做出不同假设?" 会 → 进契约;显然的东西 / 纯 plumbing / 普通 CRUD 字段 → 不进(写进去只稀释信噪比、增加维护面)。 深度上限不是 Lean 的表达力,而是你愿意在每次实现变更时手动回头同步的量——写得比你能维护的更深,多出来的部分会率先过期、反过来误导实现。

CI

.gitea/workflows/spec-check.yml 在每次 push / PR 时于 spec/ 下跑 lake build,确保契约始终 type-check 通过(从第一天起就是"绿"的)。这是良构 gate,见宪法第 2 条。

View Git Blame Copy Permalink