forked from EduCraft/curriculum-project-hub

Files

T

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

5.7 KiB

Raw Permalink Blame History

ADR 0014: Direction For A Markdown / HTML Export Backend

Status

Proposed — design-only. This ADR fixes the direction and the key open decision for a future markdown/HTML export target; it does not implement a backend. No code or schema changes accompany it. (The 恒一小奥 lesson ships with student/teacher PDF targets and a kendoku-generated interactives target; a markdown/HTML analog is future work gated on the decision below.)

Builds on ADR-0009 (export targets are builds producing typed artifacts; "which markdown dialect … stays open") and ADR-0011 (presentation lives in the template; the manifest is injected). Relates to ADR-0013 (a non-typst backend could ride a shell step or earn a typed step — still open).

Context

The third-party 恒一小奥 deliverable was a slide-deck markdown bundle (lesson_slides.md). A recurring goal is to export an analog of such markdown/HTML from the same engineering file. The hard part is math: a curriculum is formula-heavy, and a markdown/HTML export that turns formulas into images (losing selectability, accessibility, and editability) is a regression. Three facts were established (web research + reading the pinned deps), and a fourth is the user's framing:

typlite (tinymist's markdown export) renders math as images and loses cross-references and styles — it goes through HTML as an intermediary. This is exactly the failure mode to avoid for a math-rich curriculum.
typst 0.15 native HTML export (the version this repo pins; typst-html 0.15 is already in Cargo.lock) emits equations as MathML. MathML is accessibility-oriented: selectable and screen-readable, but not trivially convertible to KaTeX/LaTeX, and rendering fidelity varies by browser.
mitex converts LaTeX → typst (an authoring-time import direction), not typst → LaTeX. So it is not, by itself, the typst-source → markdown lever; the user's instinct that "keep the formula source span and convert it" is right about what we want, but mitex's direction is the reverse of what a typst→markdown path needs.
The user's framing: the content a markdown/HTML target needs and the content the PDF 讲义/教案 need do not fully overlap — so whether a markdown/HTML export must reuse the same typst-content source, or instead draw on target-specific content, is genuinely open and is the pivotal design decision here.

Decision (direction, not implementation)

The pivotal open decision: shared source vs. target-specific content

Before any backend is built, decide: does the markdown/HTML target render the same per-element typst-content the PDF targets render, or does it consume target-specific content? This ADR does not pre-pick it; it names it as the gating decision and frames the two routes so the next round can choose deliberately (constitution rule 2 — surface, do not assume):

(R1) Shared typst-content. One source of truth; markdown/HTML is another projection of the same .typ. Requires a real typst-source → markdown/HTML converter that preserves math as editable markup. Highest reuse, hardest math story.
(R2) Target-specific content. The element carries (or the target supplies) content authored for the web medium. Decouples the hard typst→markdown math problem from the PDF path, at the cost of a second content surface to maintain.

Preferred math direction (whichever route is chosen)

Math must survive as markup, not images. The favored approach is to obtain each equation's source span from the typst AST and convert that span's source to LaTeX/KaTeX, rather than accept typlite's image rendering or 0.15's accessibility-MathML as the final form. Concretely, the next round should evaluate:

harvesting equation source spans via typst-syntax and emitting $…$ /$$…$$ (KaTeX-compatible) from the typst math source, and
studying tinymist's own conversion crate (typlite / cmarker) for reusable pieces — adopting what helps, but not its math-as-image fallback.

A small proof-of-concept scoped to this lesson (whose math is trivial — 8×, 2-, 12×) is the right first experiment: it exercises the pipeline end-to-end while sidestepping the hardest formula cases, and shows whether equations come out as text/KaTeX rather than images.

Backend mechanics, once the route is chosen

typst 0.15 HTML export is reachable today (typst-html 0.15 is a transitive dep; promotable to a direct dep) — usable for R1's HTML side.
A markdown (rather than HTML) artifact may post-process that HTML, or emit markdown directly from the AST — open, decided with the route.
Per ADR-0013, the backend may run as a typed step or a shell step; whether the non-typst backend earns its own typed Step constructor is still open.

Consequences

The export-backend work has an explicit gating decision (R1 vs. R2) and a pinned math principle (markup, not images), so the next round starts from a decision rather than a blank page.
No implementation, schema, or Lean change lands now — the contract is unchanged; this is a recorded design direction.
The PDF and interactives paths are unaffected and remain the lesson's shipping targets.

Open Questions / Deferred

R1 vs. R2 — the pivotal decision above; unresolved by design.
Concrete math conversion — span-harvest → KaTeX vs. reusing a tinymist crate; to be settled by the PoC.
Markdown dialect — which dialect/fenced-div conventions the markdown artifact targets (ADR-0009 left this open; still open).
Typed non-typst step — whether the backend rides Shell or earns a typed Step (ADR-0013 open question).

5.7 KiB Raw Permalink Blame History Unescape Escape