Add weekly Azure source profiling and an explorer badge

[Vilin97]

Add a weekly Azure VM job that captures every LeanPool source module with lean-source-profiler, audits the pinned recording, and publishes the complete snapshot to https://vilin97.github.io/lean-source-profiler/pool/. The README links to the explorer and adds a badge showing the latest completed recording date.

The Monday 02:00 UTC systemd job has no runtime timeout, checkpoints completed files, resumes after reboot, retries failures, and preserves the previous public recording until the full build/capture/coverage audit passes. Storage stays on /data; publishing preserves concurrent viewer edits.

Validation: six runner regression tests, including a real Git push race and failed-capture recovery; Ruff checks/formatting; systemd unit validation. The profiler changes are deployed separately, with 65 unit tests and a native Lean build/capture/audit/export/resume integration test passing. The VM timer is installed and a fresh recording has been started.

[greptile-apps]

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

[High impact] Adds weekly profiling job with Azure VM infrastructure setup.

The saved-run disk check still needs repair before merging.

Findings

1.  Space check blocks saved runs ▶

Summary

Adds a weekly Azure profiling job and links its public explorer from the README.

• An Azure job profiles LeanPool every Monday and publishes audited results.
• The README links readers to the source explorer and latest recording date.

_{Reviews (3) · Last reviewed commit: "fix: recover interrupted weekly profilin..." · Reviewed by Greptile}

[Vilin97]

🤖 LLM review — refactor (gpt-6.1-sol)

Reviewed head: 79665335cf0e9a202cc51d897b3ef0307c2a9508

Verdict: 🛑 request_changes

This adds weekly profiling infrastructure and an explorer badge without modifying Lean proofs. The six runner tests and Ruff checks pass, but targeted experiments reproduced three recovery defects: interrupted clones permanently block retries, the disk reserve blocks saved publication stages, and interrupted completion bookkeeping bypasses retention. These create recurring operator work and should be fixed before merging. Whole-pool capture was not exercised, and systemd validation could not run in this sandbox.

Aspect	Value
Scope	profiling infrastructure
Introduces tech debt	🛑 yes
Maintainability	🛑 regressed
Brittleness	🛑 more_brittle
Risk	🟡 medium

The runner needs recoverable checkout setup, phase-aware disk checks, and idempotent completion bookkeeping before its unattended operation is maintainable.

Findings (3)

• interrupted-checkout — scripts/weekly-profile/run.py:55
  Any existing destination is treated as a completed clone. Killing a real clone during fetch left a directory without HEAD; both subsequent retries failed at git diff --exit-code HEAD without recloning. A reboot during initial setup therefore blocks every later recording until manual repair. Clone into a staging directory and rename after success, or recreate incomplete checkouts before pinning a run.
• resume-space-check — scripts/weekly-profile/run.py:235
  The unconditional 30 GiB check runs before loading the saved phase. If a recording consumes that reserve and restarts after export, every publication retry fails; retention cleanup cannot help because it runs only after publication. A saved publish checkpoint with simulated 29 GiB free reproduced this blockage. Separate the fresh-run reserve from phase-appropriate checks for resuming completed work.
• completion-checkpoint — scripts/weekly-profile/run.py:209
  The active checkpoint becomes complete before the per-run completion record is written. Injecting a failure at that second write caused the next invocation to start a new recording, while the published recording lacked the marker required by pruning and remained indefinitely. The pending marker also remained. Write the per-run completion record before marking the active checkpoint complete, and make finalization and cleanup recoverable on restart.

---

Tokens: 849,417 in / 8,755 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $3.5290 (Standard API equivalent; uncached input) (long-context rate)
Automated review against .github/REFACTOR_REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.
request_changes is an ask, not a close: of the reviewer's past request_changes verdicts, 39% were merged after a human looked. Read the findings before acting on the verdict.

[Vilin97]

Reviewed commit 10b9e6780fe58343b7d5e83d0448e1319bd2d90d.

I found and fixed an interruption window in finalization: the runner could clear its pending state before writing complete.json, leaving a published run outside completed-run retention. The fix writes the completion marker first. Two regression cases interrupt immediately before and after that write, then verify that resuming finishes the same run without repeating capture/export and still retains the two newest completed runs.

All eight runner tests pass locally; the two new cases fail against the original runner at the expected phase assertion. Ruff and formatting checks pass. I also reviewed the referenced profiler's capture/export source contract; this review does not claim a completed production profiling run.

The code review is clear after this small fix. Merge remains pending successful CI on this exact commit, including the pool build.

[Vilin97]

Reviewed commit 26a3070. The recovery paths now handle interrupted clones, preserve the completion marker before cleanup, and resume a saved publish phase when free space is below 30 GiB. Preparation, capture, and export still enforce the 30 GiB guard.

Validation: all 26 weekly-profile tests pass; Ruff check and format check pass. The two new regression cases fail as expected against the original runner. Both committed files match the reviewed and tested postimages.

The outdated disk-space advisory is addressed by the phase-aware guard. Head CI is green, including the full pool build. The existing protected auto-merge request is retained. I have not run a complete production profiling cycle.