forked from bai/curriculum-project-hub
Compare commits
5 Commits
| Author | SHA1 | Date | |
|---|---|---|---|
|
4c697904e6
|
|||
|
3c1eb846a9
|
|||
|
ebcb3a7589
|
|||
|
57f7773987
|
|||
|
4a9eb59aa9
|
Generated
+16
-6
@@ -294,6 +294,15 @@ dependencies = [
|
||||
"strsim",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "clap_complete"
|
||||
version = "4.6.5"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "e0a7a9bfdb35811f9e59832f0f05975114d2251b415fb534108e6f34060fd772"
|
||||
dependencies = [
|
||||
"clap",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "clap_derive"
|
||||
version = "4.6.1"
|
||||
@@ -386,7 +395,7 @@ dependencies = [
|
||||
|
||||
[[package]]
|
||||
name = "cph-check"
|
||||
version = "0.0.1"
|
||||
version = "0.0.2"
|
||||
dependencies = [
|
||||
"cph-diag",
|
||||
"cph-model",
|
||||
@@ -396,9 +405,10 @@ dependencies = [
|
||||
|
||||
[[package]]
|
||||
name = "cph-cli"
|
||||
version = "0.0.1"
|
||||
version = "0.0.2"
|
||||
dependencies = [
|
||||
"clap",
|
||||
"clap_complete",
|
||||
"cph-check",
|
||||
"cph-diag",
|
||||
"cph-typst",
|
||||
@@ -406,14 +416,14 @@ dependencies = [
|
||||
|
||||
[[package]]
|
||||
name = "cph-diag"
|
||||
version = "0.0.1"
|
||||
version = "0.0.2"
|
||||
dependencies = [
|
||||
"serde",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "cph-model"
|
||||
version = "0.0.1"
|
||||
version = "0.0.2"
|
||||
dependencies = [
|
||||
"cph-diag",
|
||||
"serde",
|
||||
@@ -422,7 +432,7 @@ dependencies = [
|
||||
|
||||
[[package]]
|
||||
name = "cph-schema"
|
||||
version = "0.0.1"
|
||||
version = "0.0.2"
|
||||
dependencies = [
|
||||
"cph-diag",
|
||||
"cph-model",
|
||||
@@ -432,7 +442,7 @@ dependencies = [
|
||||
|
||||
[[package]]
|
||||
name = "cph-typst"
|
||||
version = "0.0.1"
|
||||
version = "0.0.2"
|
||||
dependencies = [
|
||||
"cph-diag",
|
||||
"cph-model",
|
||||
|
||||
+1
-1
@@ -12,7 +12,7 @@ members = [
|
||||
# Shared metadata for all workspace crates. Individual crates inherit these via
|
||||
# `version.workspace = true` / `edition.workspace = true`.
|
||||
[workspace.package]
|
||||
version = "0.0.1"
|
||||
version = "0.0.2"
|
||||
edition = "2021"
|
||||
license = "MIT OR Apache-2.0"
|
||||
|
||||
|
||||
@@ -6,7 +6,7 @@
|
||||
|
||||
## 安装 `cph` 命令行
|
||||
|
||||
当前版本 **0.0.1**。从源码安装(本仓库根目录):
|
||||
当前版本 **0.0.2**。从源码安装(本仓库根目录):
|
||||
|
||||
```sh
|
||||
cargo install --path crates/cph-cli --locked
|
||||
@@ -15,11 +15,19 @@ cargo install --path crates/cph-cli --locked
|
||||
`render` 包已嵌入二进制(build.rs 编译期拷入 + `include_dir!`),所以装好后**无需任何环境变量、不依赖源码树**即可用。渲染包按版本解压到 per-user cache(`~/.cache/cph/render-<version>/` 或 macOS `~/Library/Caches/cph/...`);开发时可设 `CPH_RENDER_DIR` 指向 live `render/` 目录覆盖。
|
||||
|
||||
```sh
|
||||
cph --version # cph 0.0.1
|
||||
cph check <工程目录> # 校验合法性(6 类诊断)
|
||||
cph --version # cph 0.0.2
|
||||
cph check <工程目录> # 校验合法性(7 类诊断)
|
||||
cph build <工程目录> --target student -o build/student.pdf # 渲讲义 PDF
|
||||
```
|
||||
|
||||
**版本契约(ADR-0016):** 教研工程文件根放一个 `.cph-version` 文件,内容为它面向的 cph 版本(如 `0.0.2`)。`cph` 加载时比对自身版本,不相容则报 `E-CPH-VERSION` error 并拒绝(当前判定为版本完全相等;后续可放宽为 semver 区间,只改一处谓词)。`examples/` 与本仓 fixture 已带该文件作为迁移起点;缺文件的工程暂时跳过此检查(OPEN)。
|
||||
|
||||
Shell 补全(可选):
|
||||
|
||||
```sh
|
||||
cph completions zsh > ~/.zfunc/_cph # 或 bash/fish/powershell/elvish
|
||||
```
|
||||
|
||||
## 仓库布局
|
||||
|
||||
```
|
||||
|
||||
@@ -13,3 +13,4 @@ cph-check = { path = "../cph-check" }
|
||||
cph-diag = { workspace = true }
|
||||
cph-typst = { path = "../cph-typst" }
|
||||
clap = { version = "4", features = ["derive"] }
|
||||
clap_complete = "4"
|
||||
|
||||
@@ -46,6 +46,22 @@ enum Command {
|
||||
#[arg(short = 'o', long, value_name = "OUT")]
|
||||
out: Option<PathBuf>,
|
||||
},
|
||||
/// Print a shell-completion script to stdout (clap_complete; ADR-0013 opt-in
|
||||
/// sibling: a local convenience, no lesson involved). Pipe to your shell's
|
||||
/// completion file, e.g. `cph completions zsh > ~/.zfunc/_cph`.
|
||||
Completions {
|
||||
/// Which shell to generate completions for.
|
||||
shell: Shell,
|
||||
},
|
||||
}
|
||||
|
||||
#[derive(Debug, Clone, Copy, clap::ValueEnum)]
|
||||
enum Shell {
|
||||
Bash,
|
||||
Zsh,
|
||||
Fish,
|
||||
PowerShell,
|
||||
Elvish,
|
||||
}
|
||||
|
||||
fn main() -> ExitCode {
|
||||
@@ -59,9 +75,29 @@ fn main() -> ExitCode {
|
||||
match cli.command {
|
||||
Command::Check { path } => run_check(&path, &engine),
|
||||
Command::Build { path, target, out } => run_build(&path, &engine, &target, out),
|
||||
Command::Completions { shell } => run_completions(shell),
|
||||
}
|
||||
}
|
||||
|
||||
/// Emit a shell-completion script for `shell` to stdout. The script is built
|
||||
/// from the same `Cli` clap definition above, so it tracks subcommands/flags as
|
||||
/// they evolve.
|
||||
fn run_completions(shell: Shell) -> ExitCode {
|
||||
use clap::CommandFactory;
|
||||
use clap_complete::Shell as CompShell;
|
||||
|
||||
let sh = match shell {
|
||||
Shell::Bash => CompShell::Bash,
|
||||
Shell::Zsh => CompShell::Zsh,
|
||||
Shell::Fish => CompShell::Fish,
|
||||
Shell::PowerShell => CompShell::PowerShell,
|
||||
Shell::Elvish => CompShell::Elvish,
|
||||
};
|
||||
let mut cmd = Cli::command();
|
||||
clap_complete::generate(sh, &mut cmd, "cph", &mut std::io::stdout());
|
||||
ExitCode::SUCCESS
|
||||
}
|
||||
|
||||
/// Print every diagnostic in `report` to stderr, followed by a summary line.
|
||||
fn print_diagnostics(report: &CheckReport) {
|
||||
for d in &report.diagnostics {
|
||||
|
||||
@@ -88,6 +88,9 @@ pub enum DiagCode {
|
||||
TypstCompile,
|
||||
/// An element is ignored under a render target (ADR-0005: warning).
|
||||
RenderIgnored,
|
||||
/// The engineering file's `.cph-version` is not compatible with the running
|
||||
/// CLI's version (ADR-0016). Decided at load time; `error` severity.
|
||||
CphVersionMismatch,
|
||||
}
|
||||
|
||||
impl DiagCode {
|
||||
@@ -103,6 +106,7 @@ impl DiagCode {
|
||||
DiagCode::SchemaViolation => "E-SCHEMA",
|
||||
DiagCode::TypstCompile => "E-TYPST-COMPILE",
|
||||
DiagCode::RenderIgnored => "W-RENDER-IGNORED",
|
||||
DiagCode::CphVersionMismatch => "E-CPH-VERSION",
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
@@ -391,6 +391,14 @@ pub fn load(root: &Path) -> (Option<Lesson>, Vec<Diagnostic>) {
|
||||
}
|
||||
};
|
||||
|
||||
// `.cph-version` compatibility (ADR-0016). Decided at load time, before
|
||||
// any structural/schema/compile work. An incompatible version is an
|
||||
// error diagnostic (`CphVersionMismatch`); it does not halt loading, so
|
||||
// any other defects surface alongside it — but an error diagnostic alone
|
||||
// already makes the lesson illegal (ADR-0010), so `check`/`build` refuse.
|
||||
// A missing `.cph-version` is skipped for now (ADR-0016 OPEN).
|
||||
check_cph_version(root, &mut diags);
|
||||
|
||||
// [project] and [info] are required to build a Lesson at all.
|
||||
let project = match raw.project {
|
||||
Some(p) => Project {
|
||||
@@ -506,6 +514,58 @@ pub fn load(root: &Path) -> (Option<Lesson>, Vec<Diagnostic>) {
|
||||
(Some(lesson), diags)
|
||||
}
|
||||
|
||||
/// The cph version the running CLI was built with (ADR-0016). Pulled from the
|
||||
/// crate's `CARGO_PKG_VERSION` at compile time.
|
||||
pub const CPH_VERSION: &str = env!("CARGO_PKG_VERSION");
|
||||
|
||||
/// Read the engineering file's `.cph-version` and, if present, push a
|
||||
/// `CphVersionMismatch` error when it is not compatible with [`CPH_VERSION`]
|
||||
/// (ADR-0016). A missing file is skipped for now (migration period; OPEN in
|
||||
/// ADR-0016).
|
||||
fn check_cph_version(root: &Path, diags: &mut Vec<Diagnostic>) {
|
||||
let path = root.join(".cph-version");
|
||||
let Ok(src) = std::fs::read_to_string(&path) else {
|
||||
return; // missing `.cph-version` — skipped (ADR-0016 OPEN).
|
||||
};
|
||||
let file_version = src.trim();
|
||||
if file_version.is_empty() {
|
||||
diags.push(
|
||||
Diagnostic::error(
|
||||
DiagCode::CphVersionMismatch,
|
||||
format!(".cph-version is empty; expected cph version {CPH_VERSION}"),
|
||||
)
|
||||
.with_hint(format!(
|
||||
"write the cph version this file targets into {} (currently {CPH_VERSION})",
|
||||
path.display()
|
||||
)),
|
||||
);
|
||||
return;
|
||||
}
|
||||
if !versions_compatible(file_version, CPH_VERSION) {
|
||||
diags.push(
|
||||
Diagnostic::error(
|
||||
DiagCode::CphVersionMismatch,
|
||||
format!(
|
||||
".cph-version declares {file_version}, but this cph is {CPH_VERSION} (incompatible)"
|
||||
),
|
||||
)
|
||||
.with_hint(format!(
|
||||
"align them: set .cph-version to {CPH_VERSION}, or install cph {file_version}"
|
||||
)),
|
||||
);
|
||||
}
|
||||
}
|
||||
|
||||
/// Whether an engineering file's declared cph version is compatible with the
|
||||
/// running CLI's version (ADR-0016). **The rule is exact equality** — the
|
||||
/// strictest choice, deliberately, while the format is young (0.0.x). This is
|
||||
/// the single seam for future relaxation to a semver range: relaxing the
|
||||
/// format does not change the diagnostic class, the spec, or the CLI — only
|
||||
/// this predicate.
|
||||
fn versions_compatible(file_version: &str, cli_version: &str) -> bool {
|
||||
file_version == cli_version
|
||||
}
|
||||
|
||||
/// Load one element's `element.toml` into an [`ElementDescriptor`], collecting
|
||||
/// diagnostics. On a missing/malformed `element.toml` the descriptor falls back
|
||||
/// to the part's declared kind with empty scalars so the lesson stays buildable.
|
||||
|
||||
@@ -0,0 +1 @@
|
||||
0.0.2
|
||||
@@ -272,3 +272,90 @@ fn malformed_target_config_is_non_fatal_with_schema_violations() {
|
||||
"a diagnostic should name the bad step type, got: {diags:?}"
|
||||
);
|
||||
}
|
||||
|
||||
// --- `.cph-version` compatibility gate (ADR-0016) ------------------------------
|
||||
|
||||
/// The cph version the running CLI was built with — what `.cph-version` must
|
||||
/// match exactly (ADR-0016's MVP rule).
|
||||
const CPH_VERSION: &str = env!("CARGO_PKG_VERSION");
|
||||
|
||||
/// Write a one-part lesson into a temp dir, optionally with a `.cph-version`
|
||||
/// file. Returns the temp dir so the caller runs `load`.
|
||||
fn tmp_lesson_with_version(version: Option<&str>) -> PathBuf {
|
||||
let mut p = std::env::temp_dir();
|
||||
let nanos = std::time::SystemTime::now()
|
||||
.duration_since(std::time::UNIX_EPOCH)
|
||||
.unwrap()
|
||||
.as_nanos();
|
||||
p.push(format!("cph-version-test-{nanos}"));
|
||||
std::fs::create_dir_all(&p).unwrap();
|
||||
std::fs::write(
|
||||
p.join("manifest.toml"),
|
||||
"[project]\nid = \"v\"\nname = \"v\"\n[info]\ntitle = \"v\"\n[[parts]]\nkind = \"segment\"\npath = \"segments/a\"\n",
|
||||
)
|
||||
.unwrap();
|
||||
let seg = p.join("segments").join("a");
|
||||
std::fs::create_dir_all(&seg).unwrap();
|
||||
std::fs::write(seg.join("element.toml"), "kind = \"segment\"\n").unwrap();
|
||||
std::fs::write(seg.join("textbook.typ"), "t.\n").unwrap();
|
||||
if let Some(v) = version {
|
||||
std::fs::write(p.join(".cph-version"), v).unwrap();
|
||||
}
|
||||
p
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn cph_version_matching_is_not_a_diagnostic() {
|
||||
let tmp = tmp_lesson_with_version(Some(CPH_VERSION));
|
||||
let (_lesson, diags) = load(&tmp);
|
||||
let _ = std::fs::remove_dir_all(&tmp);
|
||||
assert!(
|
||||
diags.iter().all(|d| d.code != DiagCode::CphVersionMismatch),
|
||||
"a matching .cph-version must not warn, got {diags:?}"
|
||||
);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn cph_version_mismatch_is_an_error_diagnostic() {
|
||||
let tmp = tmp_lesson_with_version(Some("99.99.99"));
|
||||
let (lesson, diags) = load(&tmp);
|
||||
let _ = std::fs::remove_dir_all(&tmp);
|
||||
// The lesson still loads (so other defects could surface), but the
|
||||
// mismatch is an error diagnostic — which alone makes it illegal.
|
||||
assert!(lesson.is_some(), "a mismatch should not halt loading");
|
||||
let mm: Vec<_> = diags
|
||||
.iter()
|
||||
.filter(|d| d.code == DiagCode::CphVersionMismatch)
|
||||
.collect();
|
||||
assert_eq!(mm.len(), 1, "expected one CphVersionMismatch, got {diags:?}");
|
||||
assert!(
|
||||
mm[0].message.contains("99.99.99") && mm[0].message.contains(CPH_VERSION),
|
||||
"diagnostic should name both versions, got: {}",
|
||||
mm[0].message
|
||||
);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn cph_version_missing_is_skipped() {
|
||||
// No `.cph-version` file at all → skipped (ADR-0016 migration period; OPEN).
|
||||
let tmp = tmp_lesson_with_version(None);
|
||||
let (_lesson, diags) = load(&tmp);
|
||||
let _ = std::fs::remove_dir_all(&tmp);
|
||||
assert!(
|
||||
diags.iter().all(|d| d.code != DiagCode::CphVersionMismatch),
|
||||
"a missing .cph-version must be skipped, got {diags:?}"
|
||||
);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn cph_version_empty_is_an_error() {
|
||||
let tmp = tmp_lesson_with_version(Some(" \n"));
|
||||
let (_lesson, diags) = load(&tmp);
|
||||
let _ = std::fs::remove_dir_all(&tmp);
|
||||
assert!(
|
||||
diags
|
||||
.iter()
|
||||
.any(|d| d.code == DiagCode::CphVersionMismatch && d.message.contains("empty")),
|
||||
"an empty .cph-version should be an error, got {diags:?}"
|
||||
);
|
||||
}
|
||||
|
||||
@@ -0,0 +1 @@
|
||||
0.0.2
|
||||
@@ -0,0 +1,105 @@
|
||||
# ADR 0016: The `.cph-version` Contract File
|
||||
|
||||
## Status
|
||||
|
||||
Accepted — and implemented. The cph CLI refuses to process an engineering
|
||||
file whose `.cph-version` is not compatible with the running CLI, surfacing
|
||||
this as a 7th diagnostic class `cphVersionMismatch`.
|
||||
|
||||
Builds on **ADR-0005** (the engineering file is the asset; its structure is
|
||||
declared), **ADR-0008** (the engineering file is a directory tree rooted at
|
||||
`manifest.toml`), and **ADR-0010/0012** (the diagnostic taxonomy and the
|
||||
"legal lesson = no error diagnostics" rule).
|
||||
|
||||
## Context
|
||||
|
||||
As the cph tool and the authored curriculum engineering files evolve
|
||||
independently, a file authored against one version of the format may not be
|
||||
processable by a CLI built against another. Without a version contract, a
|
||||
mismatch surfaces as confusing downstream failures (a malformed-manifest
|
||||
diagnostic, a compile error, or a silently-wrong build) rather than as the
|
||||
real cause: "this file expects a different cph than the one you're running."
|
||||
|
||||
The user's framing: the curriculum engineering-file workspace should carry a
|
||||
`.cph-version` file naming the cph version it targets; the CLI should
|
||||
**fail early** when that version is not compatible with itself. The
|
||||
compatibility rule can be refined over time, but for now it is the strictest
|
||||
possible: **exact version equality**.
|
||||
|
||||
## Decision
|
||||
|
||||
### A `.cph-version` file at the engineering-file root
|
||||
|
||||
An engineering file's root (alongside `manifest.toml`) carries a
|
||||
`.cph-version` file whose entire content is the version string the file
|
||||
targets (e.g. `0.0.2`, no trailing newline required, whitespace trimmed).
|
||||
The CLI reads its own version from `CARGO_PKG_VERSION`.
|
||||
|
||||
### Compatibility is decided at `load` time and is a diagnostic
|
||||
|
||||
The version check runs in the `load` phase (`cph-model::load`), before any
|
||||
structural/schema/compile work. An incompatible version produces a
|
||||
`cphVersionMismatch` **error** diagnostic — not a CLI-level early exit
|
||||
without a diagnostic. This keeps the failure inside the checker's normal
|
||||
diagnostic vocabulary: `cph check` reports it and exits 1 (which *is* an
|
||||
early refusal — load-phase errors halt the pipeline), and `cph build`
|
||||
refuses to run. Because it is an error diagnostic, an incompatible-version
|
||||
file is, by the contract, **not a legal lesson** (ADR-0010's "legal = no
|
||||
error diagnostics").
|
||||
|
||||
The diagnostic carries a hint pointing the user at both versions and at the
|
||||
file (`expected <cli-version>, found <file-version> in .cph-version`).
|
||||
|
||||
### The 7th diagnostic class `cphVersionMismatch`
|
||||
|
||||
The taxonomy grows from six to seven classes. `cphVersionMismatch` is
|
||||
**structural** (the loader decides it from a file read — no oracle needed),
|
||||
like `partPathMissing`/`unknownKind`; its severity is `error`. This is a
|
||||
real divergence point (the taxonomy is spec-pinned), so it lands in Lean
|
||||
(`Spec.Courseware.Check.Diagnostic.DiagKind`) and in `DiagCode`.
|
||||
|
||||
### The compatibility rule is exact equality, for now — and is replaceable
|
||||
|
||||
The current rule is: **the file's `.cph-version` must exactly equal the
|
||||
CLI's version.** This is deliberately the strictest choice — it fails
|
||||
loudly on any drift, which is the right default while the format is young
|
||||
(0.0.x). The rule is isolated in one function
|
||||
(`cph_model::versions_compatible`), so it can be relaxed later to a semver
|
||||
range (e.g. "same major" or "compatible minor") **without touching the
|
||||
diagnostic class, the spec, or the CLI** — only that one predicate changes.
|
||||
The taxonomy and the "it's a `cphVersionMismatch` error" contract are
|
||||
stable across that evolution.
|
||||
|
||||
### A missing `.cph-version` is not (yet) an error
|
||||
|
||||
If the file has no `.cph-version`, the check is skipped (no diagnostic) for
|
||||
now — existing files and the `mini`/`TH-141` fixtures predate the contract.
|
||||
Whether a missing file should itself be a `cphVersionMismatch` (or a softer
|
||||
warning) once the ecosystem migrates is left open. The KenKen lesson and
|
||||
this repo's examples carry the file as the migration's starting point.
|
||||
|
||||
## Consequences
|
||||
|
||||
- A curriculum file now declares the cph version it was authored against;
|
||||
the CLI refuses incompatible versions with a clear diagnostic rather than
|
||||
a downstream mystery.
|
||||
- The diagnostic taxonomy is seven classes (was six). The Lean master, the
|
||||
`DiagCode` enum, and the severity mapping all gain `cphVersionMismatch`.
|
||||
- The compatibility predicate is the single place future semver relaxation
|
||||
lands — a deliberate seam.
|
||||
- `cph check`/`build` against the repo's own examples requires those
|
||||
examples' `.cph-version` to match the workspace version; the release
|
||||
commit updates them together.
|
||||
|
||||
## Open Questions / Deferred
|
||||
|
||||
- **Missing-file policy.** Whether an absent `.cph-version` should become an
|
||||
error (forcing migration) or a warning — deferred until the contract is
|
||||
broadly adopted.
|
||||
- **Semver relaxation.** The exact equality rule is a placeholder; the real
|
||||
compatibility intervals (per ADR-0014-style "what's a breaking change")
|
||||
are settled when there is a real breaking change to justify loosening.
|
||||
- **Manifest vs file.** The version lives in a sibling file, not a
|
||||
`[project] cph-version = …` manifest key. This mirrors how a toolchain
|
||||
version is often a separate file (`.tool-versions`, `rust-toolchain`);
|
||||
whether it should migrate into the manifest is open.
|
||||
@@ -0,0 +1 @@
|
||||
0.0.2
|
||||
@@ -6,7 +6,7 @@ import Spec.Courseware.Open
|
||||
/-!
|
||||
# Courseware —— 产品层契约(课程工程文件)
|
||||
|
||||
护城河:课程"工程文件"的语义母本与合法性规则。决策出处 ADR-0005..0015。按四组组织:
|
||||
护城河:课程"工程文件"的语义母本与合法性规则。决策出处 ADR-0005..0016。按四组组织:
|
||||
|
||||
- **`Model`** —— 工程文件的内容模型:基元 `Primitives`、富内容 `RichContent`、原子
|
||||
单位 `Element`、单节课 `Lesson`(element 的有序序列)。
|
||||
|
||||
@@ -6,12 +6,12 @@ import Spec.Courseware.Export.Render
|
||||
|
||||
产品里"站在 Lean 位置"的 rule-based checker,语义在此沉淀(ADR-0010,经 ADR-0012
|
||||
修订)。它对 lesson 提诊断,每条有**分类**(`DiagKind`)与**严重级别**(`Severity`)。
|
||||
本模块:钉级别类型(二分);钉 6 类诊断各自的含义与级别,并把"**合法 lesson = 无
|
||||
本模块:钉级别类型(二分);钉 7 类诊断各自的含义与级别,并把"**合法 lesson = 无
|
||||
error 级诊断**"建成判定(ADR-0005 deferred 的"完整合法判定"的回填);对**模型外设施**
|
||||
型诊断(typst 编过否、数据合 schema 否)用**抽象谓词 + `Oracle` 实现边界**表示——契约
|
||||
说"存在这条诊断、什么意思、什么级别",真值由实现提供,不在 Lean 内计算(不内嵌 typst
|
||||
编译器)。引用解析(`@ref`、相对 import)不另设诊断:它们都是 typst 编译期失败,归
|
||||
`typstCompile`(ADR-0012)。
|
||||
`typstCompile`(ADR-0012)。版本契约诊断 `cphVersionMismatch`(ADR-0016)是第 7 类。
|
||||
-/
|
||||
|
||||
namespace Spec.Courseware
|
||||
@@ -22,10 +22,10 @@ inductive Severity where
|
||||
| warning
|
||||
| error
|
||||
|
||||
/-- 诊断**分类**(`PINNED` 6 类, ADR-0010,经 ADR-0012 修订为 6 类)。按"谁来判定"分
|
||||
三层:**结构型**(模型自身可判):`partPathMissing`/`unknownKind`;**schema/外部设施型**
|
||||
(靠实现 oracle):`missingContentFile`/`schemaViolation`/`typstCompile`;**语义型**:
|
||||
`renderIgnored`。 -/
|
||||
/-- 诊断**分类**(`PINNED` 7 类, ADR-0010,经 ADR-0012 修订为 6 类,经 ADR-0016 增至 7
|
||||
类)。按"谁来判定"分三层:**结构型**(模型自身可判):`partPathMissing`/`unknownKind`/
|
||||
`cphVersionMismatch`;**schema/外部设施型**(靠实现 oracle):
|
||||
`missingContentFile`/`schemaViolation`/`typstCompile`;**语义型**:`renderIgnored`。 -/
|
||||
inductive DiagKind where
|
||||
/-- manifest 的 part 指向不存在的文件夹(或经 `..` 逃出根)。结构型。 -/
|
||||
| partPathMissing
|
||||
@@ -41,17 +41,24 @@ inductive DiagKind where
|
||||
| typstCompile
|
||||
/-- 某被用到的 kind 在某声明的 target 下无渲染规则,该 element 被忽略。语义型。 -/
|
||||
| renderIgnored
|
||||
/-- 工程文件的 `.cph-version` 与 CLI(cph)版本不相容(ADR-0016)。**结构型**(加载期
|
||||
判)。工程文件根的 `.cph-version` 声明它所面向的 cph 版本;CLI 加载时按**兼容性判
|
||||
定**比对自身版本(实现侧 `CARGO_PKG_VERSION`),不相容即产此类。**当前判定为版本
|
||||
完全相等才相容**(MVP;后续可放宽为 semver 区间,判定逻辑可逐步修改而不动本分类)。
|
||||
`error` 级——版本不相容的工程文件不应被该 CLI 处理。 -/
|
||||
| cphVersionMismatch
|
||||
|
||||
/-- 每类诊断的**严重级别**(`PINNED`, ADR-0010)。五类 `error`(阻断);**唯
|
||||
/-- 每类诊断的**严重级别**(`PINNED`, ADR-0010)。六类 `error`(阻断);**唯
|
||||
`renderIgnored` 为 `warning`**——ADR-0005 种子规则"缺渲染 ⇒ warning,不阻断导出"。
|
||||
钉成全函数使"哪类阻断"成为可引用、可对齐的事实(实现侧 `DiagCode` 级别据此对齐)。 -/
|
||||
def DiagKind.severity : DiagKind → Severity
|
||||
| .partPathMissing => .error
|
||||
| .unknownKind => .error
|
||||
| .partPathMissing => .error
|
||||
| .unknownKind => .error
|
||||
| .missingContentFile => .error
|
||||
| .schemaViolation => .error
|
||||
| .typstCompile => .error
|
||||
| .renderIgnored => .warning
|
||||
| .schemaViolation => .error
|
||||
| .typstCompile => .error
|
||||
| .renderIgnored => .warning
|
||||
| .cphVersionMismatch => .error
|
||||
|
||||
/-- 缺渲染诊断的级别 = **warning**(`PINNED`, ADR-0005/0010,**非 error**)。具名常量,
|
||||
使"它是 warning"可被实现侧 grep 对齐(实现里同名常量 `RENDER_IGNORED_SEVERITY` 引用
|
||||
|
||||
@@ -14,7 +14,9 @@ namespace Spec.Courseware
|
||||
|
||||
/-- 检查管线的**阶段**(`PINNED` 5 阶段, ADR-0010)。
|
||||
|
||||
- `load` —— 解析 manifest + 各 element.toml。硬失败则**停**整条管线。
|
||||
- `load` —— 解析 manifest + 各 element.toml。**含 `.cph-version` 兼容性判定**
|
||||
(ADR-0016:工程根 `.cph-version` 与 CLI 版本不相容 ⇒ `cphVersionMismatch` error)。
|
||||
硬失败(无法解析 lesson)则**停**整条管线。
|
||||
- `structural` —— part 路径存在、无 `..`、kind 已知且一致。此处判缺的 part 后续跳过。
|
||||
- `schema` —— 每个"存在且 kind 已知"的 part 按其 kind schema 校验。
|
||||
- `compile` —— 模型外设施阶段(typst 编译)。**门控:仅当前序零 error 才跑**。
|
||||
|
||||
Reference in New Issue
Block a user