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