Commit Graph

6 Commits

Author SHA1 Message Date
ecc92c9a87 docs(adr): cph 的 nested-manifest / batch-export 改号 0036/0037
上游 0029/0030 与本地 filelib 侧同号 ADR 相撞,cph 两份改到本地空闲号段,
代码锚点引用一并跟随。
2026-08-06 00:51:33 +08:00
hongjr03 9927d38c18 feat(cph): implement nested outline manifest and batch/combined export
ADR-0029 — nested outline manifest, supersedes ADR-0008's flat [[parts]]:
- cph-model: recursive loader over manifest.toml containers / element.toml
  leaves; Lesson.parts (pure elements, DFS order) + Lesson.outline (elements
  interleaved with section headings at their DFS-open position); rejects
  ambiguous/incomplete folders and root-vs-container table misplacement
- cph-diag: new DiagCode::ManifestMalformed for carrier-document structure
  errors (discharges an existing TODO)
- cph-typst: augmented manifest now serializes the outline (element/section
  entries) instead of a flat parts array
- render/lib.typ: render-lesson renders section headings at their depth
- examples/TH-141 migrated to 5 nested section containers + 3 root segments,
  byte-identical element order; smoke-verified via cph check/build + pdftotext

ADR-0030 — batch & combined export, extends ADR-0009/0011:
- cph build with no --target batches every declared target (repeatable
  --target for an explicit subset); any target failure => non-zero exit,
  per-target ledger, independent per-target execution
- cph-model: bundle.toml loader (directory + [info]/[targets.*]/ordered
  lessons with per-lesson target overrides)
- cph-typst: augmented bundle manifest (path-prefixed member outlines),
  Engine::{compile_check_bundle,build_bundle_pdf}
- render/lib.typ: render-bundle assembles member lessons under per-lesson
  headings, depth-shifts their own section headings, resets example/lemma
  counters at each lesson boundary by default
- cph-cli: `cph bundle <path> --target <name>` subcommand, same batching
  contract as `cph build`
- new bundle fixtures/tests (cph-model unit + cph-typst through-template PDF
  compile), smoke-verified via a real 2-lesson merged PDF

Verification: cargo fmt/clippy/test clean across the workspace (68 tests);
real cph check/build/bundle runs against TH-141 and a bundle fixture, PDF
content inspected via pdftotext.
2026-08-05 18:34:05 +08:00
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
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 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 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