Files
curriculum-project-hub/docs/adr/0014-markdown-html-export-backend-direction.md
T
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

108 lines
5.7 KiB
Markdown
Raw Blame History

This file contains ambiguous Unicode characters
This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.
# 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:
1. **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.
2. **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.
3. **`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.
4. **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).