diff --git a/.github/workflows/proof-profile.yml b/.github/workflows/proof-profile.yml index b97c53e69f..393939d038 100644 --- a/.github/workflows/proof-profile.yml +++ b/.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). diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index cc98a25749..1f2f7e212c 100644 --- a/CONTRIBUTING.md +++ b/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//`, register it in [`LeanPool/projects/.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//Imports.lean`, which publicly imports every project source. Lake discovers all pool modules automatically; keep `LeanPool.lean` unchanged. To use a project, import `LeanPool..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 diff --git a/README.md b/README.md index 61a4832308..1ef8a48b8c 100644 --- a/README.md +++ b/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. diff --git a/python/tests/test_ci_cache_contract.py b/python/tests/test_ci_cache_contract.py index 3e79ee6e19..cbfd2c2956 100644 --- a/python/tests/test_ci_cache_contract.py +++ b/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", } diff --git a/python/tests/test_proof_profile_workflow.py b/python/tests/test_proof_profile_workflow.py new file mode 100644 index 0000000000..f019b732cf --- /dev/null +++ b/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"