diff --git a/servers/lean_client.py b/servers/lean_client.py index 2363a3c8a..c1f1df638 100644 --- a/servers/lean_client.py +++ b/servers/lean_client.py @@ -30,18 +30,20 @@ INSTALL_PATH_ID = hashlib.sha256(os.fsencode(PACKAGE_ROOT)).hexdigest()[:10] +# Code whose changes require replacing a live runtime daemon. +_RUNTIME_SOURCES = ( + Path(__file__).resolve(), + PACKAGE_ROOT / "servers" / "lean_runtime.py", + PACKAGE_ROOT / "servers" / "lsp" / "server.py", + PACKAGE_ROOT / "servers" / "repl" / "core.py", + PACKAGE_ROOT / "servers" / "repl" / "pool.py", +) + + def _build_id() -> str: """Fingerprint code that can change persistent runtime behavior.""" digest = hashlib.sha256() - runtime_files = ( - PACKAGE_ROOT / "servers" / "__init__.py", - Path(__file__).resolve(), - PACKAGE_ROOT / "servers" / "lean_runtime.py", - PACKAGE_ROOT / "servers" / "lsp" / "server.py", - PACKAGE_ROOT / "servers" / "repl" / "core.py", - PACKAGE_ROOT / "servers" / "repl" / "pool.py", - ) - for path in runtime_files: + for path in (PACKAGE_ROOT / "servers" / "__init__.py", *_RUNTIME_SOURCES): try: digest.update(path.read_bytes()) except OSError: @@ -51,15 +53,8 @@ def _build_id() -> str: def _build_generation() -> int: """Order in-place builds so an older live wrapper cannot replace a newer one.""" - candidates = ( - Path(__file__).resolve(), - PACKAGE_ROOT / "servers" / "lean_runtime.py", - PACKAGE_ROOT / "servers" / "lsp" / "server.py", - PACKAGE_ROOT / "servers" / "repl" / "core.py", - PACKAGE_ROOT / "servers" / "repl" / "pool.py", - ) mtimes: list[int] = [] - for path in candidates: + for path in _RUNTIME_SOURCES: try: mtimes.append(path.stat().st_mtime_ns) except OSError: @@ -463,7 +458,6 @@ def _request_once( raise LeanRuntimeProtocolError("Lean runtime request exceeds the message limit") connection = socket.socket(socket.AF_UNIX, socket.SOCK_STREAM) - dispatched = False try: connection.settimeout(self.connect_timeout) try: @@ -473,36 +467,30 @@ def _request_once( f"Lean runtime is not listening at {self.paths.socket}" ) from error except OSError as error: - if error.errno in {2, 61, 111}: - raise LeanRuntimeUnavailable( - f"Lean runtime is not listening at {self.paths.socket}" - ) from error raise LeanRuntimeError(f"cannot connect to Lean runtime: {error}") from error connection.settimeout(response_timeout or self.response_timeout) # From this point onward, any failure is ambiguous: the daemon may # have received the request. Never auto-replay Lean execution. - dispatched = True - connection.sendall(payload) - raw = self._read_line(connection) - except socket.timeout as error: - phase = "response" if dispatched else "connection" - raise LeanRuntimeError(f"timed out waiting for Lean runtime {phase}") from error - except LeanRuntimeError: - raise - except OSError as error: - if not dispatched: - raise LeanRuntimeUnavailable( - f"Lean runtime is not listening at {self.paths.socket}" + try: + connection.sendall(payload) + raw = self._read_line(connection) + except socket.timeout as error: + raise LeanRuntimeError("timed out waiting for Lean runtime response") from error + except OSError as error: + raise LeanRuntimeError( + "connection to Lean runtime closed after request dispatch; the request was not retried" ) from error - raise LeanRuntimeError( - "connection to Lean runtime closed after request dispatch; the request was not retried" + except OSError as error: + # Only settimeout() reaches here; nothing has been sent yet. + raise LeanRuntimeUnavailable( + f"Lean runtime is not listening at {self.paths.socket}" ) from error finally: connection.close() try: - response = json.loads(raw) + response = json.loads(raw.decode("utf-8")) except (UnicodeDecodeError, json.JSONDecodeError) as error: raise LeanRuntimeProtocolError("Lean runtime returned invalid JSON") from error if not isinstance(response, dict): @@ -523,7 +511,7 @@ def _request_once( raise LeanRuntimeRemoteError(f"{error_type}: {message}") @staticmethod - def _read_line(connection: socket.socket) -> str: + def _read_line(connection: socket.socket) -> bytes: data = bytearray() while len(data) <= MAX_MESSAGE_BYTES: chunk = connection.recv(min(65536, MAX_MESSAGE_BYTES + 1 - len(data))) @@ -534,5 +522,5 @@ def _read_line(connection: socket.socket) -> str: if newline >= 0: if data[newline + 1 :]: raise LeanRuntimeProtocolError("Lean runtime returned trailing response data") - return bytes(data[:newline]).decode("utf-8") + return bytes(data[:newline]) raise LeanRuntimeProtocolError("Lean runtime response exceeds the message limit") diff --git a/tests/test_shared_lean_runtime.py b/tests/test_shared_lean_runtime.py index 18029355c..ebbc0a69c 100644 --- a/tests/test_shared_lean_runtime.py +++ b/tests/test_shared_lean_runtime.py @@ -886,6 +886,63 @@ def close(self): client.request("repl.run", {"project_dir": "/lean", "code": "#check Nat"}) +def test_non_utf8_response_is_a_protocol_error(runtime_dir, monkeypatch): + from servers import lean_client + + class NonUtf8Socket: + def settimeout(self, timeout): + pass + + def connect(self, path): + pass + + def sendall(self, payload): + pass + + def recv(self, size): + return b"\xff\n" + + def close(self): + pass + + client = LeanRuntimeClient(socket_path=runtime_dir / "fake.sock") + monkeypatch.setattr(lean_client.socket, "socket", lambda *args: NonUtf8Socket()) + + with pytest.raises(lean_client.LeanRuntimeProtocolError, match="invalid JSON"): + client.request("repl.run", {"project_dir": "/lean", "code": "#check Nat"}) + + +def test_response_timeout_is_never_retried(runtime_dir, monkeypatch): + from servers import lean_client + + class TimeoutSocket: + def settimeout(self, timeout): + pass + + def connect(self, path): + pass + + def sendall(self, payload): + pass + + def recv(self, size): + raise socket.timeout + + def close(self): + pass + + client = LeanRuntimeClient(socket_path=runtime_dir / "fake.sock") + monkeypatch.setattr(lean_client.socket, "socket", lambda *args: TimeoutSocket()) + monkeypatch.setattr( + client, + "ensure_running", + lambda: pytest.fail("an ambiguously dispatched request must not be retried"), + ) + + with pytest.raises(LeanRuntimeError, match="timed out waiting for Lean runtime response"): + client.request("repl.run", {"project_dir": "/lean", "code": "#check Nat"}) + + @pytest.mark.parametrize( ("name", "value", "match"), [