Restore automatic proof-profile comments on every PR

.github/workflows/proof-profile.yml

@@ -1,7 +1,8 @@
 name: Proof Profile
 
-# Profile on demand when the PR author or anyone with write access comments
-# `/profile`, or through workflow_dispatch with an explicit PR number.
+# Keep a sticky profile comment on every PR, including drafts, and refresh it
+# after pushes or reopening. The PR author or anyone with write access can
+# also comment `/profile`; workflow_dispatch takes an explicit PR number.
 #
 # Added files get an absolute profile (`lean --profile` + heartbeat counts).
 # Modified files instead get a base→head compile-cost comparison: heartbeats
@@ -43,6 +44,8 @@ name: Proof Profile
 # also take from the default branch).
 
 on:
+  pull_request:
+    types: [opened, synchronize, reopened, ready_for_review]
   issue_comment:
     types: [created]
   workflow_dispatch:
@@ -68,6 +71,7 @@ concurrency:
   group: >-
     ${{
       (github.event_name == 'workflow_dispatch' ||
+       github.event_name == 'pull_request' ||
        (github.event_name == 'issue_comment' &&
         startsWith(github.event.comment.body, '/profile')))
       && format('proof-profile-{0}',
@@ -82,7 +86,7 @@ jobs:
   plan:
     runs-on: ubuntu-latest
     name: Plan profile
-    # workflow_dispatch also supports drafts. For issue comments, run only
+    # Automatic PR events also support drafts. For issue comments, run only
     # when the body starts with `/profile` AND the commenter is
     # either the PR author or someone with write access. The measurement jobs
     # check out and *run* the PR's Lean code, so the workflow stays
@@ -92,6 +96,7 @@ jobs:
     # on someone else's fork PR.
     if: >-
       github.event_name == 'workflow_dispatch' ||
+      github.event_name == 'pull_request' ||
       (github.event_name == 'issue_comment' &&
        github.event.issue.pull_request != null &&
        startsWith(github.event.comment.body, '/profile') &&
@@ -165,11 +170,11 @@ jobs:
           CACHE_MATCHED: ${{ steps.lake-cache.outputs.cache-matched-key }}
         run: |
           set -euo pipefail
-          added=$(git diff --name-only --diff-filter=A "$BASE_SHA"...HEAD \
+          added=$(git diff --no-renames --name-only --diff-filter=A "$BASE_SHA"...HEAD \
                     -- LeanPool \
                   | grep '\.lean$' \
                   | tr '\n' ' ' || true)
-          modified=$(git diff --name-only --diff-filter=M "$BASE_SHA"...HEAD \
+          modified=$(git diff --no-renames --name-only --diff-filter=M "$BASE_SHA"...HEAD \
                        -- LeanPool \
                      | grep '\.lean$' \
                      | tr '\n' ' ' || true)
@@ -222,7 +227,7 @@ jobs:
             echo "head_build_modules=$head_build_modules"
           } >> "$GITHUB_OUTPUT"
           if [ -z "$files" ]; then
-            echo "No new or modified Lean files in this diff; profile will no-op."
+            echo "No new or modified Lean files in this diff; report will explain that."
           else
             echo "Will profile: $files"
             echo "Compare against merge base $merge_base: $compare"
@@ -489,8 +494,7 @@ jobs:
     # renderer degrades gracefully when a log is missing. `!cancelled()`
     # keeps this off only when the run was cancelled outright.
     if: >-
-      !cancelled() && needs.plan.result == 'success' &&
-      needs.plan.outputs.files != ''
+      !cancelled() && needs.plan.result == 'success'
     runs-on: ubuntu-latest
     name: Report profile
     # Only the reporting job receives comment permissions; measurement jobs
@@ -507,12 +511,14 @@ jobs:
           persist-credentials: false
 
       - name: Download measurement logs
+        if: needs.plan.outputs.files != ''
         uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093
         with:
           pattern: proof-profile-part-*
           merge-multiple: true
 
       - name: Render profile summary
+        if: needs.plan.outputs.files != ''
         env:
           BASE_SHA: ${{ needs.plan.outputs.base_sha }}
           HEAD_SHA: ${{ needs.plan.outputs.head_sha }}
@@ -546,7 +552,21 @@ jobs:
             || cp scripts/proof-profile/statements.py "$RUNNER_TEMP/statements.py"
           python3 "$RUNNER_TEMP/render.py"
 
-      # A `/profile` comment or dispatch posts the comment itself. The `workflow_run`
+      - name: Report no files to profile
+        if: needs.plan.outputs.files == ''
+        run: |
+          cat > proof-profile.md <<'EOF'
+          ## 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._
+          EOF
+          cat proof-profile.md >> "$GITHUB_STEP_SUMMARY"
+
+      # Same-repo PR runs, `/profile` comments, and dispatches post directly.
+      # Fork PRs use the artifact companion because their token is read-only.
+      # The `workflow_run`
       # companion cannot cover these reliably: GitHub never emits the event
       # for re-run attempts, which silently lost the comment on a bot-opened
       # PR whose first attempt sat waiting for approval (#326).

CONTRIBUTING.md

@@ -18,7 +18,7 @@ There are two paths:
 - **Propose a repo.** Open an issue with the GitHub URL and a maintainer can import it. Repos that Reservoir does not index can be added to [`candidates/manual.txt`](candidates/manual.txt).
 - **Open a content PR.** Add your project under `LeanPool/<YourProject>/`, register it in [`LeanPool/projects/<slug>.yaml`](LeanPool/projects/) — the card must declare `provenance` (`human`, `AI`, or `mix`; see below) — and regenerate the indexes with `lake exe mk_all`. Commit `LeanPool/<YourProject>/Imports.lean`, which publicly imports every project source. Lake discovers all pool modules automatically; keep `LeanPool.lean` unchanged. To use a project, import `LeanPool.<YourProject>.Imports`.
 
-Either way the result must pass CI (build, linters, and quality checks — see [Linting and testing](#linting-and-testing)) and an [LLM review](.github/REVIEW_RULES.md) of fit and significance. Accepted projects must be `sorry`-free, introduce no axioms beyond `Classical.choice`/`propext`/`Quot.sound`, and avoid `unsafe`/`partial`. Each project card must also declare its **provenance** — who wrote the Lean proofs — as `human` (written by people), `AI` (mostly produced by an AI system), or `mix` (both contributed substantially). (Proof profiling via `/profile` is available but informational, not a gate: added files get an absolute profile, while modified files get a base→head compile-cost comparison — useful for checking that a refactor doesn't regress compile time.)
+Either way the result must pass CI (build, linters, and quality checks — see [Linting and testing](#linting-and-testing)) and an [LLM review](.github/REVIEW_RULES.md) of fit and significance. Accepted projects must be `sorry`-free, introduce no axioms beyond `Classical.choice`/`propext`/`Quot.sound`, and avoid `unsafe`/`partial`. Each project card must also declare its **provenance** — who wrote the Lean proofs — as `human` (written by people), `AI` (mostly produced by an AI system), or `mix` (both contributed substantially). (Every PR gets an automatic proof-profile comment, refreshed after pushes and available on demand via `/profile`. It is informational, not a gate: added files get an absolute profile, while modified files get a base→head compile-cost comparison — useful for checking that a refactor doesn't regress compile time.)
 
 ## Dev setup
 

README.md

@@ -44,8 +44,10 @@ To work on a single project you don't need the whole pool built — see the
 
 See [`CONTRIBUTING.md`](CONTRIBUTING.md).
 
-The PR author or a maintainer can comment `/profile` to request an advisory
-compile-cost report. Failed or zero-phase timed runs show unavailable timing
+Every PR, including drafts, gets an advisory compile-cost comment, refreshed
+after pushes. PRs without added or modified Lean files get a no-files report.
+The PR author or a maintainer can also comment `/profile` to rerun it.
+Failed or zero-phase timed runs show unavailable timing
 and are excluded from totals; errors and any successfully measured heartbeat
 counts remain visible.
 

python/tests/test_ci_cache_contract.py

@@ -695,10 +695,11 @@ def test_dependency_tracking_tests_scope(
         assert tracking["if"] == "needs.plan.outputs.dependency_tests == 'true'"
 
 
-def test_profiling_is_opt_in_and_cache_pruning_is_scheduled() -> None:
-    """Advisory compilation and maintenance do not run on ordinary PR events."""
+def test_profiling_is_automatic_and_cache_pruning_is_scheduled() -> None:
+    """PRs get advisory profiles while cache maintenance stays scheduled."""
     profiling = yaml.safe_load((WORKFLOWS / "proof-profile.yml").read_text())
     assert set(profiling.get("on", profiling.get(True))) == {
+        "pull_request",
         "issue_comment",
         "workflow_dispatch",
     }

python/tests/test_proof_profile_workflow.py

@@ -0,0 +1,114 @@
+"""Regression coverage for automatic PR profiling and its no-files report."""
+
+import os
+import subprocess
+from pathlib import Path
+
+import yaml
+
+WORKFLOW = Path(__file__).resolve().parents[2] / ".github/workflows/proof-profile.yml"
+
+
+def test_every_pr_update_can_start_a_profile():
+    """Keep automatic events wired through both admission and concurrency."""
+    workflow = yaml.safe_load(WORKFLOW.read_text())
+    events = workflow.get("on", workflow.get(True))
+    assert set(events["pull_request"]["types"]) == {
+        "opened",
+        "synchronize",
+        "reopened",
+        "ready_for_review",
+    }
+    for expression in (
+        workflow["jobs"]["plan"]["if"],
+        workflow["concurrency"]["group"],
+    ):
+        assert "github.event_name == 'pull_request' ||" in expression
+        assert "draft" not in expression
+    assert "issue_comment" in events
+    assert "workflow_dispatch" in events
+
+
+def test_no_lean_changes_still_produce_a_comment(tmp_path):
+    """Execute the no-files report used when all measurement jobs are skipped."""
+    workflow = yaml.safe_load(WORKFLOW.read_text())
+    report = workflow["jobs"]["report"]
+    assert "needs.plan.outputs.files" not in report["if"]
+    steps = {step["name"]: step for step in report["steps"]}
+    empty_report = steps["Report no files to profile"]
+    assert empty_report["if"] == "needs.plan.outputs.files == ''"
+    for name in ("Download measurement logs", "Render profile summary"):
+        assert steps[name]["if"] == "needs.plan.outputs.files != ''"
+    summary = tmp_path / "summary.md"
+    subprocess.run(
+        ["bash", "-euo", "pipefail", "-c", empty_report["run"]],
+        cwd=tmp_path,
+        env={**os.environ, "GITHUB_STEP_SUMMARY": str(summary)},
+        check=True,
+        capture_output=True,
+    )
+    comment = (tmp_path / "proof-profile.md").read_text()
+    assert "No added or modified Lean files" in comment
+    assert summary.read_text() == comment
+    assert (
+        "needs.plan.outputs.files"
+        not in steps["Post sticky PR comment (writable-token runs)"]["if"]
+    )
+
+
+def test_forks_keep_the_artifact_comment_path():
+    """Read-only fork runs must stage the same report for the writable poster."""
+    workflow = yaml.safe_load(WORKFLOW.read_text())
+    steps = {step["name"]: step for step in workflow["jobs"]["report"]["steps"]}
+    direct = steps["Post sticky PR comment (writable-token runs)"]["if"]
+    assert "github.event_name != 'pull_request'" in direct
+    assert (
+        "github.event.pull_request.head.repo.full_name == github.repository" in direct
+    )
+    for name in (
+        "Stage comment payload for the companion workflow",
+        "Upload comment payload",
+    ):
+        assert "steps.direct_post.outcome != 'success'" in steps[name]["if"]
+
+
+def test_renamed_lean_files_are_profiled(tmp_path):
+    """A pure rename must produce an added file instead of an empty profile."""
+    for arguments in (
+        ["init", "-q"],
+        ["config", "user.name", "Test"],
+        ["config", "user.email", "test@example.com"],
+    ):
+        subprocess.run(["git", *arguments], cwd=tmp_path, check=True)
+    project = tmp_path / "LeanPool"
+    project.mkdir()
+    source = project / "Before.lean"
+    source.write_text("theorem probe : True := .intro\n")
+    subprocess.run(["git", "add", "."], cwd=tmp_path, check=True)
+    subprocess.run(["git", "commit", "-qm", "base"], cwd=tmp_path, check=True)
+    base = subprocess.check_output(
+        ["git", "rev-parse", "HEAD"], cwd=tmp_path, text=True
+    ).strip()
+    source.rename(project / "After.lean")
+    subprocess.run(["git", "add", "."], cwd=tmp_path, check=True)
+    subprocess.run(["git", "commit", "-qm", "rename"], cwd=tmp_path, check=True)
+    workflow = yaml.safe_load(WORKFLOW.read_text())
+    selection = next(
+        step for step in workflow["jobs"]["plan"]["steps"] if step.get("id") == "files"
+    )
+    output = tmp_path / "output"
+    subprocess.run(
+        ["bash", "-euo", "pipefail", "-c", selection["run"]],
+        cwd=tmp_path,
+        env={
+            **os.environ,
+            "BASE_SHA": base,
+            "CACHE_MATCHED": "",
+            "GITHUB_OUTPUT": str(output),
+        },
+        check=True,
+        capture_output=True,
+    )
+    values = dict(line.split("=", 1) for line in output.read_text().splitlines())
+    assert values["added"].strip() == "LeanPool/After.lean"
+    assert values["profile_files"].strip() == "LeanPool/After.lean"