| 321 | return final_proof_dict |
| 322 | |
| 323 | def parse_args(): |
| 324 | parser = argparse.ArgumentParser(description="Verify Lean theorem proofs") |
| 325 | |
| 326 | # File paths |
| 327 | parser.add_argument("--input_file", required=True, |
| 328 | help="Path to the input file containing answers to be verified") |
| 329 | parser.add_argument("--output_file", required=True, |
| 330 | help="Path to the output file to save verification results") |
| 331 | |
| 332 | # Verification parameters |
| 333 | parser.add_argument("--repl_path", default="/workspace/ky_ding/math/minictx-eval/repl", |
| 334 | help="Path to Lean REPL") |
| 335 | parser.add_argument("--lean_env_path", default="/workspace/ky_ding/math/minictx-eval/repl/test/Mathlib", |
| 336 | help="Path to Lean environment") |
| 337 | parser.add_argument("--num_batches", default=96, type=int, |
| 338 | help="Number of parallel verification batches") |
| 339 | |
| 340 | # Timeout parameters |
| 341 | parser.add_argument("--session_timeout", default=600, type=int, |
| 342 | help="Timeout for interactive sessions (in seconds)") |
| 343 | parser.add_argument("--expect_timeout", default=120, type=int, |
| 344 | help="Timeout for the expect command (in seconds)") |
| 345 | |
| 346 | return parser.parse_args() |
| 347 | |
| 348 | def main(): |
| 349 | args = parse_args() |