forked from EduCraft/curriculum-project-hub
chore(spec+checker): cleanup pass — trim docs, reorg Courseware, covers-as-data, fold DanglingReference (ADR-0012)
Spec母本噪音清理 + 一处 spec↔impl 对齐 + 一处契约自洽修正。 Part A — spec doc 瘦身:每条 doc 收到"语义点 + 标签 + ADR ref + 承载性 why", 把跨文件复读的方法论(element-kind 开放性对比、likec4 画不出、分歧点测试)上移到 module header。OPEN 框架保持清晰(RunState/Capability 完整性仍明示须 surface)。 Part B — Courseware/ 由 10 文件平铺重组为 Model/ Export/ Check/ Open/ 四子命名空间 (namespace Spec.Courseware 不变,零引用改动)+ 四个子 aggregator。lake build 绿(24 jobs)。 Part C — 渲染覆盖落为数据(ADR-0011 对齐):去掉 cph-check 里硬编码的 COVERED_TARGETS,改读 TargetConfig.covers。cph-model 新增 covers: Option<Vec<String>> (None=未声明,由 cph-check 默认为全部 known kinds;显式 [] 表示不覆盖任何 kind)。 新增 3 个覆盖行为测试。 ADR-0012 — DanglingReference 退役(诊断 7→6 类):其两种情形(未解析 @ref、越界/缺失 相对 import)都是 typst 编译期失败,归 typstCompile。同步移除 Oracle.refsResolve (被 compiles 蕴含),Legal 少一个合取项。impl 删去从未被发射的 DiagCode::DanglingReference, 闭合 named-but-unemitted 的 spec↔impl 缝。ADR-0010 加修订指针。 OPEN 点(RunState/Capability 完整性、QuestionBank、Course)按既定纪律保持 OPEN,本次 只改善其框架措辞,不决策。 验证:spec lake build 绿;cargo test 全绿(含新增覆盖测试);clippy 静默; TH-141 check 0 errors/0 warnings 无回归。 Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This commit is contained in:
+23
-17
@@ -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<Diagnostic> {
|
||||
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<Diagnostic
|
||||
continue;
|
||||
}
|
||||
for target in &lesson.targets {
|
||||
let covered = COVERED_TARGETS.contains(&target.name.as_str());
|
||||
// Resolve the coverage set: an absent declaration defaults to the
|
||||
// full known-kind universe; an explicit list (possibly empty) is
|
||||
// taken verbatim.
|
||||
let covered = match &target.covers {
|
||||
None => 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<Diagnostic
|
||||
let mut d = Diagnostic::warning(
|
||||
DiagCode::RenderIgnored,
|
||||
format!(
|
||||
"kind '{}' has no render rule for target '{}'; it will be omitted from that export",
|
||||
"kind '{}' is not covered by target '{}'; it will be omitted from that export",
|
||||
part.kind, target.name
|
||||
),
|
||||
)
|
||||
.with_hint(format!(
|
||||
"add a render rule for kind '{}' under target '{}', or remove the target",
|
||||
"add '{}' to `covers` under target '{}', or remove the target",
|
||||
part.kind, target.name
|
||||
));
|
||||
// Pin the severity via the named contract const. `Diagnostic::warning`
|
||||
|
||||
@@ -136,6 +136,132 @@ path = "segments/does-not-exist"
|
||||
cleanup(&tmp);
|
||||
}
|
||||
|
||||
/// Write a throwaway one-segment lesson into `tmp`, with the given `[targets.x]`
|
||||
/// body spliced in. Returns nothing; the caller runs `check`.
|
||||
fn write_segment_lesson_with_target(tmp: &PathBuf, target_body: &str) {
|
||||
std::fs::write(
|
||||
tmp.join("manifest.toml"),
|
||||
format!(
|
||||
r#"
|
||||
[project]
|
||||
id = "cov"
|
||||
name = "cov"
|
||||
|
||||
[info]
|
||||
title = "cov"
|
||||
|
||||
[[parts]]
|
||||
kind = "segment"
|
||||
path = "segments/intro"
|
||||
|
||||
{target_body}
|
||||
"#
|
||||
),
|
||||
)
|
||||
.unwrap();
|
||||
let part_dir = tmp.join("segments").join("intro");
|
||||
std::fs::create_dir_all(&part_dir).unwrap();
|
||||
std::fs::write(part_dir.join("element.toml"), "kind = \"segment\"\n").unwrap();
|
||||
std::fs::write(part_dir.join("textbook.typ"), "Hello.\n").unwrap();
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn covers_omitting_used_kind_warns_render_ignored() {
|
||||
// A target that declares `covers = ["example"]` does NOT cover the lesson's
|
||||
// `segment` part → exactly one RenderIgnored warning (non-blocking).
|
||||
let tmp = tempdir();
|
||||
write_segment_lesson_with_target(
|
||||
&tmp,
|
||||
r#"[targets.handout]
|
||||
artifact = { type = "single-file", filepath = "build/handout.pdf" }
|
||||
covers = ["example"]
|
||||
[[targets.handout.steps]]
|
||||
type = "typst-compile"
|
||||
template = "exports/handout.typ"
|
||||
"#,
|
||||
);
|
||||
|
||||
let report = cph_check::check(&tmp, &engine());
|
||||
assert!(report.lesson_loaded);
|
||||
let render_ignored: 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 {
|
||||
|
||||
@@ -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",
|
||||
|
||||
@@ -4,7 +4,7 @@
|
||||
//! `<root>/manifest.toml` (project / info / ordered `[[parts]]` / declared
|
||||
//! `[targets.*]`) and each part's `<root>/<path>/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/<name>.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.<name>]` table key).
|
||||
@@ -82,12 +85,25 @@ pub struct TargetConfig {
|
||||
/// The ordered build steps. Defaults to a single [`Step::TypstCompile`]
|
||||
/// with template `exports/<name>.typ` when no `[[steps]]` are given.
|
||||
pub steps: Vec<Step>,
|
||||
/// 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<Vec<String>>,
|
||||
}
|
||||
|
||||
/// 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<Diagnostic>) -
|
||||
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<Diagnostic>) -
|
||||
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<Diagnostic>) -> Option<Vec<String>> {
|
||||
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",
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
@@ -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(),
|
||||
};
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -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 `<field>.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.
|
||||
+15
-29
@@ -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`。
|
||||
-/
|
||||
|
||||
@@ -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
|
||||
@@ -0,0 +1,9 @@
|
||||
import Spec.Courseware.Check.Diagnostic
|
||||
import Spec.Courseware.Check.Pipeline
|
||||
|
||||
/-!
|
||||
# Courseware.Check —— checker 语义
|
||||
|
||||
诊断分类与合法 lesson(`Diagnostic`)、检查管线的阶段与序(`Pipeline`)。决策出处
|
||||
ADR-0010。
|
||||
-/
|
||||
@@ -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` 字段缺对应 `<field>.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
|
||||
@@ -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
|
||||
@@ -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。本文件当前不引入任何
|
||||
承诺性声明。
|
||||
-/
|
||||
@@ -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` 字段缺对应 `<field>.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
|
||||
@@ -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
|
||||
@@ -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。
|
||||
-/
|
||||
@@ -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
|
||||
@@ -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
|
||||
@@ -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
|
||||
@@ -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。
|
||||
-/
|
||||
@@ -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
|
||||
@@ -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
|
||||
@@ -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
|
||||
@@ -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
|
||||
@@ -0,0 +1,9 @@
|
||||
import Spec.Courseware.Open.QuestionBank
|
||||
import Spec.Courseware.Open.Course
|
||||
|
||||
/-!
|
||||
# Courseware.Open —— 留白骨架(核心关系 OPEN)
|
||||
|
||||
题库与 element 的关系(`QuestionBank`)、课程编排规则(`Course`)。两者均为已 surface
|
||||
但未决策的分歧点,按宪法第 2 条不臆造,待专门 ADR 落定。
|
||||
-/
|
||||
@@ -0,0 +1,10 @@
|
||||
/-!
|
||||
# Course —— 课程编排(骨架,规则 OPEN)
|
||||
|
||||
ADR-0005:工程文件的粒度是**单节课**;course / 单元**不是**工程文件,而是 lesson 的
|
||||
**编排**。但"编排"的具体规则未决策:有序列表还是带层级(单元 → 课)的树?lesson 被
|
||||
引用还是被包含?跨 lesson 有无约束(目标覆盖、前后置)?这些都是 `OPEN`。
|
||||
|
||||
按宪法第 2 条本模块**不臆造**编排结构——不建 `Course := List Lesson`(那会偷偷承诺
|
||||
"扁平有序、无层级")。只在此 surface:课程编排待专门 ADR。本文件当前不引入任何承诺性声明。
|
||||
-/
|
||||
@@ -0,0 +1,10 @@
|
||||
/-!
|
||||
# QuestionBank —— 题库(骨架,核心关系 OPEN)
|
||||
|
||||
题库是与工程文件并列的资产(类比 DAW 的 sample library):有自身结构的实体,又是最
|
||||
典型的可复用单元,lesson 会引用它。但**题库与 element 的关系尚未决策**,且用户明确
|
||||
指出"纯引用可能不够"——element 内联题目数据 / lesson 持指向题库条目的引用 / 两者并存?
|
||||
|
||||
这是一个 `OPEN` 分歧点。按宪法第 2 条本模块**不替它选解**——不建 `QuestionRef` 也不建
|
||||
内联结构,只在此 surface。待专门 ADR 落定后再填。本文件当前不引入任何承诺性声明。
|
||||
-/
|
||||
@@ -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
|
||||
@@ -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
|
||||
@@ -1,17 +0,0 @@
|
||||
import Spec.Courseware.Element
|
||||
|
||||
/-!
|
||||
# QuestionBank —— 题库(骨架,核心关系 OPEN)
|
||||
|
||||
题库是整个方案里与工程文件并列的资产(讨论里类比 DAW 的 sample library):有自身
|
||||
结构的被建模实体,又是最典型的可复用单元,lesson 会引用它。
|
||||
|
||||
但**题库与 element 的关系尚未决策**,且用户明确指出"纯引用可能不够":
|
||||
- element 内联题目数据(如交互教具那样),还是
|
||||
- lesson 持一个指向题库条目的**引用**,还是
|
||||
- 两者并存?
|
||||
|
||||
这是一个 `OPEN` 分歧点。按宪法第 2 条,本模块**不替它选解**——不建 `QuestionRef`
|
||||
也不建内联结构,只在此 surface 该问题。待专门的 ADR 落定后再填。本文件当前只承载
|
||||
这条说明,不引入任何承诺性声明。
|
||||
-/
|
||||
@@ -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
|
||||
@@ -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
|
||||
+10
-23
@@ -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
|
||||
|
||||
@@ -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"的核心不变式。
|
||||
|
||||
@@ -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
|
||||
|
||||
+13
-27
@@ -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
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -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
|
||||
|
||||
Reference in New Issue
Block a user