hongjr03
a0df8b6bcf
Two bugs were introduced when sendTextMessage was changed to auto-detect message format (text/post/interactive): 1. Message type mismatch: sendTextMessage could create a text or post message, but patchTextMessage only works on interactive cards. Fix: add sendInteractiveCardMessage for streaming create (always interactive, always patchable). 2. flushTextToSink state corruption: the text management after flush had a flawed appendedDuringFlush heuristic that could lose text or duplicate it. Fix: properly track sent vs unsent text by removing the sent prefix length, keeping only the last chunk for future patches. Also fix finish() to flush pending text regardless of currentMessageId.
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/ 这份语义母本的定位与约束,是本仓库一切工作的前提。
-
角色 —— Lean 是研发侧的上游参照。
spec/用 Lean 编写,是开发者(领域专家)与 coding agent 共用的 spec 工具,用来沉淀产品各部件的语义。它不进入产品运行时——产品里"站在 Lean 这个位置"的那个 checker 用什么技术实现,尚未决定;但那个东西的语义,先在spec/里固定下来。 -
对齐机制 —— Lean 只做上游参照。 不做 extract / codegen,不派生 conformance test,CI 里没有 spec→实现的 gate。实现对齐 spec,由"开发者 review + agent 巡逻 diff"这个人肉环节承载。 (CI 里的
spec check只验 spec 自身能否 type-check,即契约内部良构,不是 spec↔实现的对齐检查。) -
资产性 —— 由 review 纪律承载,无机器兜底。 这份仓库给你的是"精确、自洽、机器验内部良构的语义共识",不是"实现正确性保证"。spec 与实现之间那道缝,是我们自愿用人来守的——清醒地守,它就是资产;放任实现漂移而不回头同步,它就退化成最贵的过期文档。
-
形态 —— 它是人机共识的契约。 契约必须自包含:凡契约未明文规定的,开发者与 agent 双方都不该假设。这比"文档"严格——type checker 会逼这份契约在结构上无洞。
-
深度判据 —— 只收录分歧点。 一条语义该不该写进 Lean,取决于一句话:"不写明,开发者与 agent 会不会各自做出不同假设?" 会 → 进契约;显然的东西 / 纯 plumbing / 普通 CRUD 字段 → 不进(写进去只稀释信噪比、增加维护面)。 深度上限不是 Lean 的表达力,而是你愿意在每次实现变更时手动回头同步的量——写得比你能维护的更深,多出来的部分会率先过期、反过来误导实现。
CI
.gitea/workflows/spec-check.yml 在每次 push / PR 时于 spec/ 下跑 lake build,确保契约始终 type-check 通过(从第一天起就是"绿"的)。这是良构 gate,见宪法第 2 条。