| """ | |
| Adapter for running Lean 4 proofs from Python. | |
| """ | |
| import subprocess | |
| import os | |
| def run_lean4(input_file: str, lean_dir: str = "external/lean4") -> str: | |
| """ | |
| Runs Lean 4 on the given input file and returns the output as a string. | |
| """ | |
| exe_path = os.path.join(lean_dir, "bin", "lean") | |
| if not os.path.exists(exe_path): | |
| raise FileNotFoundError(f"Lean 4 not found at {exe_path}") | |
| try: | |
| result = subprocess.run([ | |
| exe_path, input_file | |
| ], capture_output=True, text=True, check=True) | |
| return result.stdout | |
| except Exception as e: | |
| return f"Lean 4 error: {e}" | |