import os
import subprocess
import json
import time
from concurrent.futures import ThreadPoolExecutor, as_completed
import sys

HOME_DIR = os.path.expanduser('~')
DEFAULT_LAKE_PATH = f'{HOME_DIR}/.elan/bin/lake'
DEFAULT_LEAN_WORKSPACE = 'TestLean'

def process_command(process, command):

    print(command)
        
    json_input = json.dumps(command, ensure_ascii=False) + "\n\n"
    process.stdin.write(json_input)
    process.stdin.flush()
    
    
    output_lines = []
    while True:
        line = process.stdout.readline().strip()
        if not line:
            break
        output_lines.append(line)

    print(output_lines)

    return "\n".join(output_lines)

def process_commands(commands):

    process = subprocess.Popen(
            [DEFAULT_LAKE_PATH, "exe", "repl"],
            stdin=subprocess.PIPE,
            stdout=subprocess.PIPE,
            stderr=subprocess.PIPE,
            cwd=DEFAULT_LEAN_WORKSPACE,
            text=True,
            bufsize=1,
            env=os.environ,
            preexec_fn=os.setsid if sys.platform != 'win32' else None,
        )
    
    for command in commands:
        process_command(process, command)
    
    print("closing repl ... ")

    process.stdin.close()
    process.wait()

start_time = time.time()

commands = [{"cmd": f"theorem womp{i} (a{i} b c : Nat) : (a{i} + b) + c = c + a{i} + b := by sorry"} for i in range(1000)]

process_commands(commands)

end_time = time.time()



# Print results if needed
# print("\n".join(results))
print(f"Execution Time: {end_time - start_time}")

...
{'cmd': 'theorem womp161 (a161 b c : Nat) : (a161 + b) + c = c + a161 + b := by sorry'}
['{"sorries":', '[{"proofState": 161,', '"pos": {"line": 1, "column": 71},', '"goal": "a161 b c : Nat\\n⊢ a161 + b + c = c + a161 + b",', '"endPos": {"line": 1, "column": 76}}],', '"messages":', '[{"severity": "warning",', '"pos": {"line": 1, "column": 8},', '"endPos": {"line": 1, "column": 15},', '"data": "declaration uses \'sorry\'"}],', '"env": 161}']
{'cmd': 'theorem womp162 (a162 b c : Nat) : (a162 + b) + c = c + a162 + b := by sorry'}
['{"sorries":', '[{"proofState": 162,', '"pos": {"line": 1, "column": 71},', '"goal": "a162 b c : Nat\\n⊢ a162 + b + c = c + a162 + b",', '"endPos": {"line": 1, "column": 76}}],', '"messages":', '[{"severity": "warning",', '"pos": {"line": 1, "column": 8},', '"endPos": {"line": 1, "column": 15},', '"data": "declaration uses \'sorry\'"}],', '"env": 162}']
{'cmd': 'theorem womp163 (a163 b c : Nat) : (a163 + b) + c = c + a163 + b := by sorry'}
[]
{'cmd': 'theorem womp164 (a164 b c : Nat) : (a164 + b) + c = c + a164 + b := by sorry'}
Traceback (most recent call last):
  File "C:\Users\pufre\Downloads\CodingProjects\TinyProof\solver\batch_verifier1.py", line 58, in <module>
    process_commands(commands)
  File "C:\Users\pufre\Downloads\CodingProjects\TinyProof\solver\batch_verifier1.py", line 47, in process_commands
    process_command(process, command)
  File "C:\Users\pufre\Downloads\CodingProjects\TinyProof\solver\batch_verifier1.py", line 17, in process_command
    process.stdin.write(json_input)
OSError: [Errno 22] Invalid argument