diff --git a/.github/copilot-instructions.md b/.github/copilot-instructions.md new file mode 100644 index 0000000000..6f4d5b152c --- /dev/null +++ b/.github/copilot-instructions.md @@ -0,0 +1,61 @@ +# Copilot review instructions + +This repository runs two LLM reviewers on pull requests: + +1. **GitHub Copilot's automatic code review** (you). +2. **A custom workflow** that calls `gpt-5.4-mini` against the rules in + [`./REVIEW_RULES.md`](./REVIEW_RULES.md). + +Both reviewers should apply the same standards. Read [`./REVIEW_RULES.md`](./REVIEW_RULES.md) +in full before reviewing; the summary below is for convenience only. + +## What to review + +Lean Pool curates **completed, self-contained formalization projects of real +mathematics, physics, computer science, or similarly serious formal subjects +at the graduate or research level**. Single lemmas, golfing PRs, +infrastructure-only PRs, and incremental API tweaks do **not** belong, even +when they compile cleanly. + +When reviewing a PR, focus on the judgement calls only an LLM can make: + +- **S1 Significance** — graduate/research level, anchored in a paper / + textbook / problem statement. +- **S2 Self-containment** — PR ends at a coherent landmark. +- **S3 Project card** — new top-level projects must include a Lean module + docstring (`/-! ... -/`) at the top of their entry-point file describing + what was formalized, source, authors, and status. +- **S4 Statement matches description** — formal Lean theorem matches its + informal claim (no missing hypotheses, no quantifier swaps, etc.). +- **S5 Verbose proofs** — flag clearly golfable proofs (repeated `have`s, + one-line tactic where term-mode is used, `simp` chains that collapse). +- **S6 Redundancy** — trivial reformulations, possible mathlib duplicates, + declarations that exist only to be inlined. +- **S7 Pointless infrastructure** — types/instances/wrappers with no use in + the PR's main results. + +## What NOT to review + +The following are caught by separate linters in CI; **do not** flag them: + +- Presence of `sorry` / `admit` / new `axiom`. +- File headers, copyright, license, authorship metadata. +- File-size or proof-size limits. +- `set_option maxHeartbeats` overrides. +- Naming conventions (`camelCase` vs `snake_case`). +- Bare `simp` vs `simp only`. +- `decide` / `native_decide` justification comments. +- Presence of docstrings on public declarations. + +## Style + +- Comment only when a specific rule above is violated. +- Cite the file and line where you can. +- Suggest a concrete fix, not just a complaint. +- When uncertain, say nothing. +- Do not rewrite proofs in full; suggest direction. +- Do not comment on commit messages, PR titles, or PR descriptions beyond + verifying that S3's project card requirement is met for new top-level + projects. + +When in doubt, defer to [`./REVIEW_RULES.md`](./REVIEW_RULES.md). diff --git a/.github/workflows/llm-review.yml b/.github/workflows/llm-review.yml index 716e44286c..ab3915de2e 100644 --- a/.github/workflows/llm-review.yml +++ b/.github/workflows/llm-review.yml @@ -77,9 +77,14 @@ jobs: GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} # Override here if the model name needs to change. REVIEW_MODEL: gpt-5.4-mini - # USD per 1M tokens. Update against - # https://openai.com/api/pricing/ when REVIEW_MODEL changes. - # Set both to 0 to suppress the cost line; tokens still shown. - INPUT_PRICE_PER_M: "0" - OUTPUT_PRICE_PER_M: "0" + # The review job calls OpenAI with `service_tier="flex"` first + # (slower, ~50% cheaper) and falls back to standard (`auto`) on + # 429 Resource Unavailable. Cost is rendered at the tier that + # actually served the request. Verify rates against + # https://developers.openai.com/api/docs/pricing when bumping + # REVIEW_MODEL. Set any pair to 0 to suppress the cost line. + INPUT_PRICE_PER_M_FLEX: "0.375" + OUTPUT_PRICE_PER_M_FLEX: "2.25" + INPUT_PRICE_PER_M_STANDARD: "0.75" + OUTPUT_PRICE_PER_M_STANDARD: "4.50" run: uv run python -m lean_pool.review diff --git a/python/lean_pool/review.py b/python/lean_pool/review.py index 5ce8787f1f..a7a6194858 100644 --- a/python/lean_pool/review.py +++ b/python/lean_pool/review.py @@ -2,16 +2,23 @@ Reads the rules from ``.github/REVIEW_RULES.md``, fetches the PR diff via the GitHub CLI, asks the configured OpenAI model to apply the rules, and posts the -findings as a single PR comment that includes token usage and (optionally) -estimated USD cost. +findings as a single PR comment that includes token usage, the service tier +that served the request, and (optionally) estimated USD cost. + +The reviewer prefers OpenAI's `flex` tier (cheaper, slower, occasionally +unavailable). When flex returns 429 Resource Unavailable, the request is +retried with `service_tier="auto"` (standard pricing). The rendered comment +shows which tier was actually used and costs the request at that tier's rate. Environment variables: - OPENAI_API_KEY: OpenAI credentials (required). - PR_NUMBER: Pull request number to review (required). - GH_TOKEN: Token for the GitHub CLI (required in CI). - REVIEW_MODEL: Model name; defaults to ``gpt-5.4-mini``. - INPUT_PRICE_PER_M: USD per 1M input tokens (optional; default 0). - OUTPUT_PRICE_PER_M: USD per 1M output tokens (optional; default 0). + OPENAI_API_KEY: OpenAI credentials (required). + PR_NUMBER: Pull request number to review (required). + GH_TOKEN: Token for the GitHub CLI (required in CI). + REVIEW_MODEL: Model name; defaults to ``gpt-5.4-mini``. + INPUT_PRICE_PER_M_FLEX: USD per 1M input tokens at flex rates. + OUTPUT_PRICE_PER_M_FLEX: USD per 1M output tokens at flex rates. + INPUT_PRICE_PER_M_STANDARD: USD per 1M input tokens at standard rates. + OUTPUT_PRICE_PER_M_STANDARD: USD per 1M output tokens at standard rates. Run: uv run python -m lean_pool.review @@ -27,11 +34,13 @@ from textwrap import dedent from typing import Any -from openai import OpenAI +from openai import OpenAI, RateLimitError REPO_ROOT = Path(__file__).resolve().parents[2] RULES_PATH = REPO_ROOT / ".github" / "REVIEW_RULES.md" DEFAULT_MODEL = "gpt-5.4-mini" +# Flex tier requests can take longer than the default 10-minute timeout. +REQUEST_TIMEOUT_SECONDS = 900.0 SEVERITY_ICON = {"info": "ℹ️", "warning": "⚠️", "blocking": "🛑"} VERDICT_ICON = { @@ -73,6 +82,20 @@ def _float_env(name: str) -> float: return 0.0 +def load_pricing() -> dict[str, tuple[float, float]]: + """Load (input_per_m, output_per_m) per service tier from the environment.""" + return { + "flex": ( + _float_env("INPUT_PRICE_PER_M_FLEX"), + _float_env("OUTPUT_PRICE_PER_M_FLEX"), + ), + "standard": ( + _float_env("INPUT_PRICE_PER_M_STANDARD"), + _float_env("OUTPUT_PRICE_PER_M_STANDARD"), + ), + } + + def run_gh(*args: str, stdin: str | None = None) -> str: """Run ``gh`` with the given arguments and return stdout. @@ -101,36 +124,48 @@ def fetch_diff(pr_number: str) -> str: return run_gh("pr", "diff", pr_number) -def request_review(model: str, rules: str, diff: str) -> tuple[dict, Any]: +def request_review(model: str, rules: str, diff: str) -> tuple[dict, Any, str]: """Ask the model to apply ``rules`` to ``diff``. + Tries the ``flex`` service tier first; if OpenAI returns 429 Resource + Unavailable, retries with ``service_tier="auto"`` (standard tier). + Returns: - A tuple ``(payload, usage)`` where ``payload`` is the parsed JSON - review and ``usage`` is the OpenAI ``CompletionUsage`` object (or - ``None`` if the SDK did not return one). + ``(payload, usage, tier)`` where ``payload`` is the parsed JSON + review, ``usage`` is the OpenAI ``CompletionUsage`` object (or + ``None``), and ``tier`` is ``"flex"`` or ``"standard"``. """ - client = OpenAI() - response = client.chat.completions.create( - model=model, - messages=[ - {"role": "system", "content": SYSTEM_PROMPT}, - { - "role": "user", - "content": ( - f"## Review rules\n\n{rules}\n\n## PR diff\n\n```diff\n{diff}\n```" - ), - }, - ], - response_format={"type": "json_object"}, - ) + client = OpenAI(timeout=REQUEST_TIMEOUT_SECONDS) + user_content = f"## Review rules\n\n{rules}\n\n## PR diff\n\n```diff\n{diff}\n```" + messages = [ + {"role": "system", "content": SYSTEM_PROMPT}, + {"role": "user", "content": user_content}, + ] + + try: + response = client.chat.completions.create( + model=model, + messages=messages, + response_format={"type": "json_object"}, + service_tier="flex", + ) + tier = "flex" + except RateLimitError: + # Flex pool exhausted; retry on standard tier. + response = client.chat.completions.create( + model=model, + messages=messages, + response_format={"type": "json_object"}, + service_tier="auto", + ) + tier = "standard" + content = response.choices[0].message.content or "{}" - return json.loads(content), response.usage + return json.loads(content), response.usage, tier -def render_usage( - usage: Any, input_price_per_m: float, output_price_per_m: float -) -> str: - """Render a one-line token / cost footer. +def render_usage(usage: Any, tier: str, prices: dict[str, tuple[float, float]]) -> str: + """Render a one-line token / tier / cost footer. Returns an empty string if ``usage`` is unavailable. """ @@ -138,21 +173,24 @@ def render_usage( return "" in_tok = getattr(usage, "prompt_tokens", 0) or 0 out_tok = getattr(usage, "completion_tokens", 0) or 0 - line = f"**Tokens:** {in_tok:,} in / {out_tok:,} out" - if input_price_per_m > 0 or output_price_per_m > 0: - cost = (in_tok * input_price_per_m + out_tok * output_price_per_m) / 1_000_000 - line += f" · **Cost:** ${cost:.4f}" + in_price, out_price = prices.get(tier, (0.0, 0.0)) + + parts = [f"**Tokens:** {in_tok:,} in / {out_tok:,} out"] + parts.append(f"**Tier:** `{tier}`") + if in_price > 0 or out_price > 0: + cost = (in_tok * in_price + out_tok * out_price) / 1_000_000 + parts.append(f"**Cost:** ${cost:.4f}") else: - line += " · _(set INPUT_PRICE_PER_M / OUTPUT_PRICE_PER_M for cost)_" - return line + parts.append(f"_(set INPUT/OUTPUT_PRICE_PER_M_{tier.upper()} for cost)_") + return " · ".join(parts) def render_comment( payload: dict, model: str, usage: Any, - input_price_per_m: float, - output_price_per_m: float, + tier: str, + prices: dict[str, tuple[float, float]], ) -> str: """Render the model's payload as a Markdown PR comment body.""" summary = (payload.get("summary") or "").strip() @@ -189,7 +227,7 @@ def render_comment( lines.append("") lines.append("---") - usage_line = render_usage(usage, input_price_per_m, output_price_per_m) + usage_line = render_usage(usage, tier, prices) if usage_line: lines.append(usage_line) lines.append( @@ -216,8 +254,7 @@ def main() -> int: return 2 model = os.environ.get("REVIEW_MODEL", DEFAULT_MODEL) - input_price = _float_env("INPUT_PRICE_PER_M") - output_price = _float_env("OUTPUT_PRICE_PER_M") + prices = load_pricing() rules = RULES_PATH.read_text(encoding="utf-8") diff = fetch_diff(pr_number) @@ -226,13 +263,13 @@ def main() -> int: print("Empty diff; nothing to review.", file=sys.stderr) return 0 - payload, usage = request_review(model=model, rules=rules, diff=diff) + payload, usage, tier = request_review(model=model, rules=rules, diff=diff) comment = render_comment( payload, model=model, usage=usage, - input_price_per_m=input_price, - output_price_per_m=output_price, + tier=tier, + prices=prices, ) post_comment(pr_number, comment) return 0