Set gpt-5.4-mini pricing in LLM review workflow

.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).

.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

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,58 +124,73 @@ 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.
     """
     if usage is None:
         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