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>
22 lines
1019 B
Lean4
22 lines
1019 B
Lean4
import Spec.Courseware.Model
|
|
import Spec.Courseware.Export
|
|
import Spec.Courseware.Check
|
|
import Spec.Courseware.Open
|
|
|
|
/-!
|
|
# Courseware —— 产品层契约(课程工程文件)
|
|
|
|
护城河:课程"工程文件"的语义母本与合法性规则。决策出处 ADR-0005..0016。按四组组织:
|
|
|
|
- **`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`。
|
|
-/
|