10 Commits

Author SHA1 Message Date
hongjr03 3f9b60f692 chore: remove Lean spec; ADRs are the single source of truth
The spec/ Lean semantic master had no conformance gate, no codegen, and
no CI tie to implementations — alignment was carried entirely by human
review, the same mechanism that carries the ADRs. In practice the ADRs
plus greppable code comments were already the load-bearing artifacts,
so spec/ was the most expensive kind of stale documentation.

- delete spec/ and the spec-check CI workflow
- README: constitution rewritten around ADRs as decision truth
- AGENTS.md/CLAUDE.md: discipline re-anchored (new decisions -> new ADR,
  never rewrite ADR history; supersede instead)
- code comments: re-anchor 'Mirrors Spec.X' invariants to ADR numbers
  (cph-diag, cph-check, cph-model, hub runner/capacity/org, prisma)
- leave ADR bodies and .scratch audit snapshots untouched (history);
  fix live references in open readiness tickets
2026-07-20 09:07:26 +00:00
hongjr03 5f791c5ce4 chore: restore checker CI gate 2026-07-10 13:46:22 +08:00
hongjr03 b0eedfab05 test(cph-model): isolate version fixtures 2026-07-10 02:33:12 +08:00
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
sjfhsjfh 144e2d8c80 feat(spec+checker): slides/逐字稿 markdown 内容面 + assembleMarkdown step(ADR-0015)
给课程加两个 markdown 内容面:slides(大纲:h2 part → h3 小节 → ![]() 图 +
:::widget 教具)与逐字稿(口播)。直接 markdown+KaTeX 撰写,绕开 typst→md
公式转换(等于在 slides 面选 ADR-0014 的 R2)。

spec:
- RichContent.lean: content leaf 带 format(typst|markdown),新增 ContentFormat
  归纳,RichContentRef 加 format 字段
- Export/Render.lean: Step 加 assembleMarkdown (field),钉执行语义
  (同 shell 三边界 + 注入课程 h1 + 自包含收集引用图)
- Courseware.lean: ADR 区间 →0015

实现:
- cph-schema: x-cph-content 支持 true→.typ / 字符串→该扩展名(.md);
  ContentField 带 ext;4 个 kind schema 各加可选 slides/transcript
- cph-model: Step::AssembleMarkdown{field} + manifest "assemble-markdown" 解析
- cph-check: run_markdown_assemble_target / target_is_markdown_assemble
  (照 run_shell_target 形状:check 门控、注入 h1、按 [[parts]] 序拼、写盘后
  收集 ![](rel) 引用图进 build 根使产物自包含、引用图缺失属 build-过程错误
  不入 6 类诊断);compile_targets 已 filter TypstCompile,纯 assemble 自然排除
- cph-cli: run_markdown_assemble_build 路由
- cph-typst: template_step 补 AssembleMarkdown => None 分支

测试:全 workspace 49 passed(新增 6 个 markdown 装配测试含图收集);
lake build 25 jobs 绿。

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-23 14:55:55 +08:00
sjfhsjfh 5dc29fe558 feat(model): author 是有序列表;Info(canonical) vs RawInfo(授权 surface) 入契约
一节课可多人署名(教研组),故 canonical author 是**有序列表**而非单值。on-disk
形式接受裸字符串(单作者)或数组(多作者),但此"字符串或数组"二态**只活在加载边界**:
RawInfo 经归一化折叠成 canonical Info,其后系统只见 List。

Lean 母本(ADR-0008 范围):新增 Model/Info.lean,把 Info(canonical,authors: List
String)与 RawInfo/RawAuthor(授权便利 surface)+ 归一化 RawInfo.toInfo 钉死——
canonical 接收端恒为列表,raw 形式不泄漏。ADR-0008 [info] 块补 author-as-list 决策。

impl 对齐:cph-model Info.author: Option<String> → authors: Vec<String>;RawAuthor
untagged enum(One|Many)+ into_vec 归一化;augmented manifest 发射 author 数组
(typst document(author:) 与模板已接受 string/array)。doc 两端互引 spec。

测试:load.rs 单作者→单元素列表;target-configs fixture 加数组作者断言多作者。
验证:lake build 绿(25 jobs);cargo test 全绿;clippy 静默;TH-141(单字符串作者)
check+build PDF 无回归。

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-23 00:11:03 +08:00
sjfhsjfh c684d25d50 chore(spec+checker): cleanup pass — trim docs, reorg Courseware, covers-as-data, fold DanglingReference (ADR-0012)
Spec母本噪音清理 + 一处 spec↔impl 对齐 + 一处契约自洽修正。

Part A — spec doc 瘦身:每条 doc 收到"语义点 + 标签 + ADR ref + 承载性 why",
把跨文件复读的方法论(element-kind 开放性对比、likec4 画不出、分歧点测试)上移到
module header。OPEN 框架保持清晰(RunState/Capability 完整性仍明示须 surface)。

Part B — Courseware/ 由 10 文件平铺重组为 Model/ Export/ Check/ Open/ 四子命名空间
(namespace Spec.Courseware 不变,零引用改动)+ 四个子 aggregator。lake build 绿(24 jobs)。

Part C — 渲染覆盖落为数据(ADR-0011 对齐):去掉 cph-check 里硬编码的
COVERED_TARGETS,改读 TargetConfig.covers。cph-model 新增 covers: Option<Vec<String>>
(None=未声明,由 cph-check 默认为全部 known kinds;显式 [] 表示不覆盖任何 kind)。
新增 3 个覆盖行为测试。

ADR-0012 — DanglingReference 退役(诊断 7→6 类):其两种情形(未解析 @ref、越界/缺失
相对 import)都是 typst 编译期失败,归 typstCompile。同步移除 Oracle.refsResolve
(被 compiles 蕴含),Legal 少一个合取项。impl 删去从未被发射的 DiagCode::DanglingReference,
闭合 named-but-unemitted 的 spec↔impl 缝。ADR-0010 加修订指针。

OPEN 点(RunState/Capability 完整性、QuestionBank、Course)按既定纪律保持 OPEN,本次
只改善其框架措辞,不决策。

验证:spec lake build 绿;cargo test 全绿(含新增覆盖测试);clippy 静默;
TH-141 check 0 errors/0 warnings 无回归。

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-22 23:59:32 +08:00
sjfhsjfh d5bce1bede feat(checker): cph-model manifest v2 — Artifact-with-fields + typed steps (WU-B', ADR-0011)
[targets.*] reworked: artifact is now an inline table with a type discriminator
({type="single-file",filepath} / {type="file-tree",root,outputs}) and steps is an
ordered array-of-tables ({type="typst-compile",template} / {type="shell",run}).
numbering removed entirely (presentation lives in the template per ADR-0011).

TargetConfig { name, artifact: Artifact, steps: Vec<Step> }; Artifact and Step
mirror Spec.Courseware.Artifact / Spec.Courseware.Step (doc-cited). Sensible
defaults so a bare [targets.student] still works: single-file build/<name>.pdf +
one typst-compile exports/<name>.typ. Malformed artifact/step type → non-fatal
SchemaViolation with fallback. 8 tests green.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-22 09:57:50 +08:00
sjfhsjfh b5bf9d60d1 feat(checker): cph-model — structured export-target build config (WU-B, ADR-0009)
manifest.toml [targets.*] upgraded from bare names to structured build configs.
Lesson.targets: Vec<String> → Vec<TargetConfig> { name, artifact, numbering }.
ArtifactKind { SingleFile, FileTree } mirrors Spec.Courseware.Artifact.
NumberingConfig.heading: Option<Vec<String>> — None means "use framework
default" (render package owns it), so absence is distinguishable from a value.
Empty [targets.x] body = all defaults, no diagnostics. Malformed config (bad
artifact value, non-array numbering.heading) → non-fatal SchemaViolation, target
kept with defaults. Enabled toml `preserve_order` so target declaration order is
real (the old Vec<String> never actually preserved order). target_names() helper
for call sites that only want names. 8 tests green.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-22 08:42:15 +08:00
sjfhsjfh c810ea6137 feat(checker): scaffold repo-root cargo workspace + cph-diag + cph-model (WU-1)
Stand up the Rust implementation of the rule-based checker (the thing that
"stands in Lean's position" at product runtime). Single repo-wide cargo
workspace at the repo root so future components (e.g. an exporter) can reuse
shared crates.

- workspace: 6 member crates under crates/; cph-schema/cph-typst/cph-check/
  cph-cli are stubs for later WUs that compile clean today.
- cph-diag: shared diagnostic vocabulary. Severity { Warning, Error } mirrors
  Spec.Courseware.Diagnostic.Severity exactly (two-valued, no info/note — a
  contract decision documented in-code since there's no CI gate for alignment).
  Closed DiagCode set with stable string forms; Diagnostic with optional span +
  fix hint; Display renders `error[CODE]: msg / --> file:line:col / hint: …`.
- cph-model: the ADR-0008 loader. Reads manifest.toml ([project]/[info]/ordered
  [[parts]]/[targets.*]) + each part's element.toml into an ordered Lesson
  (mirrors Lean `Lesson = List (Element P)`). Structure-only: cross-checks
  part.kind == element.toml kind, rejects `..` traversal; does NOT do schema
  validation (WU-3), content-file existence (WU-3), or typst (WU-4).
  `load(root) -> (Option<Lesson>, Vec<Diagnostic>)`: Some even on collectible
  part errors, None only on hard manifest failure.
- 13 tests (7 cph-diag, 6 cph-model incl. static fixtures doubling as format
  docs). build + test + clippy -D warnings + fmt --check all green.

Judgment call flagged for review: cph-diag has no ManifestMalformed code, so
manifest-structure errors map to SchemaViolation (TODO noted in-code).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-22 01:27:32 +08:00