feat(meta): add agent-review rubric and example GitHub Action

.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 -->
+          **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"

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.