diff --git a/python/lean_pool/review.py b/python/lean_pool/review.py index fa3cc988d5..406ea2ba54 100644 --- a/python/lean_pool/review.py +++ b/python/lean_pool/review.py @@ -290,6 +290,25 @@ ) +# Appended to every system prompt. The first challenge review (PR #289) +# came back with the mathematics unreadable: `over ^R09` for `over ℚ`, +# `|(discr K : ^])| ^U 8.25 ^ finrank ^R0a K` for +# `|(discr K : ℝ)| ≥ 8.25 ^ finrank ℚ K`. The mangling is the model's own — +# nothing between `json.loads` and the posted comment touches those +# strings — and it is not a systematic escape (`ℚ` came out as both `^R0a` +# and `^R09`), so it cannot be decoded after the fact. Ask for the +# characters directly, with a graceful fallback to words, since a review of +# Lean that cannot render `ℚ` or `≥` is worth much less in this repository. +NOTATION_RULE = dedent( + """\ + Notation: when you quote Lean, copy the characters exactly as they + appear in the diff, Unicode included (ℚ, ℝ, ℕ, ≤, ≥, ∀, ∃, ⁄, ₀). + Never transliterate, escape, or approximate them. If you cannot + reproduce a symbol faithfully, describe it in words instead — a + sentence is readable, a mangled glyph is not. + """ +) + # Rules document and system prompt per PR kind, keyed by `classify_pr`. REVIEW_MODES: dict[str, tuple[Path, str]] = { "project": (PROJECT_RULES_PATH, SYSTEM_PROMPT_PROJECT), @@ -755,6 +774,7 @@ def request_review( full diff was reviewed). """ client = OpenAI(timeout=REQUEST_TIMEOUT_SECONDS) + system_prompt = f"{system_prompt}\n{NOTATION_RULE}" scaffold_tokens = estimate_tokens(rules) + estimate_tokens(system_prompt) diff_budget_tokens = MAX_INPUT_TOKENS - scaffold_tokens for attempt in range(REVIEW_FIT_ATTEMPTS): diff --git a/python/tests/test_review.py b/python/tests/test_review.py index b05b383528..22585eb05d 100644 --- a/python/tests/test_review.py +++ b/python/tests/test_review.py @@ -573,3 +573,53 @@ def test_render_comment_notes_truncation() -> None: assert "Partial review" in body assert "250" in body and "317" in body assert "3,112,190" in body + + +def test_every_review_mode_asks_for_literal_unicode(monkeypatch) -> None: + """The notation rule reaches the model whichever mode is reviewing. + + PR #289's challenge review came back with `over ^R09` where `over ℚ` + belonged, so a Lean review that cannot render its own notation is a + regression worth a test. + """ + from lean_pool import review + + captured: list[dict] = [] + + class _Message: + content = '{"summary": "s", "verdict": "approve", "findings": []}' + + class _Choice: + message = _Message() + + class _Response: + choices = [_Choice()] + usage = None + + class _Completions: + def create(self, **kwargs): + captured.append(kwargs) + return _Response() + + class _Chat: + completions = _Completions() + + class _Client: + chat = _Chat() + + def __init__(self, **kwargs): + pass + + monkeypatch.setattr(review, "OpenAI", _Client) + + for _rules_path, system_prompt in review.REVIEW_MODES.values(): + captured.clear() + review.request_review( + model="gpt-5.5", + rules="rules", + diff="diff --git a/A b/A", + system_prompt=system_prompt, + ) + sent = captured[0]["messages"][0]["content"] + assert "copy the characters exactly" in sent + assert "ℚ" in sent