run_single_file: pass pull request to prepare step

Author: henrykmichalewski

scripts/README.md

@@ -1,12 +1,13 @@
 # Codex helper
 
-The `run_single_file.py` script runs Codex inside Docker on a single file from this repository. It builds both `private_mathlib4` and `formal_conjectures` before invoking Codex.
+The `run_single_file.py` script runs Codex inside Docker on a single file from this repository. It builds both `private_mathlib4` and `formal_conjectures` before invoking Codex. When using the `--prep` option you must also provide `--pr` so `prepare_single_file.py` can fetch review comments for that pull request.
 
 Example:
 
 ```bash
 GEMINI_API_KEY="" ./scripts/run_single_file.py \
   --prep FormalConjectures/Paper/CasasAlvero.lean \
+  --pr https://github.com/OWNER/REPO/pull/123 \
   --export FormalConjectures/Paper/CasasAlvero.lean \
   run --auto-continuous --auto-continuous-first-doc \
   "lake build FormalConjectures/Paper/CasasAlvero.lean"

scripts/run_single_file.py

@@ -18,6 +18,17 @@ def parse_args() -> argparse.Namespace:
     parser.add_argument("--image", default="codex_patched", help="Docker image tag")
     parser.add_argument("--name", help="Container name (default: script-<pid>)")
     parser.add_argument("--prep", help="Prepare a single Lean file")
+    parser.add_argument(
+        "--pr",
+        dest="pull_request",
+        help="GitHub pull request URL used when preparing a file",
+    )
+    parser.add_argument(
+        "--gh-token",
+        dest="github_token",
+        default=None,
+        help="GitHub token for API access when preparing a file",
+    )
     parser.add_argument(
         "--export", action="append", default=[], help="Files to export from container"
     )
@@ -27,6 +38,8 @@ def parse_args() -> argparse.Namespace:
     args = parser.parse_args()
     if not args.cmd:
         parser.error("Need Codex command")
+    if args.prep and not args.pull_request:
+        parser.error("--prep requires --pr")
     return args
 
 
@@ -96,13 +109,18 @@ def main() -> int:
         )
 
         if args.prep:
+            prep_cmd = (
+                f"python3 -m scripts.prepare_single_file --lean {shlex.quote(args.prep)} "
+                f"--out tmp_prep --lean-explore-local --pr {shlex.quote(args.pull_request)}"
+            )
+            if args.github_token:
+                prep_cmd += f" --gh-token {shlex.quote(args.github_token)}"
             docker(
                 "exec",
                 cid,
                 "bash",
                 "-euc",
-                f"cd {repo} && "
-                f"python3 -m scripts.prepare_single_file --lean {args.prep} --out tmp_prep --lean-explore-local && "
+                f"cd {repo} && {prep_cmd} && "
                 f"cp tmp_prep/AGENTS_single_task.md AGENTS.md && "
                 f"cp tmp_prep/$(basename {args.prep}) {args.prep}",
             )