Decreasing Performance

[todbeibrot]

Hi, I have some problems with decreasing performance. Each usage of "run_tac" seems to slow down the usage of further "run_tac"s. At the end is a python file to show the behavior: it repeats (init_search, 2000x run_tac, clear_search) and takes 15s, 17s, 19s, 21s, ... Is there a way around it or should I just reopen lean-gym periodically?

import time
import subprocess
import os
import json

lean_gym_path = os.path.dirname(os.path.realpath(__file__))
lean_gym = subprocess.Popen(['lean', '--run', 'src/repl.lean'],
                            cwd=lean_gym_path,
                            stdin=subprocess.PIPE,
                            stdout=subprocess.PIPE)

def run_lean_cmd(cmd: str):
    lean_gym.stdin.write(cmd.encode('utf-8'))
    lean_gym.stdin.flush()
    return json.loads(lean_gym.stdout.readline().decode('utf-8'))

def init_search(decl: str) -> dict:
    cmd = f'["init_search", ["{decl}", ""]]\n'
    return run_lean_cmd(cmd)

def run_tac(search_id: int, tactic_state_id: int, tactic: str) -> dict:
    cmd = f'["run_tac",["{search_id}","{tactic_state_id}","{tactic}"]]\n'
    return run_lean_cmd(cmd)

def clear_search(search_id: int) -> dict:
    cmd = f'["clear_search",["{search_id}"]]\n'
    return run_lean_cmd(cmd)

t1 = time.time()
for i in range(10000):
    t2 = time.time()
    if i > 1:
        print(t2 - t1)
    t1 = t2

    result = init_search('nat.mul_left_eq_self_iff')
    search_id = int(result['search_id'])
    state_id = int(result['tactic_state_id'])

    result = run_tac(search_id, state_id, 'intros')
    search_id = int(result['search_id'])
    state_id = int(result['tactic_state_id'])

    for state_id in range(1000):
        search_id = int(result['search_id'])
        state_id = int(result['tactic_state_id'])
        result = run_tac(search_id, state_id, 'rw mul_comm')

    clear_search(search_id)

[fzyzcjy]

Hi, did you solve it? Thanks

[todbeibrot]

Sadly no. I just reopen it regularly. I also don't have any idea what is causing this behavior

[fzyzcjy]

Thank you all the same :/