diff --git a/crates/cph-check/src/lib.rs b/crates/cph-check/src/lib.rs index 90e6dc3..80680c8 100644 --- a/crates/cph-check/src/lib.rs +++ b/crates/cph-check/src/lib.rs @@ -17,15 +17,11 @@ use cph_typst::Engine; /// The default render target when a lesson declares no `[targets.*]` at all. const DEFAULT_TARGET: &str = "student"; -/// The render targets the MVP render package actually covers (student handout + -/// teacher plan). Used by the render-coverage rule (phase (e)). -const COVERED_TARGETS: &[&str] = &["student", "teacher"]; - /// Severity of the render-coverage ("element ignored under a target") diagnostic. /// /// **PINNED to `warning` by the contract.** Mirrors the Lean master's /// `Spec.Courseware.renderIgnoredSeverity : Severity := .warning` -/// (`spec/Spec/Courseware/Diagnostic.lean`), itself citing ADR-0005: when a +/// (`spec/Spec/Courseware/Check/Diagnostic.lean`), itself citing ADR-0005: when a /// `(kind, target)` pair has no render rule the checker reports that the element /// is ignored under that target and **does not block the export**. Naming the /// severity as a const makes "it is a warning, not an error" a greppable, @@ -62,7 +58,7 @@ impl CheckReport { /// Whether any collected diagnostic is `Error`-severity. /// /// **Legality decision (spec alignment).** `!has_errors()` is the - /// implementation of `Spec.Courseware.Legal` (`spec/Spec/Courseware/Diagnostic.lean`): + /// implementation of `Spec.Courseware.Legal` (`spec/Spec/Courseware/Check/Diagnostic.lean`): /// a lesson is *legal* iff its diagnostics contain no error-level diagnostic /// (warnings are non-blocking — see `Severity` / ADR-0010). There is no CI /// gate enforcing this alignment (repo constitution); it is kept greppable @@ -93,7 +89,8 @@ impl CheckReport { /// declared `lesson.targets` (defaulting to `"student"` if none), deduping /// identical diagnostics across targets. /// - **(e) render-coverage** — a `warning` (never an error) for each -/// `(kind, target)` lacking a render rule. Runs regardless of (d) gating. +/// `(kind, target)` the target's `covers` declaration does not include. Runs +/// regardless of (d) gating. /// /// The engine is taken as a parameter so the caller owns it (and tests can /// inject `Engine::with_render_dir`). @@ -259,14 +256,17 @@ fn compile_targets(lesson: &cph_model::Lesson) -> Vec<&str> { } /// Phase (e): for each `(part.kind, target)` over the lesson's declared targets, -/// emit a `RenderIgnored` **warning** when the pair has no render rule. +/// emit a `RenderIgnored` **warning** when the target does not cover that kind. /// -/// The render matrix lives in the render package and is not introspectable from -/// Rust in the MVP, so coverage is defined operationally: a kind is covered when -/// it is a known stdlib kind (`known`) AND the target is one the render package -/// handles (`COVERED_TARGETS` = student/teacher). A declared target outside that -/// set, or a kind not in the known set, yields the warning. Parts already broken -/// in (b) (missing folder / unknown kind) are skipped — they are reported there. +/// Coverage is the per-target **declaration** ADR-0011 pinned (and the spec's +/// `RenderConfig.covers k t` in `Export/Render.lean`): a target's +/// `cph_model::TargetConfig::covers` lists the kinds it renders. A used kind not +/// in that list draws the warning. An **absent** `covers` (the loader's `None`) +/// is resolved here — the orchestrator owns the kind universe via `cph-schema` — +/// to "covers all known kinds", so an undeclared target is fully covering rather +/// than covering nothing. (An explicit `covers = []` stays empty: it covers +/// nothing on purpose.) Parts already broken in (b) (missing folder / unknown +/// kind) are skipped — they are reported there. fn render_coverage(lesson: &cph_model::Lesson, known: &[&str]) -> Vec { let mut out = Vec::new(); // De-dupe (kind, target) pairs so we emit one warning per pair, not per part. @@ -278,7 +278,13 @@ fn render_coverage(lesson: &cph_model::Lesson, known: &[&str]) -> Vec true, + Some(kinds) => kinds.iter().any(|k| k == &part.kind), + }; if covered { continue; } @@ -290,12 +296,12 @@ fn render_coverage(lesson: &cph_model::Lesson, known: &[&str]) -> Vec = report + .diagnostics + .iter() + .filter(|d| d.code == DiagCode::RenderIgnored) + .collect(); + assert_eq!( + render_ignored.len(), + 1, + "expected exactly one RenderIgnored warning, got: {:#?}", + report.diagnostics + ); + // It is a non-blocking warning, so legality is unaffected by it. + assert_eq!( + report.warning_count(), + 1, + "the coverage gap is a warning: {:#?}", + report.diagnostics + ); + cleanup(&tmp); +} + +#[test] +fn covers_including_used_kind_has_no_render_ignored() { + // A target that covers `segment` (the only used kind) → no RenderIgnored. + let tmp = tempdir(); + write_segment_lesson_with_target( + &tmp, + r#"[targets.handout] +artifact = { type = "single-file", filepath = "build/handout.pdf" } +covers = ["segment"] +[[targets.handout.steps]] +type = "typst-compile" +template = "exports/handout.typ" +"#, + ); + + let report = cph_check::check(&tmp, &engine()); + assert!(report.lesson_loaded); + assert!( + !report + .diagnostics + .iter() + .any(|d| d.code == DiagCode::RenderIgnored), + "a covering target should yield no RenderIgnored, got: {:#?}", + report.diagnostics + ); + cleanup(&tmp); +} + +#[test] +fn absent_covers_defaults_to_full_coverage() { + // No `covers` key at all → the orchestrator defaults to all known kinds, so + // even a non-"student"/"teacher" target name covers `segment`. (This is the + // behavior change: coverage now follows the declaration/default, not a + // hardcoded target-name allowlist.) + let tmp = tempdir(); + write_segment_lesson_with_target( + &tmp, + r#"[targets.handout] +artifact = { type = "single-file", filepath = "build/handout.pdf" } +[[targets.handout.steps]] +type = "typst-compile" +template = "exports/handout.typ" +"#, + ); + + let report = cph_check::check(&tmp, &engine()); + assert!(report.lesson_loaded); + assert!( + !report + .diagnostics + .iter() + .any(|d| d.code == DiagCode::RenderIgnored), + "an absent `covers` defaults to full coverage, got: {:#?}", + report.diagnostics + ); + cleanup(&tmp); +} + // --- tiny temp-dir helpers (no external dev-dep) ------------------------------ fn tempdir() -> PathBuf { diff --git a/crates/cph-diag/src/lib.rs b/crates/cph-diag/src/lib.rs index c6fabd7..d7d7224 100644 --- a/crates/cph-diag/src/lib.rs +++ b/crates/cph-diag/src/lib.rs @@ -18,7 +18,7 @@ use serde::Serialize; /// Severity of a diagnostic. /// /// **Mirrors `Spec.Courseware.Diagnostic.Severity`** in the Lean semantic -/// master (`spec/Spec/Courseware/Diagnostic.lean`), whose definition is +/// master (`spec/Spec/Courseware/Check/Diagnostic.lean`), whose definition is /// exactly: /// /// ```text @@ -76,12 +76,15 @@ pub enum DiagCode { UnknownKind, /// A required `content` `.typ` file (per the kind schema) is missing. MissingContentFile, - /// A reference (e.g. a relative import or cross-element link) does not - /// resolve. - DanglingReference, /// Instance data does not conform to its kind's JSON Schema. SchemaViolation, - /// A typst source failed to compile. + /// The assembled typst source failed to compile. + /// + /// Includes **reference-resolution** failures — an unresolved cross-reference + /// (`@ref`) or a relative `import`/`include` that escapes the import boundary + /// or names a missing file. typst detects all of these at compile time, so + /// they surface here rather than as a separate diagnostic (ADR-0012 folded + /// the former `DanglingReference` class into this one). TypstCompile, /// An element is ignored under a render target (ADR-0005: warning). RenderIgnored, @@ -97,7 +100,6 @@ impl DiagCode { DiagCode::PartPathMissing => "E-PART-PATH", DiagCode::UnknownKind => "E-UNKNOWN-KIND", DiagCode::MissingContentFile => "E-MISSING-CONTENT", - DiagCode::DanglingReference => "E-DANGLING-REF", DiagCode::SchemaViolation => "E-SCHEMA", DiagCode::TypstCompile => "E-TYPST-COMPILE", DiagCode::RenderIgnored => "W-RENDER-IGNORED", diff --git a/crates/cph-model/src/lib.rs b/crates/cph-model/src/lib.rs index 8d9b6f4..893c7e1 100644 --- a/crates/cph-model/src/lib.rs +++ b/crates/cph-model/src/lib.rs @@ -4,7 +4,7 @@ //! `/manifest.toml` (project / info / ordered `[[parts]]` / declared //! `[targets.*]`) and each part's `//element.toml`, and produces an //! ordered [`Lesson`] — mirroring the Lean master's `Lesson = List (Element P)` -//! (`spec/Spec/Courseware/Lesson.lean`), where the order of `parts` carries +//! (`spec/Spec/Courseware/Model/Lesson.lean`), where the order of `parts` carries //! teaching semantics. //! //! Scope boundaries (deliberately staying in lane): @@ -72,6 +72,9 @@ impl Lesson { /// - A target with **no `steps`** defaults to a single /// [`Step::TypstCompile`] with `template = "exports/.typ"` (the /// framework's stock per-target template). +/// - A target with **no `covers`** key leaves [`TargetConfig::covers`] `None`, +/// meaning "coverage not declared". The consumer (`cph-check`) resolves that +/// to the full known-kind universe — see the field doc. #[derive(Debug, Clone, PartialEq, Eq, Serialize)] pub struct TargetConfig { /// Target name, e.g. `"student"` (the `[targets.]` table key). @@ -82,12 +85,25 @@ pub struct TargetConfig { /// The ordered build steps. Defaults to a single [`Step::TypstCompile`] /// with template `exports/.typ` when no `[[steps]]` are given. pub steps: Vec, + /// The **render-coverage declaration**: which element kinds this target + /// renders. Realizes `Spec.Courseware.TargetSpec.covers : KindId → Prop` + /// (`spec/Spec/Courseware/Export/Render.lean`) and ADR-0011's "render + /// coverage is a declaration, not a payload": the contract keeps *which + /// kinds a target renders* (used by the `renderIgnored` seed diagnostic), + /// while the rendering "how" lives in the template/steps. + /// + /// `Some(kinds)` is the explicit manifest list (`covers = ["segment", …]`). + /// `None` means the `covers` key was **absent**; the loader does not own the + /// kind universe (it must not depend on `cph-schema`), so it records the + /// absence and lets `cph-check` default it to all known kinds. An empty + /// `Some(vec![])` is distinct: a target that explicitly covers nothing. + pub covers: Option>, } /// The artifact an export target produces (ADR-0009/0011). /// /// **Mirrors `Spec.Courseware.Artifact`** in the Lean semantic master -/// (`spec/Spec/Courseware/Artifact.lean`), whose definition is exactly: +/// (`spec/Spec/Courseware/Export/Artifact.lean`), whose definition is exactly: /// /// ```text /// inductive Artifact where @@ -141,7 +157,7 @@ impl Artifact { /// One typed build step (ADR-0011). /// /// **Mirrors `Spec.Courseware.Step`** in the Lean semantic master -/// (`spec/Spec/Courseware/Render.lean`), whose definition is exactly: +/// (`spec/Spec/Courseware/Export/Render.lean`), whose definition is exactly: /// /// ```text /// inductive Step where @@ -572,6 +588,7 @@ fn parse_target(name: String, value: toml::Value, diags: &mut Vec) - return TargetConfig { artifact: Artifact::default_for(&name), steps: vec![Step::default_for(&name)], + covers: None, name, }; } @@ -587,10 +604,78 @@ fn parse_target(name: String, value: toml::Value, diags: &mut Vec) - Some(value) => parse_steps(&name, value, diags), }; + let covers = match table.remove("covers") { + None => None, + Some(value) => parse_covers(&name, value, diags), + }; + TargetConfig { name, artifact, steps, + covers, + } +} + +/// Parse a target's optional `covers` array into the render-coverage declaration +/// (ADR-0011). Each entry is a kind name (a string). A non-array `covers`, or any +/// non-string entry, is reported as a [`DiagCode::SchemaViolation`]; in that case +/// the declaration falls back to `None` ("not declared"), so `cph-check` defaults +/// it to the full known-kind universe rather than silently covering nothing. +/// +/// A well-formed but empty `covers = []` yields `Some(vec![])`: a target that +/// explicitly renders no kind (every used kind then draws a `renderIgnored` +/// warning) — distinct from an absent key. +fn parse_covers(name: &str, value: toml::Value, diags: &mut Vec) -> Option> { + let items = match value { + toml::Value::Array(items) => items, + _ => { + diags.push( + Diagnostic::error( + DiagCode::SchemaViolation, + format!( + "target '{name}' has a non-array `covers`; declare it as a list of \ + kind names, e.g. `covers = [\"segment\", \"example\"]`" + ), + ) + .with_hint("set `covers` to an array of kind-name strings, or omit it"), + ); + return None; + } + }; + + let mut kinds = Vec::with_capacity(items.len()); + for item in items { + match item { + toml::Value::String(s) => kinds.push(s), + other => { + diags.push( + Diagnostic::error( + DiagCode::SchemaViolation, + format!( + "target '{name}' has a non-string entry in `covers`: {}", + json_like_type(&other) + ), + ) + .with_hint("each `covers` entry is a kind name (a string)"), + ); + return None; + } + } + } + Some(kinds) +} + +/// A short type label for a TOML value, for the `covers` non-string diagnostic. +fn json_like_type(v: &toml::Value) -> &'static str { + match v { + toml::Value::String(_) => "string", + toml::Value::Integer(_) => "integer", + toml::Value::Float(_) => "float", + toml::Value::Boolean(_) => "boolean", + toml::Value::Datetime(_) => "datetime", + toml::Value::Array(_) => "array", + toml::Value::Table(_) => "table", } } diff --git a/crates/cph-typst/tests/compile.rs b/crates/cph-typst/tests/compile.rs index 540feaa..b4f2e2a 100644 --- a/crates/cph-typst/tests/compile.rs +++ b/crates/cph-typst/tests/compile.rs @@ -211,6 +211,7 @@ fn file_tree_artifact_is_deferred() { steps: vec![Step::TypstCompile { template: PathBuf::from("exports/web.typ"), }], + covers: None, }], root: fixture_root(), }; @@ -248,6 +249,7 @@ fn shell_only_target_is_deferred() { steps: vec![Step::Shell { run: "echo hi".into(), }], + covers: None, }], root: fixture_root(), }; diff --git a/docs/adr/0010-diagnostics-legal-lesson-and-check-pipeline.md b/docs/adr/0010-diagnostics-legal-lesson-and-check-pipeline.md index 7b601e4..55bd298 100644 --- a/docs/adr/0010-diagnostics-legal-lesson-and-check-pipeline.md +++ b/docs/adr/0010-diagnostics-legal-lesson-and-check-pipeline.md @@ -7,6 +7,13 @@ ADR-0005 explicitly deferred ("the complete definition of a legal lesson; this ADR fixes only the one seed rule"). Builds on ADR-0005's seed (missing render ⇒ warning) and ADR-0009 (target = build). Some items deferred; see *Open Questions*. +> **Corrected by ADR-0012.** The taxonomy below lists *seven* classes including +> `DanglingReference`. ADR-0012 retires `DanglingReference` — its cases +> (unresolved `@ref`, out-of-boundary `import`) are all typst compile-time +> failures, so they fold into `TypstCompile` — leaving *six* classes, and removes +> the `Oracle.refsResolve` conjunct from `Legal`. Read the taxonomy and the +> `Legal` definition here through that correction. + ## Context The checker is the product's moat — the thing that "stands in Lean's position" at diff --git a/docs/adr/0012-fold-dangling-reference-into-typst-compile.md b/docs/adr/0012-fold-dangling-reference-into-typst-compile.md new file mode 100644 index 0000000..94b5ece --- /dev/null +++ b/docs/adr/0012-fold-dangling-reference-into-typst-compile.md @@ -0,0 +1,90 @@ +# ADR 0012: Reference Resolution Folds Into `TypstCompile` (Taxonomy 7 → 6) + +## Status + +Accepted. **Corrects ADR-0010**, which fixed the diagnostic taxonomy at *seven* +classes including a separate `DanglingReference`. This ADR retires +`DanglingReference`, folding reference-resolution failures into `TypstCompile`, so +the taxonomy is now *six* classes. ADR-0010 stays the record of the original +decision; this one records the correction. + +## Context + +ADR-0010 named two distinct external-facility diagnostics for reference problems: + +- `DanglingReference` — "a relative import outside the import boundary, or an + unresolved cross-reference." +- `TypstCompile` — "the assembled typst source fails to compile (syntax error, + **unresolved `@ref`**, etc.)." + +The unresolved cross-reference (`@ref`) was listed under **both** — a genuine +contradiction in the contract. And on inspection, the *other* `DanglingReference` +case (an out-of-boundary relative import) is **also** a typst compile-time error: +typst resolves `import`/`include` paths at runtime (ADR-0011's *Correction*), so a +path escaping the import boundary fails as `"cannot access file system from +here"` — a `TypstCompile` diagnostic. Both of `DanglingReference`'s cases are +therefore detected by, and surface as, the typst compiler's own output. + +The implementation reflected this from the start: `cph-typst` maps **every** typst +`SourceDiagnostic` to `DiagCode::TypstCompile` (`crates/cph-typst/src/diag.rs`), and +**no** code path ever emits `DanglingReference`. The Lean `Oracle` likewise had a +`refsResolve` field separate from `compiles`, but `compiles t` already entails that +target `t`'s references resolve (the source would not compile otherwise) — so +`refsResolve` was redundant in the `Legal` conjunction. + +`DanglingReference` was thus a contract class with no distinct verdict, no distinct +emitter, and a definition overlapping `TypstCompile`. It diluted the taxonomy +rather than carving a real boundary. + +## Decision + +### `TypstCompile` owns reference resolution + +`TypstCompile` is the single external-facility diagnostic for the assembled typst +source failing to compile — **including** an unresolved cross-reference (`@ref`) +and a relative `import`/`include` that escapes the import boundary or names a +missing file. There is no separate reference-resolution diagnostic. + +### `DanglingReference` is retired; the taxonomy is six classes + +The diagnostic taxonomy is now: + +| Code | Meaning | Severity | Kind | +|------|---------|----------|------| +| `PartPathMissing` | A manifest `[[parts]]` entry points at a non-existent folder (or escapes the root via `..`). | error | structural | +| `UnknownKind` | A part declares a kind not in the known set (or a part/`element.toml` kind mismatch). | error | structural | +| `MissingContentFile` | A `content` field required by the kind schema has no `.typ`. | error | structural/schema | +| `SchemaViolation` | Instance data violates its kind's JSON Schema; also the malformed-`manifest`/`element.toml` fallback. | error | schema / external | +| `TypstCompile` | The assembled typst source fails to compile — syntax error, unresolved `@ref`, out-of-boundary or missing `import`/`include`. | error | external | +| `RenderIgnored` | A used kind a target does not cover; the element is omitted from that export. | **warning** | semantic | + +`RenderIgnored` alone is a `warning`; the other five are `error`. The +structural / external / semantic boundary from ADR-0010 is unchanged. + +### `Oracle.refsResolve` is removed + +The `Legal`-predicate oracle drops its `refsResolve` field. Reference resolution is +subsumed by `compiles` (per target): `compiles t` already requires `t`'s assembled +source to compile, which requires its references to resolve. `Legal` becomes +`dataConforms ∧ contentFilesPresent ∧ (∀ declared t, compiles t)`. + +## Consequences + +- The contract no longer contradicts itself on where an unresolved `@ref` is + reported: it is a `TypstCompile` diagnostic, full stop. +- The implementation needs no behavioral change — it already routed all reference + failures to `TypstCompile` and never emitted `DanglingReference`. The + correction *removes* the unused `DiagCode::DanglingReference` variant, closing + the spec↔impl gap (a named-but-unemitted code) rather than leaving it as a + permanent MVP-deferred stub. +- The `Oracle` / `Legal` definitions in the Lean master shrink by one redundant + conjunct, with no change to which lessons are legal. + +## Open Questions / Deferred + +- **Finer reference diagnostics.** Should a future checker want to distinguish an + out-of-boundary import from a missing file from an unresolved `@ref` — with + reference-specific fix hints better than typst's generic message — that is a + *new* diagnostic class, introduced deliberately when the need is real (ADR-0010's + "taxonomy is open to growth" still holds). This ADR removes the redundant class; + it does not forbid a genuinely distinct one later. diff --git a/spec/Spec/Courseware.lean b/spec/Spec/Courseware.lean index ee76da3..5a3610e 100644 --- a/spec/Spec/Courseware.lean +++ b/spec/Spec/Courseware.lean @@ -1,35 +1,21 @@ -import Spec.Courseware.Primitives -import Spec.Courseware.RichContent -import Spec.Courseware.Artifact -import Spec.Courseware.Element -import Spec.Courseware.Lesson -import Spec.Courseware.Render -import Spec.Courseware.Diagnostic -import Spec.Courseware.Pipeline -import Spec.Courseware.QuestionBank -import Spec.Courseware.Course +import Spec.Courseware.Model +import Spec.Courseware.Export +import Spec.Courseware.Check +import Spec.Courseware.Open /-! # Courseware —— 产品层契约(课程工程文件) -护城河:课程"工程文件"的语义母本与合法性规则。决策出处 ADR-0005 / 0006 / 0007 / 0008 -/ 0009 / 0010 / 0011。 +护城河:课程"工程文件"的语义母本与合法性规则。决策出处 ADR-0005..0011。按四组组织: -已填实(PINNED): -- `Primitives` —— 基元载体(表示留给实现;schema 形态见 ADR-0006)。 -- `RichContent` —— 富内容 = 带虚拟路径的 typst 源(ADR-0006 的 prose 母本)。 -- `Artifact` —— export 产物(带字段 ADT:`singleFile filepath` / `fileTree root outputs`), - target 值的一部分(ADR-0009/0011)。 -- `Element` —— kind 标签 + 依赖 schema 的数据。 -- `Lesson` —— element 的有序序列(序载教学语义、不建模时长)。 -- `Render` —— export target = artifact + 有序 typed steps:`TargetSpec` 携 `artifact` + - `steps : List Step`(`typstCompile template` / `shell run`)+ 覆盖声明 `covers`; - `RenderConfig.covers` 判定(ADR-0009/0011,修订 ADR-0005)。RenderRule 载荷已废止。 -- `Diagnostic` —— Severity + 7 类诊断的含义与级别 + **合法 lesson = 无 error 级诊断**; - 模型外设施诊断以抽象谓词 + `Oracle` 实现边界表示(ADR-0010)。 -- `Pipeline` —— 检查管线的 5 阶段、执行序、compile 门控(ADR-0010)。 - -留白骨架(核心关系 OPEN,已 surface 不臆造): -- `QuestionBank` —— 题库与 element 的关系(引用 vs 内联)。 -- `Course` —— course = lesson 编排的规则。 +- **`Model`** —— 工程文件的内容模型:基元 `Primitives`、富内容 `RichContent`、原子 + 单位 `Element`、单节课 `Lesson`(element 的有序序列)。 +- **`Export`** —— export target = artifact + 有序 typed steps:产物 ADT `Artifact` + (`singleFile` / `fileTree`),build 规格 `TargetSpec`(artifact + steps + 覆盖声明 + `covers`)与 `RenderConfig`。 +- **`Check`** —— checker 语义:`Severity` + 6 类诊断 + **合法 lesson = 无 error 级 + 诊断**(模型外设施诊断以抽象谓词 + `Oracle` 表示);检查管线的 5 阶段、序、compile + 门控。 +- **`Open`** —— 留白骨架(核心关系 OPEN,已 surface 不臆造):题库 `QuestionBank`、 + 课程编排 `Course`。 -/ diff --git a/spec/Spec/Courseware/Artifact.lean b/spec/Spec/Courseware/Artifact.lean deleted file mode 100644 index 4f6fe55..0000000 --- a/spec/Spec/Courseware/Artifact.lean +++ /dev/null @@ -1,35 +0,0 @@ -/-! -# Artifact —— export target 的产物(ADR-0009 / 0011) - -ADR-0009:一个 export target 是**一次 build**,产出一个**有类型的产物**(artifact)。 -ADR-0011 进一步钉死:产物不是一个光秃的标签,而是**带字段的 ADT**——"产物到底指什么" -(单个文件落在哪 / 一棵树产出哪些文件)是不好猜的领域语义,必须写进字段 + doc,而非 -抹成 `singleFile | fileTree` 两个空构造子。 - -路径/glob 在此用 `String` 承载并由 doc 赋义(它们就是文本:一个相对路径、一个 glob -模式),不复刻文件系统类型——契约只钉"这个字段是什么",不建模路径代数。 --/ - -namespace Spec.Courseware - -/-- -export 产物(`PINNED` 带字段 ADT, ADR-0011)。 - -- `singleFile (filepath)` —— 产物是**单个文件**,落在 `filepath`(相对工程根的路径)。 - 讲义 PDF、教案 PDF 即此。`filepath` 说清"这一份产物写到哪"。 -- `fileTree (root) (outputs)` —— 产物是 `root` 目录下、匹配 `outputs` **glob** 的**一组 - 文件**(第三方平台 archive 即此)。用 glob 而非显式清单:比逐个枚举轻,又让消费方/ - checker 知道"这次 build 该产出哪些文件"、可据以校验产物完整性。 - -**为什么字段进契约**:产物形状决定 `cph build` 吐一个文件还是一个目录、消费方期待什么; -也决定 reduce/assemble 怎么折叠(`singleFile` 把有序片段拼成一份再编译——这也是交叉引用 -`@ref` 与 例题N 计数器能工作的前提;`fileTree` 每 part 落一文件)。后端/格式(哪个 PDF -引擎、哪种 markdown 方言)仍 OPEN(ADR-0009),不在字段里。 --/ -inductive Artifact where - /-- 单文件产物,落在 `filepath`(相对工程根)。 -/ - | singleFile (filepath : String) - /-- 多文件产物:`root` 目录下匹配 `outputs` glob 的文件集。 -/ - | fileTree (root : String) (outputs : String) - -end Spec.Courseware diff --git a/spec/Spec/Courseware/Check.lean b/spec/Spec/Courseware/Check.lean new file mode 100644 index 0000000..b326f16 --- /dev/null +++ b/spec/Spec/Courseware/Check.lean @@ -0,0 +1,9 @@ +import Spec.Courseware.Check.Diagnostic +import Spec.Courseware.Check.Pipeline + +/-! +# Courseware.Check —— checker 语义 + +诊断分类与合法 lesson(`Diagnostic`)、检查管线的阶段与序(`Pipeline`)。决策出处 +ADR-0010。 +-/ diff --git a/spec/Spec/Courseware/Check/Diagnostic.lean b/spec/Spec/Courseware/Check/Diagnostic.lean new file mode 100644 index 0000000..eab8b25 --- /dev/null +++ b/spec/Spec/Courseware/Check/Diagnostic.lean @@ -0,0 +1,100 @@ +import Spec.Courseware.Model.Lesson +import Spec.Courseware.Export.Render + +/-! +# Diagnostic —— checker 诊断:分类、严重级别、合法 lesson + +产品里"站在 Lean 位置"的 rule-based checker,语义在此沉淀(ADR-0010,经 ADR-0012 +修订)。它对 lesson 提诊断,每条有**分类**(`DiagKind`)与**严重级别**(`Severity`)。 +本模块:钉级别类型(二分);钉 6 类诊断各自的含义与级别,并把"**合法 lesson = 无 +error 级诊断**"建成判定(ADR-0005 deferred 的"完整合法判定"的回填);对**模型外设施** +型诊断(typst 编过否、数据合 schema 否)用**抽象谓词 + `Oracle` 实现边界**表示——契约 +说"存在这条诊断、什么意思、什么级别",真值由实现提供,不在 Lean 内计算(不内嵌 typst +编译器)。引用解析(`@ref`、相对 import)不另设诊断:它们都是 typst 编译期失败,归 +`typstCompile`(ADR-0012)。 +-/ + +namespace Spec.Courseware + +/-- 诊断严重级别(`PINNED` 二分, ADR-0005)。`error` 阻断(产物不合法),`warning` 不 +阻断(产物仍可导出,只是有损)。更细级别(info/hint)未决策,故只二分。 -/ +inductive Severity where + | warning + | error + +/-- 诊断**分类**(`PINNED` 6 类, ADR-0010,经 ADR-0012 修订为 6 类)。按"谁来判定"分 +三层:**结构型**(模型自身可判):`partPathMissing`/`unknownKind`;**schema/外部设施型** +(靠实现 oracle):`missingContentFile`/`schemaViolation`/`typstCompile`;**语义型**: +`renderIgnored`。 -/ +inductive DiagKind where + /-- manifest 的 part 指向不存在的文件夹(或经 `..` 逃出根)。结构型。 -/ + | partPathMissing + /-- part 声明了未知 kind(含 part 与 element.toml 的 kind 不一致)。结构型。 -/ + | unknownKind + /-- kind schema 要求的某 `content` 字段缺对应 `.typ`。结构/schema 型。 -/ + | missingContentFile + /-- 实例数据不合其 kind 的 JSON Schema;亦作 manifest/element.toml 畸形的兜底。 -/ + | schemaViolation + /-- 拼装出的 typst 源编译失败:语法错、未解析的交叉引用 `@ref`、越界或缺失的相对 + `import`/`include`(后两者即旧 `danglingReference` 的两种情形——typst 在编译期 + 检出,故归此类,ADR-0012)。外部设施型。 -/ + | typstCompile + /-- 某被用到的 kind 在某声明的 target 下无渲染规则,该 element 被忽略。语义型。 -/ + | renderIgnored + +/-- 每类诊断的**严重级别**(`PINNED`, ADR-0010)。五类 `error`(阻断);**唯 +`renderIgnored` 为 `warning`**——ADR-0005 种子规则"缺渲染 ⇒ warning,不阻断导出"。 +钉成全函数使"哪类阻断"成为可引用、可对齐的事实(实现侧 `DiagCode` 级别据此对齐)。 -/ +def DiagKind.severity : DiagKind → Severity + | .partPathMissing => .error + | .unknownKind => .error + | .missingContentFile => .error + | .schemaViolation => .error + | .typstCompile => .error + | .renderIgnored => .warning + +/-- 缺渲染诊断的级别 = **warning**(`PINNED`, ADR-0005/0010,**非 error**)。具名常量, +使"它是 warning"可被实现侧 grep 对齐(实现里同名常量 `RENDER_IGNORED_SEVERITY` 引用 +本定义)。等价于 `DiagKind.renderIgnored.severity`。 -/ +def renderIgnoredSeverity : Severity := DiagKind.renderIgnored.severity + +variable (P : Primitives) + +/-- **缺渲染诊断**:lesson 在 target `t` 下存在无法渲染的 element(`PINNED`, +ADR-0005/0009)。成立 ⟺ 存在某 element,其 kind 在 `t` 下 `covers` 为假。语义型诊断, +级别 warning。 -/ +def renderIgnored (l : Lesson P) (c : RenderConfig P) (t : P.TargetId) : Prop := + ∃ e ∈ l, ¬ c.covers e.kind t + +/-! +## 模型外设施型诊断:抽象谓词 + 实现边界(ADR-0010) + +`typstCompile`/`schemaViolation`(的 schema-合规面)断言的是模型自身无法判定的事实—— +要跑 typst 编译器、schema 校验器。契约把它们建成**抽象谓词**,真值由实现提供的 oracle +给出。下面用 `Oracle` 收口这些判定:它不是要在 Lean 里实现 checker,而是把"这些事实 +来自模型外"显式化、类型化。 +-/ + +/-- **实现侧判定 oracle**(`PINNED` 实现边界, ADR-0010)。每个字段是一个谓词,真值由 +实现(checker)提供。结构型诊断(part 路径、未知 kind)不入此 oracle——那些模型自身可判。 -/ +structure Oracle (l : Lesson P) (c : RenderConfig P) where + /-- target `t` 下拼装源可编译(否 ⇒ `typstCompile`)。**含引用解析**:源能编译即蕴含 + 其 `@ref`、相对 import 全部解析(ADR-0012 已把引用诊断并入 `typstCompile`)。 -/ + compiles : P.TargetId → Prop + /-- 每个 element 数据合 schema(否 ⇒ `schemaViolation`)。 -/ + dataConforms : Prop + /-- schema 要求的 content 文件齐备(否 ⇒ `missingContentFile`)。 -/ + contentFilesPresent : Prop + +/-- **合法 lesson**(`PINNED`, ADR-0010;回填 ADR-0005 deferred 的"完整合法判定")。 + +合法 ⟺ 检查管线产出**零条 error 级诊断**。展开为:模型外设施判定(经 `Oracle`)全为真, +**且**每个声明的 target 都编译通过。结构型诊断由 `cph-model` 在加载期判定;能走到这步 +谈合法性意味着已加载成功,故此处聚焦 schema/外部设施层。引用解析不单列——已被 +`compiles` 蕴含(ADR-0012)。`renderIgnored` 是 warning,**不**进合取——ADR-0005 种子 +规则的体现。`targets` 用全称式表达以不绑定 `TargetId` 的可枚举性。 -/ +def Legal (l : Lesson P) (c : RenderConfig P) (o : Oracle P l c) : Prop := + o.dataConforms ∧ o.contentFilesPresent ∧ + (∀ t : P.TargetId, (c.spec t).isSome → o.compiles t) + +end Spec.Courseware diff --git a/spec/Spec/Courseware/Check/Pipeline.lean b/spec/Spec/Courseware/Check/Pipeline.lean new file mode 100644 index 0000000..00efa01 --- /dev/null +++ b/spec/Spec/Courseware/Check/Pipeline.lean @@ -0,0 +1,52 @@ +import Spec.Courseware.Check.Diagnostic + +/-! +# Pipeline —— checker 检查管线的阶段与序(ADR-0010) + +checker 的 `check` 按**固定顺序**跑五个阶段,逐阶段收集诊断;`compile` 阶段有**门控**。 +顺序与门控是契约——它决定用户看到哪些诊断(藏在缺文件背后的语法错,在文件补齐前不 +显示,这是有意的)。每阶段的**算法**不进 Lean(宪法第 5 条深度上限):只钉**阶段、序、 +门控**。阶段对应上游模块:`load`←`cph-model`;`structural`←part 路径/未知 kind; +`schema`←`cph-schema`;`compile`←`cph-typst`(模型外设施);`coverage`←`renderIgnored`。 +-/ + +namespace Spec.Courseware + +/-- 检查管线的**阶段**(`PINNED` 5 阶段, ADR-0010)。 + +- `load` —— 解析 manifest + 各 element.toml。硬失败则**停**整条管线。 +- `structural` —— part 路径存在、无 `..`、kind 已知且一致。此处判缺的 part 后续跳过。 +- `schema` —— 每个"存在且 kind 已知"的 part 按其 kind schema 校验。 +- `compile` —— 模型外设施阶段(typst 编译)。**门控:仅当前序零 error 才跑**。 +- `coverage` —— 语义型 warning(`renderIgnored`);**不**受门控,总跑。 -/ +inductive Phase where + | load + | structural + | schema + | compile + | coverage +deriving DecidableEq + +/-- 管线阶段的**执行序**(`PINNED`, ADR-0010)。`order p` 越小越先跑。序是契约: +`compile`(3)排在 `structural`(1)/`schema`(2)之后,正因前者门控于后者无 error。 -/ +def Phase.order : Phase → Nat + | .load => 0 + | .structural => 1 + | .schema => 2 + | .compile => 3 + | .coverage => 4 + +/-- 某阶段是否**受"前序零 error"门控**(`PINNED`, ADR-0010)。唯 `compile` 受门控:藏在 +结构/schema 错背后的编译错,在前者修好前不显示——有意降噪。 -/ +def Phase.gated : Phase → Bool + | .compile => true + | _ => false + +/-- 管线在 `load` 硬失败时**停**(`PINNED`, ADR-0010)。`load` 拿不到可解析 lesson 时, +无 lesson 可喂下游,整条管线终止——唯一会截断后续所有阶段的情形(区别于 `compile` +门控只跳过自己)。 -/ +def Phase.haltsPipelineOnFailure : Phase → Bool + | .load => true + | _ => false + +end Spec.Courseware diff --git a/spec/Spec/Courseware/Course.lean b/spec/Spec/Courseware/Course.lean deleted file mode 100644 index 30a165c..0000000 --- a/spec/Spec/Courseware/Course.lean +++ /dev/null @@ -1,16 +0,0 @@ -import Spec.Courseware.Lesson - -/-! -# Course —— 课程编排(骨架,规则 OPEN) - -ADR-0005:工程文件的粒度是**单节课**;course / 单元**不是**工程文件,而是 lesson -的**编排**。 - -但"编排"的具体规则未决策:course 是 lesson 的有序列表,还是带层级(单元 → 课)的 -树?编排里 lesson 是被引用还是被包含?跨 lesson 有无约束(目标覆盖、前后置)?这些 -都是 `OPEN`。 - -按宪法第 2 条,本模块**不臆造**编排结构——不建 `Course := List Lesson`(那会偷偷 -承诺"扁平有序、无层级")。只在此 surface:课程编排待专门 ADR。本文件当前不引入任何 -承诺性声明。 --/ diff --git a/spec/Spec/Courseware/Diagnostic.lean b/spec/Spec/Courseware/Diagnostic.lean deleted file mode 100644 index f57bdc6..0000000 --- a/spec/Spec/Courseware/Diagnostic.lean +++ /dev/null @@ -1,144 +0,0 @@ -import Spec.Courseware.Lesson -import Spec.Courseware.Render - -/-! -# Diagnostic —— checker 诊断:分类、严重级别、合法 lesson - -产品里"站在 Lean 位置"的那个 rule-based checker,语义在此沉淀(ADR-0010)。它对 lesson -提诊断,每条诊断有**分类**(`DiagKind`)与**严重级别**(`Severity`)。本模块: - -1. 钉级别类型(二分,ADR-0005)。 -2. 钉 7 类诊断各自的含义与级别(ADR-0010),并把"**合法 lesson = 无 error 级诊断**" - 建成判定——这是 ADR-0005 deferred 的"完整合法判定"的回填。 -3. 对**模型外设施**型诊断(typst 能否编过、引用悬否、数据合 schema 否),用**抽象谓词 + - 显式实现边界**表示:契约说"存在这样一条诊断、它什么意思、什么级别",但其**真值由 - 实现(checker)提供**,不在 Lean 内计算——保持契约诚实(不内嵌 typst 编译器)。 --/ - -namespace Spec.Courseware - -/-- -诊断的严重级别(`PINNED` 二分, ADR-0005)。 - -`error` 阻断(产物不合法),`warning` 不阻断(产物仍可导出,只是有损/有忽略)。更细的 -级别(info/hint)未决策,故只二分。 --/ -inductive Severity where - | warning - | error - -/-- -诊断的**分类**(`PINNED` 7 类, ADR-0010)。每类含义见下;级别见 `DiagKind.severity`。 - -按"谁来判定"分三层(ADR-0010 的边界): -- **结构型**(模型自身可判):`partPathMissing` / `unknownKind`。 -- **schema / 外部设施型**(判定靠实现 oracle):`missingContentFile` / `schemaViolation` - / `danglingReference` / `typstCompile`。 -- **语义型**(coverage 规则):`renderIgnored`。 --/ -inductive DiagKind where - /-- manifest 的 part 指向不存在的文件夹(或经 `..` 逃出根)。结构型。 -/ - | partPathMissing - /-- part 声明了未知 kind(含 part 与 element.toml 的 kind 不一致)。结构型。 -/ - | unknownKind - /-- kind schema 要求的某 `content` 字段缺对应 `.typ`。结构/schema 型。 -/ - | missingContentFile - /-- 实例数据不合其 kind 的 JSON Schema(标量类型错/缺必填/多余键);亦作 manifest/ - element.toml 畸形的兜底。schema / 外部设施型。 -/ - | schemaViolation - /-- 引用不解析:越界的相对 import,或悬空的交叉引用。外部设施型。 -/ - | danglingReference - /-- 拼装出的 typst 源编译失败(语法错、`@ref` 未解析…)。外部设施型。 -/ - | typstCompile - /-- 某被用到的 kind 在某声明的 target 下无渲染规则,该 element 被该 target 忽略。语义型。 -/ - | renderIgnored - -/-- -每类诊断的**严重级别**(`PINNED`, ADR-0010)。 - -六类为 `error`(阻断);**唯 `renderIgnored` 为 `warning`**——即 ADR-0005 的种子规则 -"缺渲染 ⇒ warning,不阻断导出"。把级别钉成一个全函数,使"哪类阻断、哪类不阻断"成为 -契约里可引用、可对齐的事实(实现侧 `DiagCode` 的级别据此对齐)。 --/ -def DiagKind.severity : DiagKind → Severity - | .partPathMissing => .error - | .unknownKind => .error - | .missingContentFile => .error - | .schemaViolation => .error - | .danglingReference => .error - | .typstCompile => .error - | .renderIgnored => .warning - -/-- 缺渲染诊断的级别 = **warning**(`PINNED`, ADR-0005/0010,**非 error**)。 - -保留为具名常量,使"它是 warning 不是 error"可被实现侧 grep 对齐(实现里同名常量 -`RENDER_IGNORED_SEVERITY` 引用本定义)。等价于 `DiagKind.severity .renderIgnored`。 -/ -def renderIgnoredSeverity : Severity := DiagKind.renderIgnored.severity - -variable (P : Primitives) - -/-- -**缺渲染诊断**:lesson 在 target `t` 下存在无法渲染的 element(`PINNED`, ADR-0005/0009)。 - -成立 ⟺ 存在某 element,其 kind 在 `t` 下未配渲染规则(`covers` 为假,见 `Render`)。这条 -是 checker 的**语义型**诊断,级别由 `renderIgnoredSeverity` 钉为 warning。`covers` 已随 -ADR-0009 下沉到 target 的 build 规格,但本判定式不变。 --/ -def renderIgnored (l : Lesson P) (c : RenderConfig P) (t : P.TargetId) : Prop := - ∃ e ∈ l, ¬ c.covers e.kind t - -/-! -## 模型外设施型诊断:抽象谓词 + 实现边界(ADR-0010) - -`typstCompile` / `danglingReference` / `schemaViolation`(的 schema-合规面)断言的是 -**模型自身无法判定**的事实——要跑 typst 编译器、要跑 schema 校验器。契约因此把它们建成 -**抽象谓词**,真值由一个**实现提供的 oracle** 给出。Lean 只说"这条诊断存在、什么意思、 -什么级别",**不**在 Lean 内计算其真假。 - -下面用一个 `Oracle` 结构收口这些实现侧判定。它**不是**要在 Lean 里实现 checker,而是 -把"这些事实来自模型外"这件事显式化、类型化:谁想谈论一节 lesson 合不合法,就得先有一个 -oracle 提供这些外部判定。 --/ - -/-- -**实现侧判定 oracle**(`PINNED` 实现边界, ADR-0010)。 - -收口那些"模型外设施"才能回答的判定。每个字段是一个谓词,**真值由实现(checker)提供**: - -- `compiles` —— 该 lesson 在 target `t` 下拼装出的 typst 源能否编译通过(否 ⇒ `typstCompile`)。 -- `refsResolve` —— 该 lesson 的引用(相对 import / 交叉引用)是否全部解析(否 ⇒ `danglingReference`)。 -- `dataConforms` —— 每个 element 的数据是否合其 kind schema(否 ⇒ `schemaViolation`)。 -- `contentFilesPresent` —— schema 要求的 `content` 文件是否齐备(否 ⇒ `missingContentFile`)。 - -把它们作为参数,正是"显式实现边界":契约能据此**定义**合法性,却不假装自己能算出这些 -外部事实。结构型诊断(part 路径、未知 kind)不入此 oracle——那些模型自身可判。 --/ -structure Oracle (l : Lesson P) (c : RenderConfig P) where - /-- target `t` 下拼装源可编译。 -/ - compiles : P.TargetId → Prop - /-- 引用全部解析。 -/ - refsResolve : Prop - /-- 每个 element 数据合 schema。 -/ - dataConforms : Prop - /-- schema 要求的 content 文件齐备。 -/ - contentFilesPresent : Prop - -/-- -**合法 lesson**(`PINNED`, ADR-0010;回填 ADR-0005 deferred 的"完整合法判定")。 - -一节 lesson 合法 ⟺ 检查管线产出**零条 error 级诊断**。warning(如 `renderIgnored`) -不影响合法性——带 warning 的 lesson 仍合法、仍可(有损)导出。 - -这里把"无 error 级诊断"展开为:模型外设施判定(经 `Oracle`)全部为真,**且**每个声明的 -target 都编译通过。结构型诊断(part 路径、未知 kind、kind 不一致)由 `cph-model` 在加载 -期判定;能走到这一步谈合法性,意味着已加载成功,故此处聚焦 schema/外部设施层。注意 -`renderIgnored` 是 warning,**不**进合法性合取——这正是 ADR-0005 种子规则的体现。 - -`targets` 是该工程文件声明的 target 列表(`RenderConfig.spec t` 非 `none` 者);为保持 -本层抽象、不绑定 `TargetId` 的可枚举性,这里用"对所有满足前提的 t"的全称式表达。 --/ -def Legal (l : Lesson P) (c : RenderConfig P) (o : Oracle P l c) : Prop := - o.refsResolve ∧ o.dataConforms ∧ o.contentFilesPresent ∧ - (∀ t : P.TargetId, (c.spec t).isSome → o.compiles t) - -end Spec.Courseware diff --git a/spec/Spec/Courseware/Element.lean b/spec/Spec/Courseware/Element.lean deleted file mode 100644 index d1bb7f9..0000000 --- a/spec/Spec/Courseware/Element.lean +++ /dev/null @@ -1,32 +0,0 @@ -import Spec.Courseware.Primitives - -/-! -# Element —— 课程内容的原子单位 - -ADR-0005:element 实例 = 一个 kind 标签 + 符合该 kind schema 的数据。本模块把这条 -编码成一个依赖结构,使"数据必须匹配其 kind"成为类型层面的事实而非运行时校验。 --/ - -namespace Spec.Courseware - -variable (P : Primitives) - -/-- -element 实例(`PINNED`, ADR-0005)。 - -`data` 的类型 `P.ElementData kind` **由 `kind` 决定**——这意味着无法构造一个数据与 -其 kind 不符的 element:schema 合规由类型系统而非 checker 保证。 - -ADR-0005 的 (a) 类信息(逐字稿、重点圈划等"语义性但只在某些 target 浮现"的字段) -属于具体 kind 的 schema,落在 `P.ElementData` 内,不出现在这个通用结构上;(b) 类 -信息(html 交互、build/npm)按 ADR-0005 不进 element。交互教具是一种"重型 kind", -其 `ElementData` 只承载题目/配置数据,重实现在模型之外——它在此结构里与例题、定理 -同构,仅 `kind` 不同。 --/ -structure Element where - /-- 该 element 的 kind。 -/ - kind : P.KindId - /-- 符合 `kind` schema 的数据(类型随 `kind` 而变)。 -/ - data : P.ElementData kind - -end Spec.Courseware diff --git a/spec/Spec/Courseware/Export.lean b/spec/Spec/Courseware/Export.lean new file mode 100644 index 0000000..7788bd6 --- /dev/null +++ b/spec/Spec/Courseware/Export.lean @@ -0,0 +1,8 @@ +import Spec.Courseware.Export.Artifact +import Spec.Courseware.Export.Render + +/-! +# Courseware.Export —— export target = artifact + 有序 typed steps + +产物 ADT(`Artifact`)、build 规格与渲染覆盖(`Render`)。决策出处 ADR-0009 / 0011。 +-/ diff --git a/spec/Spec/Courseware/Export/Artifact.lean b/spec/Spec/Courseware/Export/Artifact.lean new file mode 100644 index 0000000..4e202a6 --- /dev/null +++ b/spec/Spec/Courseware/Export/Artifact.lean @@ -0,0 +1,23 @@ +/-! +# Artifact —— export target 的产物(ADR-0009 / 0011) + +ADR-0009:一个 export target 是**一次 build**,产出一个**有类型的产物**。ADR-0011 +钉死:产物是**带字段的 ADT**——"产物到底指什么"(单文件落在哪 / 一棵树产出哪些文件) +是不好猜的领域语义,必须写进字段 + doc,而非抹成两个空构造子。路径/glob 用 `String` +承载并由 doc 赋义(它们就是文本),不复刻文件系统类型。 +-/ + +namespace Spec.Courseware + +/-- export 产物(`PINNED` 带字段 ADT, ADR-0011)。产物形状决定 `cph build` 吐文件还是 +目录、reduce 怎么折叠(`singleFile` 把有序片段拼成一份再编译——交叉引用 `@ref`、例题 +计数器能工作的前提;`fileTree` 每 part 落一文件)。后端/格式仍 OPEN(ADR-0009)。 -/ +inductive Artifact where + /-- 单文件产物,落在 `filepath`(相对工程根)。讲义/教案 PDF 即此。 -/ + | singleFile (filepath : String) + /-- 多文件产物:`root` 目录下匹配 `outputs` **glob** 的文件集(第三方平台 archive + 即此)。用 glob 而非显式清单:轻,又让消费方/checker 知道该产出哪些文件、可校验 + 完整性。 -/ + | fileTree (root : String) (outputs : String) + +end Spec.Courseware diff --git a/spec/Spec/Courseware/Export/Render.lean b/spec/Spec/Courseware/Export/Render.lean new file mode 100644 index 0000000..183da8b --- /dev/null +++ b/spec/Spec/Courseware/Export/Render.lean @@ -0,0 +1,59 @@ +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),供种子诊断用。 +-/ + +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) 类落这)。MVP 不实现,先建结构。 -/ + | 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 diff --git a/spec/Spec/Courseware/Lesson.lean b/spec/Spec/Courseware/Lesson.lean deleted file mode 100644 index 01564c9..0000000 --- a/spec/Spec/Courseware/Lesson.lean +++ /dev/null @@ -1,21 +0,0 @@ -import Spec.Courseware.Element - -/-! -# Lesson —— 单节课工程文件 - -ADR-0005:一个工程文件 = 一节课,是 element 实例的**有序序列**。课程/单元不是工程 -文件,而是 lesson 的编排(见 `Spec.Courseware.Course`,OPEN)。 --/ - -namespace Spec.Courseware - -/-- -一节课(`PINNED`, ADR-0005)。 - -用 `List` 而非 `Multiset`/`Finset`,因为 **element 的先后次序承载教学语义**(讲义/ -PPT 式的内容流,先讲定义再举例不同于反过来)。**不建模时长**:ADR-0005 决定 lesson -是内容编排而非时间轴,故这里没有"每块多少分钟"这类字段——序是结构,时长不是。 --/ -abbrev Lesson (P : Primitives) := List (Element P) - -end Spec.Courseware diff --git a/spec/Spec/Courseware/Model.lean b/spec/Spec/Courseware/Model.lean new file mode 100644 index 0000000..2b64818 --- /dev/null +++ b/spec/Spec/Courseware/Model.lean @@ -0,0 +1,11 @@ +import Spec.Courseware.Model.Primitives +import Spec.Courseware.Model.RichContent +import Spec.Courseware.Model.Element +import Spec.Courseware.Model.Lesson + +/-! +# Courseware.Model —— 工程文件的内容模型 + +留白基元(`Primitives`)、富内容锚点(`RichContent`)、原子单位(`Element`)、单节课 +(`Lesson`)。决策出处 ADR-0005 / 0006。 +-/ diff --git a/spec/Spec/Courseware/Model/Element.lean b/spec/Spec/Courseware/Model/Element.lean new file mode 100644 index 0000000..19bc8ac --- /dev/null +++ b/spec/Spec/Courseware/Model/Element.lean @@ -0,0 +1,24 @@ +import Spec.Courseware.Model.Primitives + +/-! +# Element —— 课程内容的原子单位 + +ADR-0005:element 实例 = 一个 kind 标签 + 符合该 kind schema 的数据。本模块把它编码成 +依赖结构,使"数据必须匹配其 kind"成为类型层面的事实而非运行时校验。 +-/ + +namespace Spec.Courseware + +variable (P : Primitives) + +/-- element 实例(`PINNED`, ADR-0005)。`data : P.ElementData kind` 由 `kind` 决定—— +无法构造数据与 kind 不符的 element,schema 合规由类型系统保证。ADR-0005 的 (a) 类 +字段(逐字稿、重点圈划)落在具体 kind 的 `ElementData` 内,不出现在此通用结构上; +交互教具等"重型 kind"在此与例题、定理同构,仅 `kind` 不同,重实现在模型之外。 -/ +structure Element where + /-- 该 element 的 kind。 -/ + kind : P.KindId + /-- 符合 `kind` schema 的数据(类型随 `kind` 而变)。 -/ + data : P.ElementData kind + +end Spec.Courseware diff --git a/spec/Spec/Courseware/Model/Lesson.lean b/spec/Spec/Courseware/Model/Lesson.lean new file mode 100644 index 0000000..3a3145d --- /dev/null +++ b/spec/Spec/Courseware/Model/Lesson.lean @@ -0,0 +1,16 @@ +import Spec.Courseware.Model.Element + +/-! +# Lesson —— 单节课工程文件 + +ADR-0005:一个工程文件 = 一节课,是 element 实例的**有序序列**。课程/单元不是工程 +文件,而是 lesson 的编排(见 `Spec.Courseware.Course`,OPEN)。 +-/ + +namespace Spec.Courseware + +/-- 一节课(`PINNED`, ADR-0005)。用 `List` 因为 **element 次序承载教学语义**(先讲 +定义再举例 ≠ 反过来);**不建模时长**——ADR-0005 决定 lesson 是内容编排而非时间轴。 -/ +abbrev Lesson (P : Primitives) := List (Element P) + +end Spec.Courseware diff --git a/spec/Spec/Courseware/Model/Primitives.lean b/spec/Spec/Courseware/Model/Primitives.lean new file mode 100644 index 0000000..656ae8b --- /dev/null +++ b/spec/Spec/Courseware/Model/Primitives.lean @@ -0,0 +1,34 @@ +/-! +# Primitives —— Courseware 契约的留白基元 + +课程工程文件模型(ADR-0005)依赖一组基元:element kind 怎么标识、某 kind 的数据 +schema 是什么、export target 怎么标识。收口成载体 `Primitives`,让模型在其上参数化 +——契约谈得了 element / lesson / 渲染**之间的关系**,而把每个基元的**内部表示**留给 +实现。注意:某基元语义已 PINNED(如 schema 形态由 ADR-0006 钉死)与其表示进 Lean +是两回事——JSON Schema / typst 的内部结构属实现细节,不入 Lean,故基元在此仍以抽象 +类型承载。富内容的 prose 母本见 `Courseware.RichContent`。 +-/ + +namespace Spec.Courseware + +/-- Courseware 契约基元载体(关系 `PINNED`, ADR-0005;各基元表示留给实现, ADR-0006)。 -/ +structure Primitives where + /-- element kind 标识(`PINNED` **开放宇宙**, ADR-0005;表示 `OPEN`)。刻意用抽象 + 类型而非 `inductive`:ADR-0005 决定 kind 是开放可扩展宇宙(stdlib + 第三方), + 封闭枚举会违背它——此处开放是**已决策的**(区别于 `RunState` 的"尚未封闭")。 -/ + KindId : Type + /-- 某 kind 的合法数据类型(`PINNED` 依赖关系, ADR-0005;schema 形态 `PINNED` + ADR-0006,表示仍抽象)。以 kind 为索引:`ElementData k` 即"符合 `k` schema 的 + 数据"。schema 形态(声明式 JSON Schema + `content` 叶子 = typst 源)是 ADR-0006 + 钉死的,但属 JSON/typst 内部结构、实现细节,不进 Lean;契约只锚定"数据符合 + kind schema"这条关系,故此处仍是抽象类型。 -/ + ElementData : KindId → Type + /-- export target 标识(`PINNED` 角色, ADR-0005;表示 `OPEN`)。一个 target 是一次 + build,产出对 lesson 的一种投影(讲义/教案/PPT/平台 archive…),见 `Render`。 -/ + TargetId : Type + +-- 注:原 `RenderRule : Type` 已随 ADR-0011 移除。渲染的"how"不再是契约层 per-target +-- 载荷,而由 `Render.TargetSpec.steps` 里 `typstCompile` step 引用的**模板文件**承载; +-- 契约只保留覆盖声明 `TargetSpec.covers`(该 target 渲染哪些 kind),供种子诊断用。 + +end Spec.Courseware diff --git a/spec/Spec/Courseware/Model/RichContent.lean b/spec/Spec/Courseware/Model/RichContent.lean new file mode 100644 index 0000000..05589bd --- /dev/null +++ b/spec/Spec/Courseware/Model/RichContent.lean @@ -0,0 +1,28 @@ +/-! +# RichContent —— 富内容(ADR-0006 的 prose 母本) + +ADR-0006:element schema 的"叶子"可以是 `content` 类型,其值是**一段 typst 源**, +语义取该源作为 module 求值后的 body content。关键约束(均 ADR-0006,源自 typst 源码 +事实):富内容**不可无主**——typst 的源必须有 `FileId`,否则 span 脱锚、相对 import +报"cannot access file system from here"。故每段富内容是 World 里的一等文件,坐落在 +一个**虚拟路径**上;相对 import 限本工程路径结构内 + `@package`(不跨工程)。 + +本模块只立 prose 锚点 + 最小抽象签名:typst 的 `Content`/`Module` 内部结构、JSON +Schema 形状属实现细节,不进 Lean,只承诺"富内容由一个虚拟路径定位"这一条关系。 +-/ + +namespace Spec.Courseware + +/-- 富内容在工程文件路径结构中的**虚拟路径**(`OPEN` 表示, ADR-0006)。把一段富内容 +定位为 World 里的一等文件(span 可解析、相对 import 可锚定)。落盘后即真实相对路径 +(ADR-0007),不在本层承诺,故 opaque。 -/ +opaque VPath : Type + +/-- 对一段富内容的**引用**:它坐落在某个虚拟路径上(`PINNED` 关系, ADR-0006)。 +刻意**不**建模源文本、不建模求值出的 `Content`(那是实现侧的事);只钉"富内容经由一个 +`VPath` 定位",作为 `Primitives.ElementData` 里 `content` 叶子的语义锚点。 -/ +structure RichContentRef where + /-- 该富内容所在的虚拟路径(ADR-0006;落盘后为真实相对路径, ADR-0007)。 -/ + vpath : VPath + +end Spec.Courseware diff --git a/spec/Spec/Courseware/Open.lean b/spec/Spec/Courseware/Open.lean new file mode 100644 index 0000000..d5f8fcb --- /dev/null +++ b/spec/Spec/Courseware/Open.lean @@ -0,0 +1,9 @@ +import Spec.Courseware.Open.QuestionBank +import Spec.Courseware.Open.Course + +/-! +# Courseware.Open —— 留白骨架(核心关系 OPEN) + +题库与 element 的关系(`QuestionBank`)、课程编排规则(`Course`)。两者均为已 surface +但未决策的分歧点,按宪法第 2 条不臆造,待专门 ADR 落定。 +-/ diff --git a/spec/Spec/Courseware/Open/Course.lean b/spec/Spec/Courseware/Open/Course.lean new file mode 100644 index 0000000..50617a4 --- /dev/null +++ b/spec/Spec/Courseware/Open/Course.lean @@ -0,0 +1,10 @@ +/-! +# Course —— 课程编排(骨架,规则 OPEN) + +ADR-0005:工程文件的粒度是**单节课**;course / 单元**不是**工程文件,而是 lesson 的 +**编排**。但"编排"的具体规则未决策:有序列表还是带层级(单元 → 课)的树?lesson 被 +引用还是被包含?跨 lesson 有无约束(目标覆盖、前后置)?这些都是 `OPEN`。 + +按宪法第 2 条本模块**不臆造**编排结构——不建 `Course := List Lesson`(那会偷偷承诺 +"扁平有序、无层级")。只在此 surface:课程编排待专门 ADR。本文件当前不引入任何承诺性声明。 +-/ diff --git a/spec/Spec/Courseware/Open/QuestionBank.lean b/spec/Spec/Courseware/Open/QuestionBank.lean new file mode 100644 index 0000000..7270d8d --- /dev/null +++ b/spec/Spec/Courseware/Open/QuestionBank.lean @@ -0,0 +1,10 @@ +/-! +# QuestionBank —— 题库(骨架,核心关系 OPEN) + +题库是与工程文件并列的资产(类比 DAW 的 sample library):有自身结构的实体,又是最 +典型的可复用单元,lesson 会引用它。但**题库与 element 的关系尚未决策**,且用户明确 +指出"纯引用可能不够"——element 内联题目数据 / lesson 持指向题库条目的引用 / 两者并存? + +这是一个 `OPEN` 分歧点。按宪法第 2 条本模块**不替它选解**——不建 `QuestionRef` 也不建 +内联结构,只在此 surface。待专门 ADR 落定后再填。本文件当前不引入任何承诺性声明。 +-/ diff --git a/spec/Spec/Courseware/Pipeline.lean b/spec/Spec/Courseware/Pipeline.lean deleted file mode 100644 index 16bf937..0000000 --- a/spec/Spec/Courseware/Pipeline.lean +++ /dev/null @@ -1,72 +0,0 @@ -import Spec.Courseware.Diagnostic - -/-! -# Pipeline —— checker 检查管线的阶段与序(ADR-0010) - -checker 的 `check` 按**固定顺序**跑五个阶段,逐阶段收集诊断;`compile` 阶段有**门控**。 -顺序与门控是契约——它决定用户看到哪些诊断(藏在缺文件背后的语法错,在文件补齐前不显示, -这是**有意**的)。每阶段的**算法**不进 Lean(宪法第 5 条深度上限):本模块只钉**阶段、序、 -门控**,不形式化每步怎么算。 - -阶段与上游模块的对应:`load` ← `cph-model`;`structural` ← part 路径/未知 kind;`schema` -← `cph-schema`;`compile` ← `cph-typst`(模型外设施,见 `Diagnostic.Oracle`);`coverage` -← `Diagnostic.renderIgnored`。 --/ - -namespace Spec.Courseware - -/-- -检查管线的**阶段**(`PINNED` 5 阶段, ADR-0010)。 - -- `load` —— 解析 manifest + 各 element.toml。硬失败(无可解析 lesson)则**停**整条管线。 -- `structural` —— part 路径存在、无 `..`、kind 已知、part 与 element kind 一致。此处已被 - 判缺的 part,在后续阶段**跳过**(不在同一根因上堆诊断)。 -- `schema` —— 每个"存在且 kind 已知"的 part 的数据按其 kind schema 校验(标量 + content 文件)。 -- `compile` —— 模型外设施阶段(typst 编译)。**门控:仅当 `load`/`structural`/`schema` 零 - error 才跑**(否则在已知坏输入上编译只是噪声)。跑时对每个声明的 target 编译(ADR-0009)。 -- `coverage` —— 语义型 warning 规则(`renderIgnored`);**不**受门控,总跑。 --/ -inductive Phase where - | load - | structural - | schema - | compile - | coverage -deriving DecidableEq - -/-- -管线阶段的**执行序**(`PINNED`, ADR-0010)。`order p` 越小越先跑。 - -序是契约:`compile`(3)排在 `structural`(1)/`schema`(2)之后,正因前者门控于后者无 error。 -`coverage`(4)排最后但不门控(见 `gated`)。 --/ -def Phase.order : Phase → Nat - | .load => 0 - | .structural => 1 - | .schema => 2 - | .compile => 3 - | .coverage => 4 - -/-- -某阶段是否**受"前序零 error"门控**(`PINNED`, ADR-0010)。 - -唯 `compile` 受门控:前序(load/structural/schema)出任何 error 则跳过它——藏在结构/schema -错背后的编译错,在前者修好前不显示,这是有意的降噪。其余阶段不门控:`load` 是入口, -`structural`/`schema` 是门控的**依据**(自身得先跑),`coverage` 产 warning 故无条件跑。 --/ -def Phase.gated : Phase → Bool - | .compile => true - | _ => false - -/-- -管线在 `load` 硬失败时**停**(`PINNED`, ADR-0010)。 - -`load` 拿不到可解析的 lesson(`cph-model` 返回 `none`)时,没有 lesson 可喂给下游, -整条管线就此终止——这是唯一会"截断"后续所有阶段的情形(区别于 `compile` 的门控只跳过 -自己)。 --/ -def Phase.haltsPipelineOnFailure : Phase → Bool - | .load => true - | _ => false - -end Spec.Courseware diff --git a/spec/Spec/Courseware/Primitives.lean b/spec/Spec/Courseware/Primitives.lean deleted file mode 100644 index 0c03121..0000000 --- a/spec/Spec/Courseware/Primitives.lean +++ /dev/null @@ -1,50 +0,0 @@ -/-! -# Primitives —— Courseware 契约的留白基元 - -课程工程文件模型(ADR-0005)依赖一组基元:element kind 怎么标识、某 kind 的数据 -schema 是什么、export target 怎么标识、渲染规则的载荷长什么样。 - -把它们收口成一个载体 `Primitives`,让 lesson 模型在其上参数化——契约因此能谈 -element / lesson / 渲染**之间的关系**,而把每个基元的**内部表示**留给实现。注意: -"某基元的语义已 PINNED"与"其表示进 Lean"是两回事——schema 的**形态**已由 ADR-0006 -钉死(声明式 JSON Schema + 富内容叶子 = typst content),但那是 JSON / typst 的内部 -结构、属实现细节,**不入 Lean**;Lean 只锚定"数据符合 kind schema"这条关系,故这些 -基元在此仍以抽象类型承载。富内容这一新概念的 prose 母本见 `Courseware.RichContent`。 --/ - -namespace Spec.Courseware - -/-- -Courseware 契约基元载体(关系 `PINNED`, ADR-0005;各基元表示留给实现, ADR-0006)。 --/ -structure Primitives where - /-- - element kind 的标识(`PINNED` 开放宇宙, ADR-0005;表示 `OPEN`)。 - - **刻意用抽象类型而非 `inductive`**:ADR-0005 决定 kind 是开放可扩展宇宙(stdlib - default + 第三方),封闭枚举会直接违背它。这与 `RunState` 的"未封闭"不同——此处 - 开放是**已决策的**。 - -/ - KindId : Type - /-- - 某 kind 的合法数据类型(`PINNED` 依赖关系, ADR-0005;schema 形态 `PINNED` ADR-0006, - 表示仍抽象)。 - - 以 kind 为索引:不同 kind 的合法数据类型不同。这正是 ADR-0005"kind 的最小契约 - = 数据 schema"的载体——`ElementData k` 即"符合 `k` 之 schema 的数据"。 - - schema 的**形态**已由 ADR-0006 定:声明式 **JSON Schema**,字段类型 = 内置标量 + - 一个 `content` 扩展类型;`content` 字段的值是一段 **typst 源**(canonical 存为带 - 虚拟路径的源,语义取其 module body)。但这些是 JSON / typst 的内部结构——**实现 - 细节,非分歧点**,不进 Lean。故 `ElementData` 在此**仍是抽象类型**:契约只承诺 - "存在一个由 kind 决定的合法数据类型",不复刻 JSON Schema / typst Content 的形状。 - -/ - ElementData : KindId → Type - /-- export target 的标识(`PINNED` 角色, ADR-0005;表示 `OPEN`)。一个 target 是一次 build,产出对 lesson 的一种投影(讲义/教案/PPT/平台 archive…),见 `Render`。 -/ - TargetId : Type - --- 注:原有 `RenderRule : Type` 已随 ADR-0011 移除。渲染的"how"不再是契约层的 per-target --- 载荷,而是 `Render.TargetSpec.steps` 里 `typstCompile` step 所引用的**模板文件**承载; --- 契约只保留覆盖声明 `TargetSpec.covers`(该 target 渲染哪些 kind),供种子诊断用。 - -end Spec.Courseware diff --git a/spec/Spec/Courseware/QuestionBank.lean b/spec/Spec/Courseware/QuestionBank.lean deleted file mode 100644 index f0450be..0000000 --- a/spec/Spec/Courseware/QuestionBank.lean +++ /dev/null @@ -1,17 +0,0 @@ -import Spec.Courseware.Element - -/-! -# QuestionBank —— 题库(骨架,核心关系 OPEN) - -题库是整个方案里与工程文件并列的资产(讨论里类比 DAW 的 sample library):有自身 -结构的被建模实体,又是最典型的可复用单元,lesson 会引用它。 - -但**题库与 element 的关系尚未决策**,且用户明确指出"纯引用可能不够": -- element 内联题目数据(如交互教具那样),还是 -- lesson 持一个指向题库条目的**引用**,还是 -- 两者并存? - -这是一个 `OPEN` 分歧点。按宪法第 2 条,本模块**不替它选解**——不建 `QuestionRef` -也不建内联结构,只在此 surface 该问题。待专门的 ADR 落定后再填。本文件当前只承载 -这条说明,不引入任何承诺性声明。 --/ diff --git a/spec/Spec/Courseware/Render.lean b/spec/Spec/Courseware/Render.lean deleted file mode 100644 index 25a0d0c..0000000 --- a/spec/Spec/Courseware/Render.lean +++ /dev/null @@ -1,88 +0,0 @@ -import Spec.Courseware.Primitives -import Spec.Courseware.Artifact - -/-! -# Render —— export target = artifact + 有序 typed steps(ADR-0009 / 0011) - -ADR-0009:export target 是**一次 build**,产出一个有类型的 `Artifact`。ADR-0011 钉死 -build 的**形状**:一个 target 是 `artifact` + 一串**有序的 typed step**。每个 step 是一个 -**有类型的操作**: - -- `typstCompile template` —— 把**模板文件**(如 `exports/student.typ`)编译成产物。它是 - *typed* 而非裸 shell,正因框架要把 **manifest 注入**模板(经 `--input manifest=…`), - 裸 `typst compile` 字符串表达不了这个 wiring。presentation(numbly 编号、样式)住在 - 模板里,**不**在 manifest。 -- `shell run` —— 逃生口,给难以声明的步骤(ADR-0005 的 (b) 类 medium-only:HTML 交互、 - npm build 落这)。 - -MVP 每个 target 只有一个 `typstCompile` step,但 `steps` 是 **list**,因为 `FileTree` / -第三方 build 会需要多步。 - -**渲染覆盖**:ADR-0011 废止了 per-target 的 `RenderRule` 载荷——渲染的"how"已移进模板。 -契约只保留**覆盖声明** `covers : KindId → Prop`(该 target 渲染哪些 kind),供种子诊断用; -模板是其实现。`RenderConfig.covers`/`renderIgnored` 据此,ADR-0005 种子规则不变。 --/ - -namespace Spec.Courseware - -variable (P : Primitives) - -/-- -一个 build **step**(`PINNED` typed, ADR-0011;可扩展)。 - -- `typstCompile (template)` —— 编译模板文件(相对工程根的路径)成产物;框架把 manifest - 注入它。**typed** 的理由:注入这件事裸 shell 写不出。 -- `shell (run)` —— 逃生口,执行 `run` 命令(ADR-0005 的 (b) 类落这)。MVP 不实现,先建结构。 - -**刻意不**把模板内部、shell 命令的解析结构写进来:那是实现细节(ADR-0011 OPEN)。此处只钉 -"step 是有类型操作,目前两型,可扩展"这一骨架。 --/ -inductive Step where - /-- 编译模板文件 `template`(相对工程根)成产物;框架注入 manifest。 -/ - | typstCompile (template : String) - /-- shell 逃生口:执行命令 `run`。 -/ - | shell (run : String) - -/-- -一个 export target 的 build 规格(`PINNED` artifact + 有序 steps, ADR-0011)。 - -- `artifact` —— 产物(`Courseware.Artifact`,带字段)。决定 build 折叠成单文件还是文件树。 -- `steps` —— **有序** step 列表。按序执行;MVP 仅一个 `typstCompile`。 -- `covers` —— **覆盖声明**:`covers k` 表示此 target **渲染** kind `k`。这是 ADR-0011 把 - 旧 `renders : KindId → Option RenderRule` 降级后的产物——契约只声明"渲染哪些 kind" - (种子诊断 `renderIgnored` 用),渲染的"how"由 `steps` 的模板实现,不再是契约层载荷。 --/ -structure TargetSpec where - /-- 产物(带字段, ADR-0011)。 -/ - artifact : Artifact - /-- 有序 build steps。 -/ - steps : List Step - /-- 覆盖声明:此 target 是否渲染该 kind。 -/ - covers : P.KindId → Prop - -/-- -渲染配置(`PINNED` target-中心, ADR-0009/0011)。 - -`spec t = none` 表示 target `t` **未声明**(此工程文件不导出该 target);`some s` 给出该 -target 的 build 规格 `s`(artifact + steps + 覆盖声明)。 --/ -structure RenderConfig where - /-- target ↦ 该 target 的 build 规格(未声明则 `none`)。 -/ - spec : P.TargetId → Option (TargetSpec P) - -/-- -kind `k` 在 target `t` 下**被渲染**(`PINNED`, ADR-0009/0011;承接 ADR-0005 `covers`)。 - -成立 ⟺ target `t` 已声明(`spec t = some s`)**且**其覆盖声明含 `k`(`s.covers k`)。 -`covers` 为假即"此 kind 在此 target 下不被渲染"——checker 据此报 warning(见 -`Spec.Courseware.Diagnostic.renderIgnored`)。语义与 ADR-0005 连续,只是判定基底从 -"有无 RenderRule"换成"覆盖声明是否含此 kind"(ADR-0011 废 RenderRule 载荷)。`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 diff --git a/spec/Spec/Courseware/RichContent.lean b/spec/Spec/Courseware/RichContent.lean deleted file mode 100644 index eadc61e..0000000 --- a/spec/Spec/Courseware/RichContent.lean +++ /dev/null @@ -1,39 +0,0 @@ -/-! -# RichContent —— 富内容(ADR-0006 的 prose 母本) - -ADR-0006 给 element schema 的"叶子"定了形:一个字段可以是 `content` 类型,其值是 -**一段 typst 源**,语义上取该源作为 module 求值后的 **body content**。 - -关键约束(均 ADR-0006,源自 typst 源码事实):富内容**不可无主**——typst 的源必须 -有 `FileId`,否则 span 脱锚(`span.id() = none`,点击跳转失效)且相对 `import` 报 -"cannot access file system from here"。故每段富内容是 World 里的一等文件,坐落在一个 -**虚拟路径**上;相对 import 限本工程路径结构内 + `@package`(不跨工程)。 - -本模块只为这个概念立一个 prose 锚点 + 一个**最小抽象签名**。typst 的 `Content` / -`Module` 内部结构、JSON Schema 的形状都是**实现细节、非分歧点**,不进 Lean——这里 -不复刻它们,只承诺"富内容由一个虚拟路径定位"这一条 ADR-0006 钉死的关系。 --/ - -namespace Spec.Courseware - -/-- -富内容在工程文件路径结构中的**虚拟路径**(`OPEN` 表示, ADR-0006)。 - -它把一段富内容定位为 World 里的一等文件(span 可解析、相对 import 可锚定)。其具体 -表示——以及它落到磁盘后就是真实相对路径(ADR-0007)——不在本层承诺,故 opaque。 --/ -opaque VPath : Type - -/-- -对一段富内容的**引用**:它坐落在某个虚拟路径上(`PINNED` 关系, ADR-0006)。 - -契约层面,一段 `content` 字段值由其虚拟路径标识(canonical 存储是该路径下的 typst -源文本,而非序列化的 `Content`——后者不可反序列化)。这里**刻意不**建模源文本、 -不建模求值出的 `Content`:那是实现侧的事。此结构只钉死"富内容经由一个 `VPath` -定位"这一条关系,作为 `Primitives.ElementData` 里 `content` 叶子的语义锚点。 --/ -structure RichContentRef where - /-- 该富内容所在的虚拟路径(ADR-0006;落盘后为真实相对路径, ADR-0007)。 -/ - vpath : VPath - -end Spec.Courseware diff --git a/spec/Spec/Prelude.lean b/spec/Spec/Prelude.lean index 5c96fdf..df99553 100644 --- a/spec/Spec/Prelude.lean +++ b/spec/Spec/Prelude.lean @@ -1,37 +1,24 @@ /-! # Prelude —— System 层共享标识符 -平台层(`Spec.System`)反复引用一组**标识符**(项目、run、session、principal)。 -它们在 likec4 / ADR 里只作为引用键出现,**内部表示从未被决策**(是 UUID 还是 -复合键、principal 怎么分类),也不构成语义分歧点。 - -故把它们收口成一个 opaque 载体 `Identifiers`,System 各模块在其上参数化。这样 -契约谈得了"锁的 owner 是哪个 run""grant 授给哪个 principal"这类**关系**,却 -不对标识符的表示作任何承诺。 +平台层反复引用一组标识符(项目、run、session、principal)。其内部表示从未被决策 +(UUID / 复合键、principal 子类型学),也非分歧点,故收口成 opaque 载体 +`Identifiers`,System 各模块在其上参数化——契约谈得了"锁 owner 是哪个 run"这类 +**关系**,却不对标识符表示作承诺。 -/ namespace Spec.System -/-- -System 层标识符载体(`OPEN` 表示,关系结构 `PINNED`)。 - -每个字段是一个 opaque 类型:契约只用它做引用键,绝不假设其内部表示。System 各 -模块 `variable (I : Identifiers)` 后即可引用 `I.ProjectId` 等。 --/ +/-- System 层标识符载体(关系结构 `PINNED`;各字段表示 `OPEN`)。 -/ structure Identifiers where - /-- 课程项目的标识(`OPEN` 表示;聚合根,见 likec4 `Project`)。 -/ + /-- 课程项目标识(`OPEN` 表示;聚合根,likec4 `Project`)。 -/ ProjectId : Type - /-- 一次 Claude 处理任务的标识(`OPEN` 表示;锁的 owner、审计主体,见 `AgentRun`)。 -/ + /-- 一次 Claude 任务的标识(`OPEN` 表示;锁的 owner、审计主体,`AgentRun`)。 -/ RunId : Type - /-- 长生命周期 Claude 会话的标识(`OPEN` 表示;跨多 run 复用,ADR-0002)。 -/ + /-- 长生命周期 Claude 会话标识(`OPEN` 表示;跨多 run 复用,ADR-0002)。 -/ SessionId : Type - /-- - 权限主体的标识(`OPEN` 表示及其**子类型学**)。 - - ADR-0004 列出 principal 可以是 user / feishu_chat / department / user_group / - app。这套子类型学本身**未定且非本层分歧点**(纯 plumbing),故此处只留 opaque - 键,不展开为 `inductive`。 - -/ + /-- 权限主体标识(`OPEN` 表示及其子类型学;ADR-0004 的 user/chat/department/… + 子类型学未定且非本层分歧点,纯 plumbing,故只留 opaque 键)。 -/ Principal : Type end Spec.System diff --git a/spec/Spec/System.lean b/spec/Spec/System.lean index 5659c01..d1ae702 100644 --- a/spec/Spec/System.lean +++ b/spec/Spec/System.lean @@ -6,9 +6,9 @@ import Spec.System.Audit /-! # System —— Hub 平台层契约 -协作与执行的平台:项目、飞书群、AgentRun、锁、权限、审计。`main` 分支的 likec4 -(`docs/architecture/likec4/`)已画出这一层的**结构**(9 实体 + 容器 + 视图);本层 -只补 likec4 画不出的**语义分歧点**,不重复结构: +协作与执行的平台:项目、飞书群、AgentRun、锁、权限、审计。likec4 +(`docs/architecture/likec4/`)已画出这一层的**结构**;本层只补 likec4 画不出的 +**语义分歧点**: - `Run` —— AgentRun 状态与终止判定(状态集合完整性 OPEN)。 - `Lock` —— 锁 owner=run(ADR-0002),及"持锁者必为非终止 run"的核心不变式。 diff --git a/spec/Spec/System/Audit.lean b/spec/Spec/System/Audit.lean index 93da09d..114d4d1 100644 --- a/spec/Spec/System/Audit.lean +++ b/spec/Spec/System/Audit.lean @@ -3,23 +3,18 @@ import Spec.Prelude /-! # Audit —— 审计日志(有意从简) -likec4 把 `AuditLog` 列为实体:`AgentRun -> AuditLog 'records lifecycle events'`, -admin 经控制台审计。但**审计记录里装什么**(事件 schema、保留策略、可查询维度) -在任何 ADR / 散文里都未决策,且大多是 plumbing——按分歧点测试**不入契约**:写明 -与否不会让开发者与 agent 各做不同假设。 - -故本模块**刻意几乎为空**:只固定一条已决策的关系——审计以 run 为主体记录其生命 -周期事件——其余 `OPEN`。这里留白本身是契约的一部分(承诺"此处尚无答案,勿填")。 +likec4 把 `AuditLog` 列为实体(`AgentRun -> AuditLog 'records lifecycle events'`), +但**审计记录里装什么**(事件 schema、保留策略、可查询维度)在任何 ADR / 散文里都 +未决策,且大多是 plumbing——按分歧点测试不入契约。故本模块刻意几乎为空:只固定 +"审计以 run 为主体记录其生命周期事件"这一条已决策关系,其余 `OPEN`(留白本身是 +契约的一部分:承诺此处尚无答案、勿填)。 -/ namespace Spec.System -/-- -审计条目的最小骨架(关系 `PINNED` / 内容 `OPEN`, likec4 `records lifecycle events`)。 - -只承诺"一条审计记录关联到某个 run"。事件类型、时间、actor、详情等字段**未定** -(`OPEN`),待出现真实分歧点(如"取消必须记录 actor")时再由对应 ADR 落定。 --/ +/-- 审计条目的最小骨架(关系 `PINNED` / 内容 `OPEN`, likec4)。只承诺"一条审计记录 +关联到某个 run";事件类型、时间、actor、详情等字段 `OPEN`,待真实分歧点出现时由 +对应 ADR 落定。 -/ structure AuditEntry (I : Identifiers) where /-- 该审计条目所属的 run(`PINNED` 关系, likec4)。 -/ run : I.RunId diff --git a/spec/Spec/System/Lock.lean b/spec/Spec/System/Lock.lean index db26b85..94a0e22 100644 --- a/spec/Spec/System/Lock.lean +++ b/spec/Spec/System/Lock.lean @@ -4,46 +4,32 @@ import Spec.System.Run /-! # Lock —— 项目锁与排他不变式 -ADR-0002 的核心:防止并发 Claude 执行同时改一个项目,而锁的 **owner 是当前 -`AgentRun`**(不是 teacher / chat / session)。本模块把这条决策编码进类型,并钉死 -likec4 画不出的那条语义不变式——**持锁者必为非终止 run**。 +ADR-0002 的核心:防止并发 Claude 同改一个项目,锁的 **owner 是当前 `AgentRun`** +(不是 teacher / chat / session)。本模块把这条决策编码进类型,并钉死那条 +likec4 画不出的语义不变式——**持锁者必为非终止 run**。 -/ namespace Spec.System variable (I : Identifiers) -/-- -项目级锁(`PINNED`, ADR-0002)。 - -`owner` 的类型是 `RunId` 而非 `SessionId`/`Principal`——这从类型上编码 ADR-0002 -"lock owner = run_id":锁不可能被一个 session 或 teacher 持有。`scope` 为项目级 -(一个项目一把锁,见 `LockTable`)。 --/ +/-- 项目级锁(`PINNED`, ADR-0002)。`owner : RunId`(非 SessionId/Principal)从类型 +上编码"lock owner = run_id":锁不可能被 session / teacher 持有。 -/ structure ProjectAgentLock where - /-- 锁的作用域:项目级(`PINNED`, ADR-0002 `scope = project_id`)。 -/ + /-- 作用域:项目级(`PINNED`, ADR-0002 `scope = project_id`)。 -/ scope : I.ProjectId - /-- 锁的持有者:一个 run(`PINNED`, ADR-0002 `owner = run_id`)。 -/ + /-- 持有者:一个 run(`PINNED`, ADR-0002 `owner = run_id`)。 -/ owner : I.RunId -/-- -锁表:每个项目当前的持锁 run(`PINNED` 排他性, ADR-0002)。 - -`Option` 编码"每项目至多一把锁":`none` = 无活动 run 占用,`some r` = run `r` -正持有。这个 `ProjectId → Option RunId` 的结构**本身**即排他——不可能为同一项目 -登记两个并发 owner。 --/ +/-- 锁表:每项目当前持锁 run(`PINNED` 排他性, ADR-0002)。`ProjectId → Option RunId` +的结构**本身**即排他——不可能为同一项目登记两个并发 owner。 -/ def LockTable := I.ProjectId → Option I.RunId -/-- -锁表良构:**持锁者必为非终止 run**(`PINNED` 平台核心不变式, ADR-0002)。 +/-- 锁表良构:**持锁者必为非终止 run**(`PINNED` 平台核心不变式, ADR-0002)。 -ADR-0002 说锁在 run 终止时释放。其逻辑等价物:任何时刻,若项目 `p` 的锁被 `r` -持有,则 `r` 不在终止态。`statusOf` 给出每个 run 的当前状态。 - -这条不变式把 **Lock 与 Run 两个实体耦合**起来——likec4 能画"run owns lock while -running"这条边,但画不出"终止即必须释放"这个**约束**;它正是契约相对结构图的增量。 --/ +"锁在 run 终止时释放"的逻辑等价物:若 `p` 的锁被 `r` 持有,则 `r` 不在终止态。这条 +把 Lock 与 Run 耦合起来——likec4 能画"run owns lock while running",画不出"终止即 +必须释放"这个约束;它正是契约相对结构图的增量。 -/ def LockTable.WellFormed (lt : LockTable I) (statusOf : I.RunId → RunState) : Prop := ∀ p r, lt p = some r → ¬ (statusOf r).Terminal diff --git a/spec/Spec/System/Permission.lean b/spec/Spec/System/Permission.lean index 9edf44a..daffb18 100644 --- a/spec/Spec/System/Permission.lean +++ b/spec/Spec/System/Permission.lean @@ -3,31 +3,22 @@ import Spec.Prelude /-! # Permission —— 角色、能力与授权 -ADR-0004:权限走"飞书云文档式"——**协作者授权(grant)与操作设置(settings) -分离**;grant 是 `resource + principal + role`,role 取自封闭的 `read / edit / -manage`,且 **read ⊂ edit ⊂ manage** 累积赋能;强制释放锁是 **admin-only**,在 -role 体系之外。本模块把这套结构与"高 role 含低 role 全部能力"的单调性钉死。 +ADR-0004:权限走"飞书云文档式"——grant(`resource + principal + role`)与 settings +分离;role 取自封闭的 `read / edit / manage`,且 **read ⊂ edit ⊂ manage** 累积赋能; +强制释放锁是 **admin-only**,在 role 体系之外。本模块把这套结构与"高 role 含低 +role 全部能力"的单调性钉死。 -/ namespace Spec.System -/-- -协作者角色(`PINNED` 封闭, ADR-0004 逐字 "roles are read, edit, or manage")。 - -与 element-kind / RunState 不同,这里 ADR **明示**只有三个 role,故 `inductive` -是封闭授权,不是"尚未封闭"。 --/ +/-- 协作者角色(`PINNED` 封闭, ADR-0004 逐字 "roles are read, edit, or manage")。 -/ inductive Role where | read | edit | manage -/-- -角色的**赋能层级**(`PINNED` 序, ADR-0004 read⊂edit⊂manage)。 - -把 ADR-0004 的累积包含关系数值化:read=0 ⊂ edit=1 ⊂ manage=2。它只服务于下面的 -`Role.le` 与能力推导,不对外承诺"层级就是个 `Nat`"。 --/ +/-- 角色赋能层级(`PINNED` 序, ADR-0004 read⊂edit⊂manage 数值化)。仅服务于 +`Role.le` 与能力推导,不对外承诺"层级就是 `Nat`"。 -/ def Role.level : Role → Nat | .read => 0 | .edit => 1 @@ -36,16 +27,9 @@ def Role.level : Role → Nat /-- 角色偏序:`r₁ ≤ r₂` 即 `r₁` 赋能不强于 `r₂`(`PINNED`, ADR-0004)。 -/ def Role.le (r₁ r₂ : Role) : Prop := r₁.level ≤ r₂.level -/-- -受 role 调控的操作能力(项 `PINNED` 取自 ADR-0004;**枚举完整性 `OPEN`**)。 - -逐项来源于 ADR-0004 对各 role 的展开:`view`(read);`discussComment` / -`editArtifact` / `triggerAgent` / `answerChoiceCard`(edit);`manageCollaborators` -/ `projectSettings` / `groupBinding` / `normalCancel`(manage)。 - -⚠ **完整性 OPEN**:这是 ADR 当前点名的能力,不保证穷尽;新增产品操作时可能扩。 -注意 **force-release 不在此列**——它是 admin-only override,见 `RequiresAdmin`。 --/ +/-- 受 role 调控的操作能力(各项 `PINNED` 取自 ADR-0004;**枚举完整性 `OPEN`**—— +这是 ADR 当前点名的能力,不保证穷尽,新增产品操作时可能扩)。注意 force-release +**不在此列**——它是 admin-only override,见 `RequiresAdmin`。 -/ inductive Capability where | view | discussComment @@ -57,43 +41,26 @@ inductive Capability where | groupBinding | normalCancel -/-- -某能力所**要求的最低角色**(`PINNED`, ADR-0004 各 role 的能力展开)。 - -read 级仅 `view`;edit 级是讨论/评论、编辑产物、触发 Claude、应答 choice card; -manage 级是协作者管理、项目设置、群绑定、常规取消。授权判定 `Role.can` 据此定义, -从而"谁能做什么"只有这一处真相。 --/ +/-- 某能力所**要求的最低角色**(`PINNED`, ADR-0004 各 role 能力展开)。授权判定 +`Role.can` 据此定义,"谁能做什么"只有这一处真相。 -/ def Capability.requiredRole : Capability → Role | .view => .read | .discussComment | .editArtifact | .triggerAgent | .answerChoiceCard => .edit | .manageCollaborators | .projectSettings | .groupBinding | .normalCancel => .manage -/-- -角色 `r` **具备**能力 `c`(`PINNED`, ADR-0004)。 - -定义为"`c` 要求的最低角色 ≤ `r`"。这一处定义同时编码了 read⊂edit⊂manage 的累积性: -manage 自动具备所有 edit / read 能力,无需逐条列举。 --/ +/-- 角色 `r` **具备**能力 `c`(`PINNED`, ADR-0004)。定义为"`c` 的最低角色 ≤ `r`", +这一处同时编码了 read⊂edit⊂manage 的累积性。 -/ def Role.can (r : Role) (c : Capability) : Prop := c.requiredRole |>.le r -/-- -**单调性**:角色越高,能力只增不减(`PINNED` 定理, ADR-0004 累积赋能)。 - -这是 read⊂edit⊂manage 的形式化保证:若 `r₁ ≤ r₂` 且 `r₁` 能做 `c`,则 `r₂` 也能。 -证明即偏序传递性——之所以成立得这么干净,正因为 `can` 是按"最低角色阈值"定义的。 --/ +/-- **单调性**:`r₁ ≤ r₂` 且 `r₁` 能做 `c` ⇒ `r₂` 也能(`PINNED` 定理, ADR-0004 累积 +赋能的形式化保证)。证明即偏序传递性,得益于 `can` 按"最低角色阈值"定义。 -/ theorem Role.can_mono {r₁ r₂ : Role} {c : Capability} (h : r₁.le r₂) (hc : r₁.can c) : r₂.can c := Nat.le_trans hc h -/-- -**强制释放锁**要求 admin,**在 role 体系之外**(`PINNED`, ADR-0004 admin-only override)。 - -ADR-0004 明确:force release 卡住的锁是异常操作,不是任何协作者 role 的能力—— -即便 `manage` 也不经由 `Role.can` 获得它。故它不是一个 `Capability`,而是这样一个 -独立谓词:仅当主体是 admin 时成立。`isAdmin` 由平台另行判定(本层不建 admin 模型)。 --/ +/-- **强制释放锁**要求 admin,**在 role 体系之外**(`PINNED`, ADR-0004 admin-only +override)。即便 `manage` 也不经 `Role.can` 获得它,故它不是 `Capability` 而是独立 +谓词;`isAdmin` 由平台另行判定(本层不建 admin 模型)。 -/ def RequiresAdmin (isAdmin : Prop) : Prop := isAdmin end Spec.System diff --git a/spec/Spec/System/Run.lean b/spec/Spec/System/Run.lean index ba7c1c8..7662200 100644 --- a/spec/Spec/System/Run.lean +++ b/spec/Spec/System/Run.lean @@ -1,30 +1,16 @@ /-! # Run —— AgentRun 状态机 -一次 `@Claude` 创建一个 `AgentRun`(ADR-0001),它在生命周期里经历若干状态,并在 -**终止时释放项目锁**(ADR-0002)。本模块固定 run 的**状态**与**终止判定**——后者 -是 Lock 排他不变式(见 `Spec.System.Lock`)的依赖。 - -完整的合法转移关系**未在任何 ADR / likec4 散文里定下**,故本模块不臆造转移边, -只刻画状态本身与"何为终止"。 +一次 `@Claude` 创建一个 `AgentRun`(ADR-0001),它在终止时释放项目锁(ADR-0002)。 +合法转移关系在任何 ADR / likec4 散文里都未定下,故本模块只刻画**状态**与**终止 +判定**(后者是 Lock 排他不变式的依赖),不臆造转移边。 -/ namespace Spec.System -/-- -AgentRun 的运行状态(状态名 `PINNED` 取自 ADR-0001..0003 + likec4 散文; -**集合完整性 `OPEN`**)。 - -各状态来源:`active`(run 进行中)、`waitingForUser`(likec4 Run Orchestrator -"等待用户")、`completed` / `failed` / `timedOut` / `canceled`(ADR-0002 列出的 -释放锁时机)。 - -⚠ **完整性是 OPEN**:散文从未声明"状态恰好这些"。这里用 `inductive` 是为了能 -谈终止判定与不变式,**不等于**封闭授权——若实现侧发现还需要别的状态(如排队中 -的 pending),那是一个待 surface 的分歧点,**不得**默认本枚举已穷尽。这与 -element-kind 那种**明示开放**的宇宙性质不同:那里"开放"是决策,这里"未封闭"是 -尚未决策。 --/ +/-- AgentRun 运行状态(状态名 `PINNED`, ADR-0001..0003 + likec4;**完整性 `OPEN`** +——散文从未声明"状态恰好这些";实现若需新状态(如 pending)须 surface,不得默认 +本枚举已穷尽)。终止态见 `RunState.Terminal`。 -/ inductive RunState where | active | waitingForUser @@ -33,13 +19,8 @@ inductive RunState where | timedOut | canceled -/-- -run 处于**终止态**(`PINNED`, ADR-0002)。 - -ADR-0002 钉死:锁在 run `completes / fails / times out / is canceled` 时释放。 -这四个状态即终止态;锁的释放时机由它定义(见 `Spec.System.Lock.LockTable.WellFormed`)。 -`active` 与 `waitingForUser` 非终止——后者虽在等待,run 仍占用项目(锁未释放)。 --/ +/-- run 处于**终止态**(`PINNED`, ADR-0002:锁在 completes/fails/timesOut/canceled +时释放)。`active`/`waitingForUser` 非终止——后者仍占用项目(锁未释放)。 -/ def RunState.Terminal : RunState → Prop | .completed | .failed | .timedOut | .canceled => True | .active | .waitingForUser => False