forked from EduCraft/curriculum-project-hub
sjfhsjfh
ebcb3a7589
教研工程文件根放 .cph-version(内容=面向的 cph 版本)。cph 加载时比对自身版本
(CARGO_PKG_VERSION),不相容报 CphVersionMismatch error 并拒绝。当前判定为版本完全
相等(MVP);判定逻辑孤立在 versions_compatible 单谓词,后续可放宽为 semver 区间而
不动诊断分类/spec/CLI。
spec(7 类诊断,原 6 类):
- Diagnostic.lean: DiagKind 增 cphVersionMismatch(error 级),分类注释 6→7
- Pipeline.lean: load 阶段含 .cph-version 兼容性判定
- Courseware.lean: ADR 区间 →0016
实现:
- cph-diag: DiagCode::CphVersionMismatch("E-CPH-VERSION")
- cph-model: load() 解析 manifest 成功后 check_cph_version;versions_compatible
谓词(完全相等);CPH_VERSION const。missing .cph-version 暂跳过(迁移期 OPEN);
空文件报 error
- examples/TH-141、valid/mini fixture、KenKen 课各加 .cph-version=0.0.2
测试:cph-model 4 个版本门测试;全 workspace 53 passed;lake 25 jobs 绿。
负向验证:9.9.9 .cph-version → E-CPH-VERSION error + check 拒绝(exit 1)。
bump: workspace.package 0.0.1→0.0.2;cph --version 报 cph 0.0.2;README 同步
(含版本契约说明)。
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
106 lines
5.2 KiB
Markdown
106 lines
5.2 KiB
Markdown
# 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.
|