[SamuelSchlesinger]

Cache bootstrap completion previously looked like a cache hit, origin attempts had no timed result, and the serial restored-source audit could remain silent on a long file. Report each origin's completed/failed/timed-out result and elapsed time; show bootstrap attempt start, finish and reuse without treating the attempt stamp or a zero optional-fetch exit as proof of a hit. Missing-only lookup failure now includes the final HTTP/curl status instead of claiming that no uploaded outputs exist.

The serial audit reports its selected count, current source before elaboration and elapsed audit time locally. --quiet suppresses progress; CI is quiet by default and --progress overrides it. Failures and the final count/time summary remain visible in every mode. Selected sources, warning/output failures, cancellation, exit codes, origin order and deadlines are unchanged. The existing Remote cache: <revision> line remains compatible with the handoff measurement parser.

Part of #4972, owned by Codex worker /root/cache_fallback_change on perf/cache-validation-progress. This PR supplies observability; it does not establish a performance improvement or complete the staging/rotation profiling lanes.

Manual impact

Updated the Operator's Manual troubleshooting procedure and linked cache guide for the new output and progress controls. The Agent Operator's Manual needs no edit: assignment, authorization, ownership, review and handoffs are unchanged. No Lean examples changed; hosted rendered-page review remains pending.

Validation

• Audit fixtures: 18 tests passed, including progress before elaboration, CI/quiet controls, warning retention and cancellation without advancing to another file. Quick-check caller fixtures: 49 passed; full-check parity: 16 passed.
• Cache mirrors: 21 tests passed with 6 platform-specific skips; bootstrap: 15 passed. Existing timeout, partial-download, strict-build failure and unsafe-shutdown cases remain covered.
• Handoff measurement/parser tests: 24 passed with TMPDIR=/private/tmp (the default macOS temporary-path alias trips an existing unrelated fixture comparison).
• Manual tooling: 72 tests passed; source/link checker, shell syntax and git diff --check passed.
• No library Lean build or native Lean fixture was run locally; hosted CI supplies integration coverage.

AI assistance

Codex implemented and checked the change; independent exact-head review is requested before integration.

[SamuelSchlesinger]

Independent agent review by Codex /root/cache_ci_status at 928cda49768bd5f5d5e20947ed6b861b5338d3fb: approved; no blocking findings. Checked bootstrap exit/cancellation handling, per-origin timing and HTTP-status output, serial audit selection/failure behavior, and the quiet/progress overrides through the quick/full-check callers. The successful Remote cache: <revision> line used by the handoff parser is unchanged. Completion is correctly distinguished from a new download or cache hit.

Independently ran the audit/bootstrap suites (36 tests) and mirror/handoff-measurement suites (45 tests, 6 platform skips), plus manual source/link, shell syntax and diff checks. The Operator’s Manual explains the progress controls accurately; the Agent Operator’s Manual needs no edit because roles and handoffs are unchanged. This improves visibility and does not establish a speedup.

Rendered review passed for the changed troubleshooting paragraph (PDF page 96 / printed page 88) in manual artifact 14012212846. Both manifests identify this exact clean revision; PDF and chapter hashes match the downloaded PDFs and source. The added text and commands are readable without clipping or overlap.

All review holds are resolved. Hosted PR-head CI passed; final advisory notices identify no changed library definitions, theorems or proof blocks to review. The actual reader log loaded GCS’s mapping for 3eaf13933279… covering 9,160 modules, with none missing in .lake, and reported native-request completion in 3.7 seconds. That confirms the new reporting behavior; it does not imply a fresh artifact transfer or a measured speedup. This is agent review, not human approval.

Queueing this unchanged reviewed head. Non-author coordinator /root/cache_ci_status owns monitoring through landing and any actionable ejection. #4972 retains the separate staging/profiling objectives.