4 Commits

Author SHA1 Message Date
sjfhsjfh 9590e15236 feat(checker+typst): 嵌入 render 使 cph 可 cargo install;实现 shell step 执行器(ADR-0013)
三件事,服务于"把恒一小奥 KenKen 课作者化为合法 native 工程文件"这条主线
(工程文件本身在 repo 外的 sibling playground,不入此提交):

1. cph-typst: 把 render/ 编译期嵌入二进制,`cargo install` 后开箱即用
   - build.rs 把 render/ 拷进 OUT_DIR,剔除 dev 自指符号链接 vendor/local-packages
     (否则 include_dir! 无限递归)
   - embedded.rs 用 include_dir! 嵌入,运行时按版本解压到 per-user cache dir
     (CPH_RENDER_DIR 仍优先作 dev override)
   - default_render_dir 不再用编译期 CARGO_MANIFEST_DIR 写死路径

2. cph-check + cph-cli: 实现 Step::Shell 执行器(此前仅占位)
   - run_shell_target: 跑 check 门控 → 以工程根为 cwd 执行 shell step,首非零退出即停
   - target_is_shell + CLI run_shell_build 路由;`check` 不跑 shell(结构校验只看 lesson)
   - compile_targets 只保留含 TypstCompile 的 target,纯 shell target 不走 typst 引擎
   - 语义:失败属 build-过程错误,不入 6 类诊断(taxonomy 保持 6,显式拒绝加 ShellStep 码)

3. spec + ADR: 在 Export/Render.lean 钉 shell step 执行语义 prose;
   ADR-0013(已实现)、ADR-0014(md/HTML 导出后端方向,Proposed/设计先行,未实现)

测试:全 workspace 42 passed(新增 4 个 shell 执行器测试);lake build 25 jobs 绿。

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-23 12:09:49 +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
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