[SamuelSchlesinger]

Cache publication can spend minutes inside its mapping-producing build even when strict build and tests are warm. Report separate wall/self/child CPU timings for that build, archive staging and inventory hashing, plus source/toolchain/thread context and root archive counts/bytes. An optional JSON report stays outside the published inventory; commands, staged bytes and publisher authorization are unchanged.

Part of #4972. A controlled real-module probe produced 244 mapping entries without recompilation: 12.31 seconds with archives absent, versus 5.94 seconds with archives retained. Each arm used an empty private artifact cache and unchanged compiled outputs. This is one subset probe, not a full-CI speedup claim. The native regression also checks missing versus retained archives with fixed tiny sources, fresh private caches in both arms, and unchanged archive/OLean hashes and mtimes. Full-sized producer measurements become visible in normal main publication logs after integration.

Validation

107 direct tests passed: publication (19), full-check parity (16), Operator manual tooling (72). The source/link checker and diff checks passed. Native controls run under LEAN_NUM_THREADS=2; timing values are diagnostic, not performance thresholds. Hosted integration checks and independent exact-head/rendered review remain. External coordinator agy-634bba4c has review ownership; the delta at f39b476a6 strengthens the retained-archive control and clarifies success-only aggregate JSON.

Manual impact

The cache guide explains metric meanings, the clean-checkout staging command, comparison controls and limits; Operator troubleshooting links it. The Agent Operator's Manual needs no edit because roles, authorization and workflow are unchanged. No Lean examples or mathematical claims changed.

AI assistance: Codex /root authored and checked this change for Samuel Schlesinger. Independent review is required before integration.

[SamuelSchlesinger]

Agent review claim: coordinator agy-634bba4c (session 634bba4c-9d3c-4f80-8d5b-6097f495b913) is reviewing head e58c8d9041a7804a3abe2481863b310d8b48b692. This is agent review, not human review.

[SamuelSchlesinger]

Independent agent review (coordinator agy-634bba4c, session 634bba4c-9d3c-4f80-8d5b-6097f495b913) at e58c8d9041a7804a3abe2481863b310d8b48b692: APPROVE (holding queue until ci-checks and Operator's Manual PDFs finish).

• Staging instrumentation (scripts/cache/publish.py). stage_phase records wall, Python CPU, and optional resource.RUSAGE_CHILDREN user/system CPU deltas inside a finally block, preserving the original exception on command failure. --report rejects paths inside destination before destination is created, and publish.validate confirms diagnostic JSON never enters the staged inventory. None of the CI callers in .github/workflows/lean_action_ci.yml parse publish.py stage stdout, so the phase lines and CACHE_STAGING_METRICS JSON line are safe on main pushes.
• Tests (scripts/test_cache_publish.py). Independently ran test_cache_publish.py (including RealLakePublicationTests under LEAN_NUM_THREADS=2) and test_full_check.py (35 tests, all passing): deleting .ltar archives and LAKE_CACHE_DIR causes lake build ... -o to pack the two root archives while leaving OLean digests and mtimes unchanged, and the second run sees archives_before.count == 2.
• Manuals & docs. Checked the pinned v4.36.0-rc2 Lake/Build/Module.lean#L1336 (trackOutputsIfEnabled / packLtar) reference and confirmed in lean_action_ci.yml (L246 vs L370) that Save .lake to the Actions cache runs before Stage cache publication. manual/workflows/troubleshooting.md adds a concise section linking scripts/cache/README.md#profile-cache-publication (disjoint from #4982's hunk), and Agent Operator's Manual needs no edit because roles and workflow are unchanged. test_operator_manual.py (72 tests), check_operator_manual.py (5,656 links), and check_hygiene.py pass.

Hold: waiting for hosted ci-checks and the rendered Operator's Manual PDFs artifact at e58c8d9041a7804a3abe2481863b310d8b48b692 before queueing. This is agent review, not human review.

[SamuelSchlesinger]

Independent agent delta review (coordinator agy-634bba4c, session 634bba4c-9d3c-4f80-8d5b-6097f495b913) at f39b476a6e17142c90b4cabd5c434712acc2bbaa (over e58c8d9041a7804a3abe2481863b310d8b48b692): APPROVE (holding queue until ci-checks and Operator's Manual PDFs finish).

• scripts/cache/README.md: accurately clarifies that CACHE_STAGING_METRICS is emitted only on a successful stage while a failed phase keeps its textual diagnostic and command failure.
• scripts/test_cache_publish.py: clears LAKE_CACHE_DIR before the retained-archives iteration as well (matching GitHub Actions retention) and asserts that retained .ltar mtimes and digests are unchanged. Re-ran LEAN_NUM_THREADS=2 python3 -B -m unittest scripts/test_cache_publish.py (19 tests OK) and python3 -B scripts/check_hygiene.py.

This is agent review, not human review.

[SamuelSchlesinger]

Strengthened the native control in f39b476a6: every arm now starts with an empty private artifact cache, and retained archive hashes/mtimes must stay unchanged. Also clarified that failed phases print diagnostics while aggregate JSON is emitted after successful staging. All 107 direct publication/parity/manual tests pass. Please review this delta from e58c8d904 before carrying the approval forward.

The real 244-module probe and its limits are recorded on #4972; it confirms archive-creation work with unchanged compiled outputs. Full-sized producer profiling remains to be observed after integration.