forked from bai/curriculum-project-hub
sjfhsjfh
3ebe4b754d
Remove filler/redundant patterns: 钉死/钉, 本模块, likec4 画不出/画得出, 臆造, 散文, 分歧点测试, 纯 plumbing, 恰好, 留白, 宪法第N条, 刻意. No code definitions changed, only doc comments.
108 lines
6.2 KiB
Lean4
108 lines
6.2 KiB
Lean4
import Spec.Courseware.Model.Lesson
|
|
import Spec.Courseware.Export.Render
|
|
|
|
/-!
|
|
# Diagnostic —— checker 诊断:分类、严重级别、合法 lesson
|
|
|
|
产品里"站在 Lean 位置"的 rule-based checker,语义在此沉淀(ADR-0010,经 ADR-0012
|
|
修订)。它对 lesson 提诊断,每条有**分类**(`DiagKind`)与**严重级别**(`Severity`)。
|
|
定级别类型(二分);定 7 类诊断各自的含义与级别,并把"**合法 lesson = 无
|
|
error 级诊断**"建成判定(ADR-0005 deferred 的"完整合法判定"的回填);对**模型外设施**
|
|
型诊断(typst 编过否、数据合 schema 否)用**抽象谓词 + `Oracle` 实现边界**表示——契约
|
|
说"存在这条诊断、什么意思、什么级别",真值由实现提供,不在 Lean 内计算(不内嵌 typst
|
|
编译器)。引用解析(`@ref`、相对 import)不另设诊断:它们都是 typst 编译期失败,归
|
|
`typstCompile`(ADR-0012)。版本契约诊断 `cphVersionMismatch`(ADR-0016)是第 7 类。
|
|
-/
|
|
|
|
namespace Spec.Courseware
|
|
|
|
/-- 诊断严重级别(`PINNED` 二分, ADR-0005)。`error` 阻断(产物不合法),`warning` 不
|
|
阻断(产物仍可导出,只是有损)。更细级别(info/hint)未决策,故只二分。 -/
|
|
inductive Severity where
|
|
| warning
|
|
| error
|
|
|
|
/-- 诊断**分类**(`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
|
|
/-- 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
|
|
/-- 工程文件的 `.cph-version` 与 CLI(cph)版本不相容(ADR-0016)。**结构型**(加载期
|
|
判)。工程文件根的 `.cph-version` 声明它所面向的 cph 版本;CLI 加载时按**兼容性判
|
|
定**比对自身版本(实现侧 `CARGO_PKG_VERSION`),不相容即产此类。**当前判定为版本
|
|
完全相等才相容**(MVP;后续可放宽为 semver 区间,判定逻辑可逐步修改而不动本分类)。
|
|
`error` 级——版本不相容的工程文件不应被该 CLI 处理。 -/
|
|
| cphVersionMismatch
|
|
|
|
/-- 每类诊断的**严重级别**(`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
|
|
| .cphVersionMismatch => .error
|
|
|
|
/-- 缺渲染诊断的级别 = **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
|