3 Commits

Author SHA1 Message Date
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 d76f9f9a54 feat(checker): compile template as main, augmented manifest closes optional-content (WU-D', ADR-0011)
Replace generated-driver compilation with the template model.

cph-typst:
- driver.rs DELETED (generate_driver, static-include driver, numbering-threading).
- New manifest.rs: build_augmented_manifest(&Lesson) emits a TOML doc with [info]
  + ordered [[parts]] each carrying a `fields` array = the kind's content fields
  whose <root>/<path>/<field>.typ exists on disk. Reuses cph-schema's
  content_field_names (new dep; no cycle). This closes the OPEN point WU-C'
  surfaced: typst has no file-exists primitive, so the engine (which has disk
  access) tells the template which optional content (lemma proof) is present.
- World main = the real engineering-file template (<root>/<template>); the
  augmented manifest is served as an in-memory virtual file at /.cph/manifest.toml
  (never written to the tree), injected via sys.inputs.manifest. render_dir kept
  only for @local/cph-render + vendored @preview/numbly resolution.
- Artifact handling: SingleFile+TypstCompile compiles; FileTree, shell-only, and
  undeclared-target are blocking "deferred/not-declared" diagnostics (ADR-0011).
- Engine public signatures unchanged; LessonWorld::new takes template+manifest_src.

cph-check: no source change needed (only uses lesson.targets/target.name +
unchanged Engine methods); pipeline + Legal alignment intact.

Fixtures: mini gets exports/{student,teacher}.typ (from render/templates/) + v2
manifest + a second proof-less lemma to exercise optional content. render-stub
retired (tests use the real render/). Through-template PDFs offline: student 44KB,
teacher 56KB; proof-less lemma compiles clean (optional-content confirmed).
Workspace: fmt + clippy -D warnings + all tests green.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-22 10:05:03 +08:00
sjfhsjfh 7e76482a31 feat(checker): cph-typst — embed typst 0.15, driver-gen, compile, PDF (WU-4)
The heart of the pipeline. Embeds the typst 0.15 compiler as a library to
compile-check a lesson and export a PDF, with diagnostics mapped back to source
spans (the product's value).

- LessonWorld: a typst World over the engineering-file directory tree. vpath =
  real relative path (ADR-0007); the per-target driver is mounted in-memory as
  `main` (.cph/driver-<target>.typ, never written to disk); @local/cph-render is
  resolved from render_dir (CPH_RENDER_DIR / with_render_dir), no package install
  or network. Fonts via typst-kit FontStore (system CJK).
- Driver generation: from the manifest, per target — static root-relative
  `include` of each content file (⇒ module body content, ADR-0006), assembled
  into the frozen `display(info, target, parts)` call; optional lemma proof
  emitted only if proof.typ exists; example `source` scalar threaded through.
- Diagnostics: typst SourceDiagnostic (errors + warnings) → cph_diag::Diagnostic.
  0.15 DiagSpan handled via span.id() + WorldExt::range → file-relative
  SourceSpan with 1-based line/col; driver-internal spans re-pointed with a
  "generated driver" hint, never dropped. typst hints/trace carried through.
- Engine API: new / with_render_dir / compile_check / build_pdf.
- 6 tests incl. build_pdf_with_real_render — full World→driver→cph-render→PDF
  producing real PDF-1.7 output (student 42KB / teacher 54KB). clippy/fmt clean.

Also fixes render/typst.toml `compiler = ">=0.15.0"` → `"0.15.0"`: typst 0.15's
manifest parser rejects a `>=` comparator on the compiler field (the 0.14 CLU
WU-2 tested against was lenient). This unblocks loading the real render package.

Pinned: typst/typst-pdf/typst-syntax/typst-library/typst-layout/typst-kit =0.15.0.

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