From 10d5a7aa761f3f04c12a45efb9acfa5bce653d58 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Fri, 24 Jan 2025 14:36:05 +0100 Subject: [PATCH 1/3] Fix to_sync when no event loop is running. --- pantograph/utils.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pantograph/utils.py b/pantograph/utils.py index 31067a8..d438078 100644 --- a/pantograph/utils.py +++ b/pantograph/utils.py @@ -13,7 +13,7 @@ def to_sync(func): @F.wraps(func) def wrapper(*args, **kwargs): - return asyncio.get_event_loop().run_until_complete(func(*args, **kwargs)) + return asyncio.run(func(*args, **kwargs)) return wrapper async def check_output(*args, **kwargs): From e2d2cc15dff3d82a4bfa66ef830940e6609f3ba1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Fri, 24 Jan 2025 14:36:49 +0100 Subject: [PATCH 2/3] Fix random freezing of pexpect.spawn.expect(). --- pantograph/utils.py | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/pantograph/utils.py b/pantograph/utils.py index d438078..104af6e 100644 --- a/pantograph/utils.py +++ b/pantograph/utils.py @@ -83,6 +83,8 @@ async def readline_async(self, size=-1): This looks for a newline as a CR/LF pair (\\r\\n) even on UNIX because this is what the pseudotty device returns. So contrary to what you may expect you will receive newlines as \\r\\n. + See https://pexpect.readthedocs.io/en/latest/overview.html#find-the-end-of-line-cr-lf-conventions + for more information. If the size argument is 0 then an empty string is returned. In all other cases the size argument is ignored, which is not standard @@ -90,8 +92,13 @@ async def readline_async(self, size=-1): if size == 0: return self.string_type() - # delimiter default is EOF - index = await self.expect([self.crlf, self.delimiter], async_=True) + + def blocking_expect(): + # We use `asyncio.to_thread` because passing `async_=True` to `expect()` sometimes hangs. See e.g.: + # https://stackoverflow.com/questions/12647212/why-is-pexpect-intermittently-hanging-not-detecting-eof-after-executing-certai + return self.expect([self.crlf, self.delimiter]) + + index = await asyncio.to_thread(blocking_expect) if index == 0: return self.before + self.crlf else: From b7284cf560314107a3aeb64b036a2d65c7754d9e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Fri, 24 Jan 2025 14:37:19 +0100 Subject: [PATCH 3/3] Quality of life improvements in server. --- pantograph/server.py | 26 +++++++++++++++++--------- 1 file changed, 17 insertions(+), 9 deletions(-) diff --git a/pantograph/server.py b/pantograph/server.py index 981e8ce..0b6a549 100644 --- a/pantograph/server.py +++ b/pantograph/server.py @@ -54,11 +54,11 @@ def __init__(self, # Set `{ "automaticMode" : False }` to handle resumption by yourself. options: Dict[str, Any]={}, core_options: List[str]=DEFAULT_CORE_OPTIONS, - timeout: int=120, + timeout: int=30, maxread: int=1000000, _sync_init: bool=True): """ - timeout: Amount of time to wait for execution + timeout: Amount of time to wait for execution (in seconds) maxread: Maximum number of characters to read (especially important for large proofs and catalogs) """ self.timeout = timeout @@ -93,7 +93,7 @@ async def create(cls, maxread: int=1000000, start:bool=True) -> 'Server': """ - timeout: Amount of time to wait for execution + timeout: Amount of time to wait for execution (in seconds) maxread: Maximum number of characters to read (especially important for large proofs and catalogs) """ self = cls( @@ -163,19 +163,19 @@ async def restart_async(self): raise RuntimeError("Server failed to emit ready signal in time") from exc if self.options: - await self.run_async("options.set", self.options) + await self.run_async("options.set", self.options, assert_no_error=True) - await self.run_async('options.set', {'printDependentMVars': True}) + await self.run_async('options.set', {'printDependentMVars': True}, assert_no_error=True) restart = to_sync(restart_async) - async def run_async(self, cmd, payload): + async def run_async(self, cmd, payload, assert_no_error=False): """ Runs a raw JSON command. Preferably use one of the commands below. :meta private: """ - assert self.proc + assert self.proc, "Server not running." s = json.dumps(payload, ensure_ascii=False) await self.proc.sendline_async(f"{cmd} {s}") try: @@ -185,15 +185,23 @@ async def run_async(self, cmd, payload): if obj.get("error") == "io": # The server is dead self._close() + if "error" in obj and assert_no_error: + raise ServerError(obj) return obj except Exception as e: + if self.proc.closed: + raise ServerError(f"Cannot decode: '{line}'") from e self.proc.sendeof() remainder = await self.proc.read_async() self._close() - raise ServerError(f"Cannot decode: {line}\n{remainder}") from e + raise ServerError(f"Cannot decode: '{line}\n{remainder}'") from e except pexpect.exceptions.TIMEOUT as exc: self._close() - return {"error": "timeout", "message": str(exc)} + result = {"error": "timeout", "message": str(exc)} + if assert_no_error: + raise ServerError(result) from exc + else: + return result run = to_sync(run_async)