Commit Graph

5 Commits

Author SHA1 Message Date
sjfhsjfh 4a9eb59aa9 feat(cli): cph completions <shell> 子命令(clap_complete)
用 clap_complete 4 给 cph 生成 shell 补全脚本(bash/zsh/fish/powershell/elvish)。
clap ValueEnum 枚举 Shell;run_completions 从 Cli::command() 派生,自动跟随
子命令/flag 演进。用法:`cph completions zsh > ~/.zfunc/_cph`。

- 依赖经 `cargo add clap_complete@4 -p cph-cli` 添加(4.6.5,默认 features 无额外依赖)
- README 补补全安装一节

测试:全 workspace 49 passed。

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-23 15:21:46 +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 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 b86ee24a26 feat(checker): cph-check orchestrator + cph-cli cph binary (WU-5)
Closes the core pipeline: the `cph` CLI checks an engineering file and compiles
a PDF.

cph-check — phases (a) load → (b) structural (known-kind set) → (c) schema →
(d) typst compile → (e) render-coverage. Compile is gated: skipped if (a)-(c)
produced any Error (broken input would only add noise); `check` compiles every
declared target (dedup identical diags), `build` compiles the one requested.
Render-coverage emits a non-blocking RenderIgnored *warning* when a (kind,
target) has no render rule — severity pinned via RENDER_IGNORED_SEVERITY const
citing spec Diagnostic.renderIgnoredSeverity + ADR-0005. No double-emit:
unknown/missing parts are skipped downstream. API: check(root, engine) ->
CheckReport, build(root, engine, target) -> (Option<pdf>, CheckReport).

cph-cli — clap: `cph check <path>` (exit 1 on any Error, warnings → 0) and
`cph build <path> --target <name> [-o out]` (default target student, default
out <path>/build/<target>.pdf). Diagnostics → stderr via Display, results →
stdout. --render-dir override.

End-to-end on examples/TH-141 (39 parts): `check` → 0 errors/0 warnings;
`build` → real PDF student 9pp/395KB, teacher 12pp/474KB. Broken-element check
(unclosed delimiter in a stmt.typ) → span-accurate
`error[E-TYPST-COMPILE]: unclosed delimiter --> lemmas/…/stmt.typ:7:8`, exit 1.
Workspace: fmt + clippy -D warnings + test all green.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-22 01:57:34 +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