v2.1.3

Author: yangky11

src/lean_dojo/interaction/Lean4Repl.lean

@@ -248,9 +248,9 @@ end TacticRepl
 
 
 private def loop (m : Type → Type) [Monad m] [MonadLift IO m] [MonadError m] (handler : Request → m Response) : m Unit := do
-  while true do
-    let line ← (← IO.getStdin).getLine
-    if line.trim == "exit" then
+ while true do
+    let line := (← (← IO.getStdin).getLine).trim
+    if line == "exit" then
       break
     match (Json.parse line) with
     | .error err => throwError s!"[fatal] failed to parse JSON {err}"

src/lean_dojo/interaction/dojo.py

@@ -392,7 +392,7 @@ def _check_alive(self) -> None:
         if exit_code == 137:
             raise DojoCrashError("OOM")
         else:
-            raise DojoCrashError(f"Unknown exit code: {exit_code}")
+            raise DojoCrashError(f"Unexpected exit code: {exit_code}")
 
     def _read_next_line(self) -> Tuple[str, str]:
         """Read the next line from `self.proc`.