LeanRepl terminates trying to run large amounts of commands on a single LeanRepl instance

When I run the following python script

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}")

I get the following error.

...
{'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

Even when I modify the runCommands function to not save snapshots it still gives the same error.

Reproduce the failure with the Python script in the issue, which sends 1,000 commands to one LeanRepl process. Start by inspecting the runCommands function and its snapshot-saving behavior. Done means the REPL can process the reported command volume without terminating or causing the writer to raise OSError 22.