forked from bai/curriculum-project-hub
sjfhsjfh
9590e15236
三件事,服务于"把恒一小奥 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>
73 lines
4.2 KiB
Lean4
73 lines
4.2 KiB
Lean4
import Spec.Courseware.Model.Primitives
|
|
import Spec.Courseware.Export.Artifact
|
|
|
|
/-!
|
|
# Render —— export target = artifact + 有序 typed steps(ADR-0009 / 0011)
|
|
|
|
ADR-0009:export target 是一次 build,产出一个有类型的 `Artifact`。ADR-0011 钉死 build
|
|
的**形状**:一个 target 是 `artifact` + 一串**有序 typed step**。
|
|
|
|
- `typstCompile template` —— 把**模板文件**(如 `exports/student.typ`)编译成产物。它是
|
|
*typed* 而非裸 shell,正因框架要把 **manifest 注入**模板(经 `--input manifest=…`),
|
|
裸字符串表达不了这个 wiring。presentation(编号、样式)住模板里,不在 manifest。
|
|
- `shell run` —— 逃生口,给难以声明的步骤(ADR-0005 的 (b) 类 medium-only)。
|
|
|
|
**渲染覆盖**:ADR-0011 废止了 per-target `RenderRule` 载荷——渲染的"how"已移进模板。
|
|
契约只保留覆盖声明 `covers`(该 target 渲染哪些 kind),供种子诊断用。
|
|
|
|
**shell step 的执行语义(ADR-0013)。** `shell` 不再只是占位:它**会被执行**,语义是把
|
|
`run` 交给平台 shell、以**工程根为工作目录**运行,产物由被调外部工具自己写出(框架不装配
|
|
内容)。三条边界是真分歧点,故钉契约:
|
|
1. **opt-in by construction** —— 任意命令执行只在用户**显式** build 一个 shell target 时发生,
|
|
绝不在 `check` 里跑。`check` 只校验结构(lesson 是否合法),不执行外部工具、不验其产物。
|
|
2. **失败归属** —— shell step 退出非零是一次 **build-过程失败**,不是 lesson 的合法性缺陷;
|
|
因此它**不**进 `Diagnostic` 的 6 类(那 6 类是 lesson 自身的诊断,见 `Check/Diagnostic.lean`),
|
|
而由 build 执行层报告。诊断分类保持 6 类不变(ADR-0013 显式拒绝新增 `ShellStep` 诊断码)。
|
|
3. **非-typst target 不过 typst 编译** —— 一个只含 `shell` step 的 target(教具包即此)由
|
|
执行器跑命令,而非走 typst 引擎;`check` 的 compile 阶段跳过它。
|
|
-/
|
|
|
|
namespace Spec.Courseware
|
|
|
|
variable (P : Primitives)
|
|
|
|
/-- 一个 build **step**(`PINNED` typed, ADR-0011;可扩展)。MVP 仅一个 `typstCompile`;
|
|
`steps` 是 list 因为 FileTree / 第三方 build 会需多步。刻意不把模板内部、shell 命令的
|
|
解析结构写进来(实现细节, ADR-0011 OPEN)。 -/
|
|
inductive Step where
|
|
/-- 编译模板文件 `template`(相对工程根)成产物;框架注入 manifest。typed 的理由:
|
|
注入这件事裸 shell 写不出。 -/
|
|
| typstCompile (template : String)
|
|
/-- shell 逃生口:执行命令 `run`(ADR-0005 (b) 类落这)。**已实现**(ADR-0013):以工程根
|
|
为 cwd 执行,opt-in(只在显式 build 该 target 时跑,`check` 不跑),失败属 build-过程错误
|
|
而非 lesson 诊断。教具包(如 KenKen 交互 HTML 由外部 `kendoku` 生成)即走此 step。 -/
|
|
| shell (run : String)
|
|
|
|
/-- 一个 export target 的 build 规格(`PINNED` artifact + 有序 steps, ADR-0011)。 -/
|
|
structure TargetSpec where
|
|
/-- 产物(带字段, ADR-0011)。决定 build 折叠成单文件还是文件树。 -/
|
|
artifact : Artifact
|
|
/-- **有序** build steps。按序执行;MVP 仅一个 `typstCompile`。 -/
|
|
steps : List Step
|
|
/-- **覆盖声明**:`covers k` 表示此 target 渲染 kind `k`。ADR-0011 把旧
|
|
`renders : KindId → Option RenderRule` 降级后的产物——契约只声明"渲染哪些 kind"
|
|
(种子诊断 `renderIgnored` 用),"how"由 `steps` 的模板实现。 -/
|
|
covers : P.KindId → Prop
|
|
|
|
/-- 渲染配置(`PINNED` target-中心, ADR-0009/0011)。`spec t = none` 表示 target `t`
|
|
未声明(不导出);`some s` 给出其 build 规格。 -/
|
|
structure RenderConfig where
|
|
/-- target ↦ 该 target 的 build 规格(未声明则 `none`)。 -/
|
|
spec : P.TargetId → Option (TargetSpec P)
|
|
|
|
/-- kind `k` 在 target `t` 下**被渲染**(`PINNED`, ADR-0009/0011;承接 ADR-0005)。成立
|
|
⟺ `t` 已声明(`spec t = some s`)**且** `s.covers k`。为假即"此 kind 在此 target 下不
|
|
被渲染"——checker 据此报 warning(见 `Diagnostic.renderIgnored`)。`P` 隐式以便点记法。 -/
|
|
def RenderConfig.covers {P : Primitives} (c : RenderConfig P)
|
|
(k : P.KindId) (t : P.TargetId) : Prop :=
|
|
match c.spec t with
|
|
| none => False
|
|
| some s => s.covers k
|
|
|
|
end Spec.Courseware
|