File size: 649 Bytes
effde1c | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 | """
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}"
|