feat(checker): align cph-typst + cph-check to export-as-build model (WU-D)

Integrate the WU-B (structured targets) and WU-C (numbly, config) changes.

cph-typst:
- World resolves any @preview/* package from the in-repo vendored dir
  (<render_dir>/vendor/typst-packages/preview/<name>/<version>/), fully offline —
  no typst-kit download. Proven: build_pdf_with_real_render compiles the real
  render package (which imports @preview/numbly:0.1.0) through the embedded
  engine, PDF out.
- Driver threads each target's presentation config: looks up the TargetConfig by
  name, emits `config: (numbering: (heading: (...)))` (escaped) when an override
  is present, else `config: (:)` (render default).
- target_precheck guards artifact/target: FileTree → blocking diagnostic (MVP is
  single-file, deferred per ADR-0009); --target not declared → blocking
  diagnostic; no-targets lesson still defaults through.

cph-check:
- Migrated to Lesson.targets: Vec<TargetConfig> (target_names() / target.name at
  the 6 sites). Pipeline unchanged (already matches ADR-0010 phases). Documented
  that !has_errors() implements Spec.Courseware.Legal (no error-level diagnostic).

Workspace: fmt + clippy -D warnings + all tests green.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This commit is contained in:
2026-06-22 08:47:13 +08:00
parent 6f46aa708a
commit bd1699a4c0
6 changed files with 193 additions and 11 deletions
+12 -5
View File
@@ -60,6 +60,13 @@ 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`):
/// 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
/// here so a reviewer can tie the orchestrator's gate to the Lean master.
pub fn has_errors(&self) -> bool {
self.diagnostics
.iter()
@@ -247,7 +254,7 @@ fn compile_targets(lesson: &cph_model::Lesson) -> Vec<&str> {
if lesson.targets.is_empty() {
vec![DEFAULT_TARGET]
} else {
lesson.targets.iter().map(String::as_str).collect()
lesson.target_names()
}
}
@@ -271,11 +278,11 @@ fn render_coverage(lesson: &cph_model::Lesson, known: &[&str]) -> Vec<Diagnostic
continue;
}
for target in &lesson.targets {
let covered = COVERED_TARGETS.contains(&target.as_str());
let covered = COVERED_TARGETS.contains(&target.name.as_str());
if covered {
continue;
}
let key = (part.kind.clone(), target.clone());
let key = (part.kind.clone(), target.name.clone());
if seen.contains(&key) {
continue;
}
@@ -284,12 +291,12 @@ fn render_coverage(lesson: &cph_model::Lesson, known: &[&str]) -> Vec<Diagnostic
DiagCode::RenderIgnored,
format!(
"kind '{}' has no render rule for target '{}'; it will be omitted from that export",
part.kind, target
part.kind, target.name
),
)
.with_hint(format!(
"add a render rule for kind '{}' under target '{}', or remove the target",
part.kind, target
part.kind, target.name
));
// Pin the severity via the named contract const. `Diagnostic::warning`
// already produces a warning, but assigning the const keeps the