From 744ed44ecc96c5d4733e067234f8bff0a9dbd811 Mon Sep 17 00:00:00 2001 From: Justin Findlay Date: Thu, 18 Jun 2026 23:59:01 -0400 Subject: [PATCH] feat(meta): add agent-review rubric and example GitHub Action * `AGENTS-REVIEW.md`: A vendor-neutral, rubric for a single review pass on a Physlib PR. * `.github/workflows/agent-review.yml`: An example implementation triggered by the `agent-review` label. Co-authored-by: Claude Sonnet 4.6 --- .github/workflows/AgentReview.yml | 157 ++++++++++++++++++++++++++++++ AGENTS-REVIEW.md | 99 +++++++++++++++++++ 2 files changed, 256 insertions(+) create mode 100644 .github/workflows/AgentReview.yml create mode 100644 AGENTS-REVIEW.md diff --git a/.github/workflows/AgentReview.yml b/.github/workflows/AgentReview.yml new file mode 100644 index 000000000..b4e3a441c --- /dev/null +++ b/.github/workflows/AgentReview.yml @@ -0,0 +1,157 @@ +name: Agent PR Review + +on: + pull_request_target: + types: [labeled] + +# One concurrent run per PR; cancel any in-flight run for the same PR when a new label fires. +concurrency: + group: agent-review-${{ github.event.pull_request.number }} + cancel-in-progress: true + +permissions: + contents: read + pull-requests: write + +jobs: + agent-review: + name: Agent review pass + runs-on: ubuntu-latest + + # Only run when the triggering label is `agent-review`. Skip drafts and PRs marked + # `awaiting-author`. + if: | + github.event.label.name == 'agent-review' && + github.event.pull_request.draft == false && + !contains(github.event.pull_request.labels.*.name, 'awaiting-author') + + steps: + - name: Checkout PR base + uses: actions/checkout@v4 + with: + # Check out the base branch so the agent can search the repository. + ref: ${{ github.event.pull_request.base.sha }} + fetch-depth: 0 + + - name: Fetch PR head + run: | + git fetch origin pull/${{ github.event.pull_request.number }}/head:pr-head + + - name: Generate unified diff + run: | + git diff ${{ github.event.pull_request.base.sha }}...pr-head \ + -- '*.lean' '*.md' > /tmp/pr.diff + wc -l /tmp/pr.diff + + - name: Read rubric + run: | + cp AGENTS-REVIEW.md /tmp/rubric.md + cp AGENTS.md /tmp/agents.md + cp AI-POLICY.md /tmp/ai-policy.md + cp docs/ReviewGuidelines.md /tmp/review-guidelines.md + + - name: Run agent review + id: review + env: + AGENT_REVIEW_API_KEY: ${{ secrets.AGENT_REVIEW_API_KEY }} + # Configure the model here. Default: a mid-tier model. + # Escalate to a top-tier model only for large or complex PRs by exception. + AGENT_MODEL: "claude-sonnet-4-5" + PR_TITLE: ${{ github.event.pull_request.title }} + PR_NUMBER: ${{ github.event.pull_request.number }} + run: | + python3 - <<'EOF' + import os, json, urllib.request, sys + from pathlib import Path + + api_key = os.environ["AGENT_REVIEW_API_KEY"] + model = os.environ.get("AGENT_MODEL", "claude-sonnet-4-5") + pr_title = os.environ["PR_TITLE"] + pr_number = os.environ["PR_NUMBER"] + + rubric = Path("/tmp/rubric.md").read_text() + agents = Path("/tmp/agents.md").read_text() + policy = Path("/tmp/ai-policy.md").read_text() + guidelines = Path("/tmp/review-guidelines.md").read_text() + diff = Path("/tmp/pr.diff").read_text() + + # Truncate diff if very large; the agent is told to flag scope issues. + MAX_DIFF_CHARS = 40_000 + if len(diff) > MAX_DIFF_CHARS: + diff = diff[:MAX_DIFF_CHARS] + "\n\n[diff truncated — PR exceeds token budget]" + + system_prompt = f"""You are performing a single review pass on a Physlib pull request. + Follow AGENTS-REVIEW.md exactly. + + --- + AGENTS-REVIEW.md: + {rubric} + + --- + AGENTS.md (authoring rules): + {agents} + + --- + AI-POLICY.md: + {policy} + + --- + docs/ReviewGuidelines.md: + {guidelines} + """ + + user_prompt = f"""PR #{pr_number}: {pr_title} + + Unified diff (Lean and Markdown files only): + + {diff} + + Produce your review now. Follow the output contract in AGENTS-REVIEW.md §5 exactly. + If no issues found, say so and stop. + """ + + payload = { + "model": model, + "max_tokens": 2048, + "system": system_prompt, + "messages": [{"role": "user", "content": user_prompt}], + } + + req = urllib.request.Request( + "https://api.anthropic.com/v1/messages", + data=json.dumps(payload).encode(), + headers={ + "x-api-key": api_key, + "anthropic-version": "2023-06-01", + "content-type": "application/json", + }, + method="POST", + ) + with urllib.request.urlopen(req, timeout=120) as resp: + body = json.loads(resp.read()) + + review_text = body["content"][0]["text"] + + # Write for the next step to pick up. + Path("/tmp/review.md").write_text(review_text) + + print(review_text) + EOF + + - name: Post review comment + env: + GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} + PR_NUMBER: ${{ github.event.pull_request.number }} + run: | + REVIEW=$(cat /tmp/review.md) + BODY=" + **Agent review pass** (model: \`$AGENT_MODEL\`, rubric: [AGENTS-REVIEW.md](https://github.com/${{ github.repository }}/blob/${{ github.event.pull_request.base.sha }}/AGENTS-REVIEW.md)) + + > This is an automated first-pass review. A human reviewer will follow. All findings are + > advisory unless labeled \`blocking\`. Mathlib citations are suggestions only. + + --- + + ${REVIEW}" + + gh pr comment "$PR_NUMBER" --body "$BODY" diff --git a/AGENTS-REVIEW.md b/AGENTS-REVIEW.md new file mode 100644 index 000000000..7f5a1d47d --- /dev/null +++ b/AGENTS-REVIEW.md @@ -0,0 +1,99 @@ +# Agent review instructions for Physlib + +Read [AGENTS.md](AGENTS.md), [AI-POLICY.md](AI-POLICY.md), and [docs/ReviewGuidelines.md](docs/ReviewGuidelines.md) before reading this file; this file references those documents and does not repeat them. Where this file and those documents appear to conflict, flag the conflict rather than guess. + +--- + +## 1. Posture + +You assist a human reviewer; you do not replace one. The human continues to review every PR regardless of what you produce. + +The asymmetry that drives the whole design: + +> A *missed* issue is still caught by the human reviewer. A *false positive* consumes a human reviewer. **Optimize for precision over recall.** + +Hard constraints: + +- **Bounded.** Review report only. Do not add or suggest edits or communicate with the contributor. All communication with human contributors must be conducted by humans (`AI-POLICY.md` §3.1). +- **Calibrated.** Only surface the issues worth a maintainer's attention. Do not exhaustively catalog all minor flaws (see §5). +- **Located and severity-tagged.** Every comment must cite `file:line` (or `file:line-range`) and carry a severity label: `blocking`, `suggestion`, or `question`. +- **Epistemically honest.** Distinguish verifiable claims from speculation. Never assert a Mathlib lemma exists unless you have verified it via a retrieval tool. If you cannot verify, say so explicitly (see §4). + +--- + +## 2. Out of scope — defer to CI + +Stay completely silent on anything the deterministic linters already catch. Re-flagging is noise and token waste. The following are fully handled by CI and are **not** your concern: + +- Trailing whitespace, line-length, indentation, `#check`/`#eval` in submitted files — caught by `./scripts/lint-style.sh`. +- `sorry`, `axiom`, `@[sorryful]`/`@[pseudo]` tagging — caught by `lake exe sorry_lint` and `lake exe lint_all`. +- Missing or unsorted imports in `Physlib.lean` / `PhyslibAlpha.lean` — caught by `lake exe check_file_imports`. +- Spelling errors — caught by `codespell`. +- Build failures — caught by `lake build`. +- Duplicate TODO tags — caught by `lake exe check_dup_tags`. +- `PhyslibAlpha` linters — caught by `lake exe runPhyslibAlphaLinters` and the alpha Python linters. + +If CI has not yet run, note that you are not a substitute for it and leave those checks to CI. + +--- + +## 3. Review rubric + +Work through the diff once. The rubric items below share context from a single read; do not split them across multiple passes. + +### 3.1 Code quality (`docs/ReviewGuidelines.md` §Code quality) + +- **Correct abstraction.** Are lemmas and definitions stated at the right level of generality? Could the same statement be proved under weaker hypotheses? Is a definition more concrete than it needs to be? +- **Concise proofs.** Could a proof be materially shorter using existing Mathlib or Physlib lemmas? Flag only when the shortening would be substantial, not cosmetic. Severity: `suggestion`. +- **Proof splitting.** Apply the heuristics in `AGENTS.md` §Proof structure. Flag when a proof exceeds 50 LOC and a natural split exists. Name the extraction direction (by meaning or by structure). Severity: `suggestion`. +- **Docstrings.** Every definition must have a docstring (`AGENTS.md` §Content). Important lemmas should have one. Flag missing docstrings on definitions as `blocking`; on important lemmas as `suggestion`. +- **`lemma` vs. `theorem`.** Use `lemma` unless the result is well known in the physics literature (`AGENTS.md` §Content, `docs/ReviewGuidelines.md` §Style conventions). Flag misuse as `suggestion`. +- **`axiom` / `sorry` / `True` fields / trivial existentials.** These are CI-caught (§2), but if you notice one that CI may have missed (e.g. in a conditional build path), flag it as `blocking`. + +### 3.2 Organization (`docs/ReviewGuidelines.md` §Organization) + +- **Correct placement.** Is each lemma or definition in the right file? A general result needed for classical mechanics belongs in `Space.Derivatives.Basic`, not in the classical mechanics file (`AGENTS.md` §Content). Flag misplacement as `suggestion`. +- **Module scope.** Does the module have a well-defined scope? Is it easy to navigate? + +### 3.3 PR scope (`docs/ReviewGuidelines.md` §PR and authorship, `AGENTS.md` §PR scope) + +- **Single coherent concept.** Every definition and lemma should either be that concept or supply the minimal API to state and prove it. Authors systematically under-split; be mildly firm here. +- **PR length.** Flag PRs over 300 lines as candidates for splitting; note this is `suggestion`, not a block. PRs 150–300 lines: note if splitting seems natural. Under 150 lines: no comment on length. +- Flag scope violations as `blocking` (multiple unrelated concepts) or `suggestion` (one concept but with excess scaffolding that could be a PR buildup sequence). + +### 3.4 Physlib duplication + +Search the repository for lemmas or definitions that appear functionally equivalent to something being added. Flag confirmed in-repo duplicates as `blocking`. Be precise: cite both the new item and the existing one with file and line. + +--- + +## 4. Mathlib duplication + +Checking Mathlib duplication reliably requires retrieval over a large external corpus (Loogle, leansearch, or `exact?` in CI). Recalling Mathlib from model weights alone is unreliable and must not produce asserted claims. + +**Rule:** For Mathlib duplication, you may only say: + +> "Consider checking whether `[LemmaName]` already exists in Mathlib — I cannot verify this; the human author must confirm per `AI-POLICY.md` §2.1." + +**Never assert that a Mathlib lemma exists.** Severity for such suggestions: `question`. + +--- + +## 5. Output contract + +Each comment must have this structure: + +``` +**[severity]** `file:line` — one-line rationale. (optional: pointer to AGENTS.md/ReviewGuidelines section) +``` + +Where `severity` is one of: +- `blocking` — must be addressed before merge +- `suggestion` — improvement worth doing, not a block +- `question` — something to check or clarify; may be a non-issue + +Rules: +- Report all `blocking` issues first, then up to 5 `suggestion`s and `question`s each, ordered by severity per review. Discard the rest if you have more. +- If you have no comments worth raising, say: "No issues found." Do not pad with low-value observations. +- Do not repeat what CI already catches (§2). +- Do not restate the contents of the PR as a summary; focus entirely on review findings.