Restore automatic proof-profile comments on every PR

[Vilin97]

PR #670 never received a proof profile because #630 removed the automatic PR trigger. Restore profiling on opening, pushes, reopening, and marking ready, including drafts, while keeping /profile and manual dispatch available. Subsequent runs update the existing comment.

Every PR now gets a report: PRs without added or modified Lean files receive an explicit no-files comment, and renamed Lean files are measured as added files. Fork PRs retain the read-only measurement and artifact-based posting path. Update the contributor documentation and regression coverage, including the former opt-in-only expectation.

Validation: actionlint, Ruff checks and formatting pass. The full Python suite passes: 831 passed, 2 skipped, with a macOS CPU-count equivalent supplied for the Linux-only nproc command. Regression tests cover trigger admission/concurrency, no-files report generation, fork delivery, and actual Git rename selection.

Live validation: this PR automatically received its no-files profile comment, and its Proof Profile workflow completed successfully.

Backfill for #670 completed successfully and posted its profile comment: https://github.com/LeanPool/lean-pool/actions/runs/39210404159.

[github-actions]

Proof profile (new / modified Lean files)

No added or modified Lean files under LeanPool/ in this PR. No compile-cost measurements are needed.

Advisory only — never blocks merge.

[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] This PR appears safe to merge; no actionable issue caused by these changes was found.

Summary

Restores automatic proof profiles when PRs open, receive pushes, reopen, or become ready for review, including drafts.

• Every PR update starts or refreshes a proof-profile comment.
• PRs without Lean changes still get a proof-profile report.
• Renamed Lean files are counted as additions for profiling.

Review was based on code inspection; tests and live GitHub workflows were not run.

_{Reviews (1) · Last reviewed commit: "Restore automatic proof-profile comments..." · Reviewed by Greptile}

[Vilin97]

Review of 3c8d2179d999d0f3ce3df64df9b3dcf7df5c9824.

The five-file change is coherent: automatic PR events and concurrency agree, drafts remain eligible, the no-files branch emits a report without measurements, and --no-renames profiles a renamed Lean file as an addition. Profiling remains advisory. I executed all four new test functions from this head in an isolated fixture; trigger wiring, the no-files shell branch, fork-routing predicates, and real Git rename selection passed. This was not a rerun of the full Python suite.

One existing publisher issue deserves follow-up: the privileged companion takes its target PR from the producer artifact and checks only that it contains digits. It does not bind that target to the triggering run's PR/repository/head, so a forged artifact can direct a bot profile comment to another PR. The producer's read-only token does not authenticate data consumed by the later write-capable workflow_run. This gap predates this PR; I am not reporting it as a newly introduced regression. Recommend authenticating the target through GitHub run/PR metadata and testing rejection of a mismatched target alongside a valid fork payload. The current fork test checks routing conditions, not this association.

Technical review is favorable within that scope. Merge remains pending the separate workflow-change authorization required by the current repository assignment and CONTRIBUTING rule, plus normal required checks and protected queue validation. No waiver or additional profiling benchmark is requested.

[Vilin97]

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

Reviewed head: 3c8d2179d999d0f3ce3df64df9b3dcf7df5c9824

Verdict: ✅ approve

This restores automatic proof-profile runs, adds explicit no-files comments, profiles renamed Lean files as additions, and updates documentation and regression coverage. No Lean proofs or measurement helpers change. Five targeted regression checks passed when invoked directly; the full Python suite and live GitHub Actions runs were not repeated.

Aspect	Value
Scope	profiling workflow restoration
Introduces tech debt	✅ no
Maintainability	✅ improved
Brittleness	➖ unchanged
Risk	✅ low

The changes improve profiling coverage and make empty reports explicit without introducing actionable maintenance debt.

---

Tokens: 403,466 in / 5,269 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $1.6929 (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.