From 97f62ce75ade2c27577740a4b6b1cdf05a264ff8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Hugues=20de=20Saxc=C3=A9?= Date: Thu, 31 Jul 2025 21:36:42 +0200 Subject: [PATCH 1/4] fix: catch oom --- server/repl.py | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/server/repl.py b/server/repl.py index 7d0c4ca..9da9c03 100644 --- a/server/repl.py +++ b/server/repl.py @@ -32,6 +32,12 @@ log_lock = asyncio.Lock() +class ReplOOMError(ReplError): + """Raised when the REPL exceeds its memory limit.""" + + pass + + async def log_snippet(uuid: UUID, snippet_id: str, code: str) -> None: if settings.environment == Environment.prod: header = f"[{uuid.hex[:8]}] Running snippet {snippet_id}:" @@ -233,6 +239,9 @@ async def send_timeout( except LeanError as e: logger.exception("Lean REPL error: %s", e) raise e + except ReplOOMError as e: + logger.error("[{}] REPL OOM: {}", self.uuid.hex[:8], e) + return ReplResponse(id=snippet.id, error=str(e), time=0.0) except ReplError as e: logger.exception("REPL error: %s", e) raise e @@ -298,6 +307,15 @@ async def send( try: resp: CommandResponse | Error = json.loads(raw) except json.JSONDecodeError: + if self._mem_max >= self.max_memory_bytes: + msg = "Lean REPL process exceeded memory limit" + logger.error( + "[{}] OOM: used {} / {} bytes", + self.uuid.hex[:8], + self._mem_max, + self.max_memory_bytes, + ) + raise ReplOOMError(msg) logger.error("JSON decode error: %r", raw) raise ReplError("JSON decode error") From ae1aeac05a7105a84f6080ddd17146f530ca8314 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Hugues=20de=20Saxc=C3=A9?= Date: Thu, 31 Jul 2025 22:13:19 +0200 Subject: [PATCH 2/4] fix: forward errors to error file --- server/repl.py | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/server/repl.py b/server/repl.py index 9da9c03..997f216 100644 --- a/server/repl.py +++ b/server/repl.py @@ -152,6 +152,9 @@ def _preexec() -> None: os.setsid() + self.error_file.seek(0) + self.error_file.truncate() + self.proc = await asyncio.create_subprocess_exec( "lake", "env", @@ -160,7 +163,7 @@ def _preexec() -> None: env=os.environ, stdin=asyncio.subprocess.PIPE, stdout=asyncio.subprocess.PIPE, - stderr=asyncio.subprocess.PIPE, + stderr=self.error_file, preexec_fn=_preexec, ) From 03c954b04f7fdcc964f18d180eb93549532f0e70 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Hugues=20de=20Saxc=C3=A9?= Date: Sun, 3 Aug 2025 07:25:38 +0200 Subject: [PATCH 3/4] fix: error logs + condition to detect OOM --- server/repl.py | 23 +++++++++++++++-------- 1 file changed, 15 insertions(+), 8 deletions(-) diff --git a/server/repl.py b/server/repl.py index 997f216..80789c2 100644 --- a/server/repl.py +++ b/server/repl.py @@ -81,7 +81,9 @@ def __init__( self.header_cmd_response: ReplResponse | None = None self.proc: Process | None = None - self.error_file = tempfile.TemporaryFile("w+") + self.error_file = tempfile.TemporaryFile( + "w+", encoding="utf-8", errors="ignore" + ) self.max_memory_bytes = max_repl_mem * 1024 * 1024 self.max_repl_uses = max_repl_uses @@ -240,13 +242,13 @@ async def send_timeout( ) raise e except LeanError as e: - logger.exception("Lean REPL error: %s", e) + logger.exception("Lean REPL error: {}", e) raise e except ReplOOMError as e: logger.error("[{}] REPL OOM: {}", self.uuid.hex[:8], e) return ReplResponse(id=snippet.id, error=str(e), time=0.0) except ReplError as e: - logger.exception("REPL error: %s", e) + logger.exception("REPL error: {}", e) raise e return ReplResponse( @@ -299,14 +301,19 @@ async def send( logger.error("Broken pipe while writing to REPL stdin") raise LeanError("Lean process broken pipe") except Exception as e: - logger.error("Failed to write to REPL stdin: %s", e) + logger.error("Failed to write to REPL stdin: {}", e) raise LeanError("Failed to write to REPL stdin") logger.debug("Reading response from REPL stdout") raw = await self._read_response() elapsed = loop.time() - start - logger.debug("Raw response from REPL: %r", raw) + await self.proc.wait() + if self.proc.returncode not in (None, 0): + self.error_file.seek(0) + err = self.error_file.read().strip() or "Lean REPL out of memory" + raise ReplOOMError(err) + logger.debug("Raw response from REPL: {}", raw) try: resp: CommandResponse | Error = json.loads(raw) except json.JSONDecodeError: @@ -319,7 +326,7 @@ async def send( self.max_memory_bytes, ) raise ReplOOMError(msg) - logger.error("JSON decode error: %r", raw) + logger.error("JSON decode error: {}", raw) raise ReplError("JSON decode error") self.error_file.seek(0) @@ -327,7 +334,7 @@ async def send( self.error_file.seek(0) self.error_file.truncate(0) if err: - logger.error("Stderr: %s", err) + logger.error("Stderr: {}", err) raise LeanError(err) elapsed_time = round(elapsed, 6) @@ -357,7 +364,7 @@ async def _read_response(self) -> bytes: break lines.append(chunk) except Exception as e: - logger.error("Failed to read from REPL stdout: %s", e) + logger.error("Failed to read from REPL stdout: {}", e) raise LeanError("Failed to read from REPL stdout") return b"".join(lines) From c22f693fa77441d935a7f392de24326f794f6dff Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Hugues=20de=20Saxc=C3=A9?= Date: Sun, 3 Aug 2025 07:45:49 +0200 Subject: [PATCH 4/4] fix: no await --- server/repl.py | 16 +++++----------- 1 file changed, 5 insertions(+), 11 deletions(-) diff --git a/server/repl.py b/server/repl.py index 80789c2..9a681b6 100644 --- a/server/repl.py +++ b/server/repl.py @@ -308,24 +308,18 @@ async def send( raw = await self._read_response() elapsed = loop.time() - start - await self.proc.wait() if self.proc.returncode not in (None, 0): self.error_file.seek(0) - err = self.error_file.read().strip() or "Lean REPL out of memory" + err = ( + self.error_file.read().strip() + or "Lean REPL died, probably out of memory" + ) raise ReplOOMError(err) + logger.debug("Raw response from REPL: {}", raw) try: resp: CommandResponse | Error = json.loads(raw) except json.JSONDecodeError: - if self._mem_max >= self.max_memory_bytes: - msg = "Lean REPL process exceeded memory limit" - logger.error( - "[{}] OOM: used {} / {} bytes", - self.uuid.hex[:8], - self._mem_max, - self.max_memory_bytes, - ) - raise ReplOOMError(msg) logger.error("JSON decode error: {}", raw) raise ReplError("JSON decode error")