| """ | |
| Adapter for running Coq proofs from Python. | |
| """ | |
| import subprocess | |
| import os | |
| def run_coq(input_file: str, coq_dir: str = "external/coq-platform") -> str: | |
| """ | |
| Runs Coq on the given input file and returns the output as a string. | |
| """ | |
| exe_path = os.path.join(coq_dir, "bin", "coqc") | |
| if not os.path.exists(exe_path): | |
| raise FileNotFoundError(f"Coq 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"Coq error: {e}" | |