Skip to content

RoughHeatKernel v0.12.0

Latest

Choose a tag to compare

@chenle02 chenle02 released this 29 Oct 15:46
· 4 commits to main since this release

RoughHeatKernel v0.12.0 renames its comparator entry modules to package-qualified roots. Breaking for anything that imports the old module names; no definition, theorem or proof changes.

  • Renamed modules. The Lean libraries Challenge and Solution are now RoughHeatKernelChallenge and RoughHeatKernelSolution, with the files and the Challenge/Reference/... tree moved to match (Challenge.Reference.* -> RoughHeatKernelChallenge.Reference.*). comparator.json names the new modules. Theorem names, which live in the RoughHeatKernel namespace, are unchanged, and in the .lean sources only import and module lines changed.
  • Why. A top-level Challenge or Solution module in a dependency shadows the same root of any downstream package: Palomar's full preflight refuses such a package with challenge.module_root_shadowed (it resolves the dependency's Challenge.lean instead of the submitted statement file). Package-qualified roots, as lean-pkg new scaffolds them, remove the collision for every package that depends on RoughHeatKernel. lean-pkg palomar check detects the case since lean-pkg #405 (0.24.0, unreleased).
  • Verification. Fresh receipts at the rename commit 16946e1: the lower-tier systemd receipt (verification gate PASS, no sorry, standard axioms only, claim axioms 56/56) and the comparator receipt (mechanism toolchain, result pass), both in .lean-receipts/; the package is re-gated in the lab registry.
  • Upgrading. Replace imports of Challenge/Solution (and Challenge.Reference.*) from this library with the new names. Packages that only import RoughHeatKernel need no change.