| 17 | |
| 18 | # Interactive thread class |
| 19 | class InteractiveThread(threading.Thread): |
| 20 | def __init__(self, session_id, repl_path, lean_env_path, initial_context=None, |
| 21 | timeout=600, expect_timeout=120): |
| 22 | super().__init__() |
| 23 | self.session_id = session_id |
| 24 | self.repl_path = repl_path |
| 25 | self.lean_env_path = lean_env_path |
| 26 | self.context = initial_context |
| 27 | self.session = None |
| 28 | self.expect_timeout = expect_timeout |
| 29 | |
| 30 | self.cmd_response_condition = threading.Event() |
| 31 | self.cmd_query_condition = threading.Event() |
| 32 | self.init_complete = threading.Event() |
| 33 | self.response = None |
| 34 | |
| 35 | self.stop_flag = False |
| 36 | self.timer = threading.Timer(timeout, self.stop) |
| 37 | |
| 38 | def initialize_check(self): |
| 39 | try: |
| 40 | if self.context == None: |
| 41 | initialize_check = {"cmd": "def init_check : Nat := 42"} |
| 42 | self.send_cmd(initialize_check) |
| 43 | self.session.expect('"env": 0}\r\n\r\n', timeout=self.expect_timeout) # If the context contains 'sorries', it will have more keys other than 'env' |
| 44 | self.init_complete.set() |
| 45 | except: |
| 46 | self.init_complete.set() |
| 47 | print(f"Session {self.session_id}: Failed to initialize Lean REPL") |
| 48 | print(self.context) |
| 49 | print(self.session.before) |
| 50 | self.stop() |
| 51 | |
| 52 | def send_cmd(self, cmd): |
| 53 | cmd_str = json.dumps(cmd, ensure_ascii=False) |
| 54 | self.session.sendline(cmd_str + '\n') |
| 55 | |
| 56 | def submit_and_receive(self, cmd): |
| 57 | if self.stop_flag: |
| 58 | return None |
| 59 | |
| 60 | self.init_complete.wait() |
| 61 | |
| 62 | self.send_cmd(cmd) |
| 63 | |
| 64 | self.cmd_query_condition.set() |
| 65 | |
| 66 | self.cmd_response_condition.wait() # Wait for the response |
| 67 | self.cmd_response_condition.clear() |
| 68 | if self.response: |
| 69 | output = self.response |
| 70 | self.response = None |
| 71 | return output |
| 72 | return None |
| 73 | |
| 74 | def process_responses(self): |
| 75 | while not self.stop_flag: |
| 76 | self.cmd_query_condition.wait() # Wait for input |