publish-lkg.yml states that chaining publication off warm-mathlib-cache "is what enforces the contract that lkg/latest.json never advertises a SHA whose cache is cold", and docs/internal/cache-warming.md repeats it. That contract does not currently hold, for two independent reasons.
Downstreams not opted into warming are published anyway. warm_cache defaults to False (scripts/models.py:66) and plan_cache_warm_jobs.py:107 skips any downstream where it is unset, so their LKG SHAs never enter the warming matrix. Their entries are still published and still consumed by bump-to-latest through fetch-latest.sh. TauCeti is in this category: its ci/inventory/downstreams.json entry is enabled: true with no warm_cache key. The published contract covers it; the warming pass does not.
Failed warming attempts are recorded as warmth. cache_warmth is (upstream, sha, warmed_at) with no status column (scripts/storage.py:634), and record_warm_shas.py:26 writes every terminal status into it, including build_failed, push_failed and verify_failed. Membership means "do not plan this SHA again", not "this SHA is warm". warm-mathlib-cache.yml:269 fails finalize only on no_result, so a SHA that failed to warm is recorded, does not fail the workflow, is published by the downstream publish-lkg run, and is never retried even though push_failed and verify_failed look transient.
As evidence of the first: TauCeti pinned c0032752b47af314b015a7b411123fa4ac99bbaf, an intermediate commit of a bors batch whose master-push build never ran. lake exe cache get found 6158 of the 8681 artifacts that tree needs, missed 2523, exited 0, and left the build to recompile 1415 modules; CI went from 27 to 86-90 minutes per run until the pin moved to the batch's built tip in TauCetiProject/TauCeti#2230. Four of TauCeti's last fifteen pins were commits with no master-push build, so selection lands on one with some regularity.
On shape, I do not think LKG should be redefined as "latest compatible and warm". That conflates compatibility with artifact availability, it would break the adjacency invariant aggregate_results.py:453 enforces between LKG and FKB, and it is circular, since the planner warms the SHA that selection chose. A separate published field, say recommended_bump_commit, would let bump-to-latest consume a warm-verified commit while last_known_good_commit keeps meaning the compatibility boundary.
That suggests:
- Give
cache_warmth an explicit status so "verified warm" and "stop retrying" are separable. This needs a migration plan, since existing rows cannot be classified under the current schema.
- Retry
push_failed and verify_failed with backoff rather than suppressing them permanently.
- Gate the published bump target on verified warmth, and either warm every enabled downstream or narrow the documented contract to opted-in ones.
Two things worth deciding separately: whether the guarantee is meant to cover FKB and release targets as well as LKG, and what warming every enabled downstream would cost.
On probing warmth cheaply, the most direct signal I found is whether mathlib's build.yml ran on the commit via push to master, since it gates publish_cache on event_name == 'push' && ref == 'refs/heads/master'. That is the run which populates the mathlib4-master container. A durable cache-ready marker written by the upload job would be more robust than any downstream inferring it, and probing the cache directly more authoritative still.
Happy to send a PR for any of this if you have a preference on the shape.
🤖 Prepared with Claude Code
publish-lkg.ymlstates that chaining publication offwarm-mathlib-cache"is what enforces the contract that lkg/latest.json never advertises a SHA whose cache is cold", anddocs/internal/cache-warming.mdrepeats it. That contract does not currently hold, for two independent reasons.Downstreams not opted into warming are published anyway.
warm_cachedefaults toFalse(scripts/models.py:66) andplan_cache_warm_jobs.py:107skips any downstream where it is unset, so their LKG SHAs never enter the warming matrix. Their entries are still published and still consumed bybump-to-latestthroughfetch-latest.sh. TauCeti is in this category: itsci/inventory/downstreams.jsonentry isenabled: truewith nowarm_cachekey. The published contract covers it; the warming pass does not.Failed warming attempts are recorded as warmth.
cache_warmthis(upstream, sha, warmed_at)with no status column (scripts/storage.py:634), andrecord_warm_shas.py:26writes every terminal status into it, includingbuild_failed,push_failedandverify_failed. Membership means "do not plan this SHA again", not "this SHA is warm".warm-mathlib-cache.yml:269failsfinalizeonly onno_result, so a SHA that failed to warm is recorded, does not fail the workflow, is published by the downstreampublish-lkgrun, and is never retried even thoughpush_failedandverify_failedlook transient.As evidence of the first: TauCeti pinned
c0032752b47af314b015a7b411123fa4ac99bbaf, an intermediate commit of a bors batch whose master-push build never ran.lake exe cache getfound 6158 of the 8681 artifacts that tree needs, missed 2523, exited 0, and left the build to recompile 1415 modules; CI went from 27 to 86-90 minutes per run until the pin moved to the batch's built tip in TauCetiProject/TauCeti#2230. Four of TauCeti's last fifteen pins were commits with no master-push build, so selection lands on one with some regularity.On shape, I do not think LKG should be redefined as "latest compatible and warm". That conflates compatibility with artifact availability, it would break the adjacency invariant
aggregate_results.py:453enforces between LKG and FKB, and it is circular, since the planner warms the SHA that selection chose. A separate published field, sayrecommended_bump_commit, would letbump-to-latestconsume a warm-verified commit whilelast_known_good_commitkeeps meaning the compatibility boundary.That suggests:
cache_warmthan explicit status so "verified warm" and "stop retrying" are separable. This needs a migration plan, since existing rows cannot be classified under the current schema.push_failedandverify_failedwith backoff rather than suppressing them permanently.Two things worth deciding separately: whether the guarantee is meant to cover FKB and release targets as well as LKG, and what warming every enabled downstream would cost.
On probing warmth cheaply, the most direct signal I found is whether mathlib's
build.ymlran on the commit via push tomaster, since it gatespublish_cacheonevent_name == 'push' && ref == 'refs/heads/master'. That is the run which populates themathlib4-mastercontainer. A durablecache-readymarker written by the upload job would be more robust than any downstream inferring it, and probing the cache directly more authoritative still.Happy to send a PR for any of this if you have a preference on the shape.
🤖 Prepared with Claude Code