diff --git a/python/lean_pool/codex_review.py b/python/lean_pool/codex_review.py index 849dd3c830..d60a5ff955 100644 --- a/python/lean_pool/codex_review.py +++ b/python/lean_pool/codex_review.py @@ -9,6 +9,7 @@ import json import os +import re import signal import subprocess import sys @@ -195,7 +196,7 @@ def run_codex(request: dict, directory: Path) -> dict: if process.returncode: raise RuntimeError(f"Codex exited {process.returncode}: {stderr[-2000:]}") envelope = json.loads((directory / "answer.json").read_text()) - payload = json.loads(envelope["review_json"]) + payload = decode_review_json(envelope["review_json"]) if not isinstance(payload, dict) or not payload: raise ValueError("Codex did not return a review object") usage = extract_usage(stdout) @@ -207,6 +208,22 @@ def run_codex(request: dict, directory: Path) -> dict: } +def decode_review_json(source: str) -> Any: + """Preserve literal Lean/LaTeX backslashes in otherwise valid model JSON.""" + try: + return json.loads(source) + except json.JSONDecodeError as error: + if error.msg != "Invalid \\escape": + raise + # Consume valid escape pairs intact, including already escaped backslashes. + repaired = re.sub( + r'\\(?:["\\/bfnrtu]|([^"\\/bfnrtu]))', + lambda match: "\\\\" + match[1] if match[1] else match[0], + source, + ) + return json.loads(repaired) + + def stop_codex(process: subprocess.Popen) -> None: """Let the account dispatcher forward termination to its separate child group.""" try: diff --git a/python/tests/test_codex_review.py b/python/tests/test_codex_review.py index 5675d908fe..ab32348154 100644 --- a/python/tests/test_codex_review.py +++ b/python/tests/test_codex_review.py @@ -256,3 +256,31 @@ def test_azure_partial_usage_labels_partial_estimate(): ) assert "**Estimated cost:** $1.0500" in footer assert "partial" in footer + + +def test_review_json_preserves_literal_mathematical_backslashes(): + """An invalid JSON escape must not lose completed mathematical evidence.""" + raw = ( + r'{"verdict":"discuss","evidence":"\lambda x => x; ' + r'\\proper; \nline; \"quote\"; \set"}' + ) + result = codex_review.decode_review_json(raw) + assert result == { + "verdict": "discuss", + "evidence": '\\lambda x => x; \\proper; \nline; "quote"; \\set', + } + + +@pytest.mark.parametrize( + "source", [r'{"evidence":"\u123"}', '{"verdict":"pass"', r'{"x":\broken}'] +) +def test_review_json_other_malformed_output_still_fails(source): + """Backslash handling cannot invent missing structure or repair other errors.""" + with pytest.raises(json.JSONDecodeError): + codex_review.decode_review_json(source) + + +def test_valid_review_json_is_unchanged(): + """Valid escapes and Unicode keep their ordinary JSON meanings.""" + payload = {"verdict": "pass", "evidence": '\\lambda\n"quoted"\tλ'} + assert codex_review.decode_review_json(json.dumps(payload)) == payload