Upgrading to 0.11.0 (from 0.10.0)
The behaviour changes of 0.11.0 that a package author has to know, one per
entry of the machine-readable record 0.11.0.yaml. The
mechanical part (formats, commands, flags, keys, aliases) is printed by
lean-pkg doctor --upgrade-from 0.10.0; see the
design. The record was completed after
0.11.0 was cut; doctor --upgrade-from 0.10.0 --to 0.11.0 reads it from the
checkout’s newer HEAD.
Act before you re-gate or publish
| Entry | PR | What changed | What to do |
|---|---|---|---|
receipt-sealed-log-required |
#202 | A lower-tier receipt whose sealed verify log is missing or unreadable is refused everywhere (gate, the claims ledger, promote, publish, next, comparator, palomar prepare, index); it used to pass with “report_sha256 not checked”. | Commit each receipt’s sealed log byte-exact (Restoring preserved evidence), or run and gate a new receipt. |
slurm-claim-needs-sacct-seal |
#202 | A comparator receipt’s Slurm claim no longer backs a coverage.yaml compute job (and the Easley sentence) unless sealed with comparator-receipt --seal-sacct. |
Seal where sacct sees the job, commit the receipt and the record, re-record with lean-pkg comparator NAME --receipt R --replace. |
page-for-mathematicians |
#205 | The README verification section is rewritten (statements first, receipts last), so every published page is stale. | lean-pkg page NAME --write (and --site/--html) once; commit. |
comparator-host-label |
#208 | Comparator receipts name the host by its label (h- + 12 hex); public-safety blocks a committed receipt whose host names its host (receipt-raw-host). |
Regenerate such a receipt, or add an allow: line if the name is public on purpose (Host policy). |
receipt-producer-fingerprint |
#207 | receipt systemd --run refuses, writing nothing, when the running lean-pkg changed during the run. |
Do not pull the checkout a long run uses; freeze the producer (receipts). |
bare-lean-pkg-newcomer-page |
#201 | lean-pkg with no command prints the newcomer page off a terminal or without a registry (it printed the board). |
Run lean-pkg registry board where a script wanted the board text. |
new-kind-paper-default |
#215 | lean-pkg new NAME scaffolds a paper companion by default (an incomplete coverage.yaml of kind: paper); --kind library is the previous scaffold. |
Add --kind library where a script scaffolds a library. |
Nothing required
| Entry | PR | What changed |
|---|---|---|
command-tree-stage-1 |
#201 | New canonical spellings (lease ..., registry ..., repo move, comparator attach, formalization render; --doi-track, --receipt-commit, --url, --repo, --target-repo). Old spellings are permanent aliases with one stderr note in text mode (LEAN_PKG_NO_ALIAS_NOTE=1 silences it); a flag of another comparator/formalization form is a usage error. |
seal-sacct-node-label |
#210 | --seal-sacct compares the node’s host label again; a mismatch refuses. |
coverage-paper-statement |
#211 | coverage/1 gains optional paper.statement / statement; once a file uses it, every reader needs 0.11.0. |
receipt-check-formalization-exemption |
#213 | receipt check applies gate’s derived-keys-only exemption to formalization.yaml (a tag on an evidence commit that refreshed it passes) and skips the comparator runner’s own records. |
mathlib-rev-none-checked |
#215 | mathlib_rev: none is checked against lake-manifest.json; older receipts are still read. |
formalization-kept-view |
#216 | lean-pkg formalization kept: the kept view of formalization.yaml and its SHA-256, for a release-input audit. |
extract-adopted-licenses |
#218 | lean-pkg-extract plan warns when an adopted file’s upstream license is not carried into the target (manifest key adopted). |
Read for this record and needing nothing from a package author: #200, #203, #204, #206, #209, #212, #214, #217 (documentation, the tutorial, proposals and decision records).