Address non-happy paths

src/lean_client/commands.py

@@ -35,8 +35,8 @@ class Response:
 
     @classmethod
     def from_dict(cls, dic):
-        if 'message' in dic and cls != ErrorResponse:
-            dic.pop('message') # This is a hack for "file invalidated" messages
+        if 'message' in dic and cls != ErrorResponse and cls != SyncResponse:
+            dic.pop('message')  # TODO (jasonrute): Is this hack needed anymore?
         return cls(**dic)
 
 Severity = Enum('Severity', 'information warning error')
@@ -103,6 +103,13 @@ class ErrorResponse(Response):
     seq_num: Optional[int] = None
 
 
+@dataclass
+class SyncResponse(Response):
+    response = 'ok'
+    message: str
+    seq_num: Optional[int] = None
+
+
 @dataclass
 class SyncRequest(Request):
     command = 'sync'
@@ -161,8 +168,8 @@ class InfoRequest(Request):
 
 @dataclass
 class InfoSource:
-    line: int
-    column: int
+    line: int = None
+    column: int = None
     file: Optional[str] = None
 
 
@@ -385,6 +392,8 @@ def parse_response(data: str) -> Response:
             return AllHoleCommandsResponse.from_dict(dic)
         elif 'replacements' in dic:
             return HoleResponse.from_dict(dic)
+        elif 'message' in dic and dic['message'] in ["file invalidated", "file unchanged"]:
+            return SyncResponse.from_dict(dic)
 
 
     # Now try classes for messages that do have a helpful response field

src/lean_client/trio_server.py

@@ -12,12 +12,12 @@
 import trio # type: ignore
 
 from lean_client.commands import (parse_response, SyncRequest, InfoRequest,
-        Request, CommandResponse, Message, Task, Response,
+        Request, CommandResponse, Message, Task, Response, SyncResponse, ErrorResponse,
         InfoResponse, AllMessagesResponse, Severity, CurrentTasksResponse)
 
 
 class TrioLeanServer:
-    def __init__(self, nursery, lean_cmd: str = 'lean', debug=False):
+    def __init__(self, nursery, lean_cmd: str = 'lean', debug=False, debug_bytes=False):
         """
         Lean server trio interface.
         """
@@ -28,6 +28,7 @@ def __init__(self, nursery, lean_cmd: str = 'lean', debug=False):
         self.current_tasks: List[Task] = []
         self.process: Optional[trio.Process] = None
         self.debug: bool = debug
+        self.debug_bytes: bool = debug_bytes
         # Each request, with sequence number seq_num, gets an event
         # self.response_events[seq_num] that it set when the response comes in
         self.response_events: Dict[int, trio.Event] = dict()
@@ -49,6 +50,9 @@ async def send(self, request: Request) -> Response:
         self.response_events[self.seq_num] = trio.Event()
         if self.debug:
             print(f'Sending {request}')
+        if self.debug_bytes:
+            bytes = (request.to_json() + '\n').encode()
+            print(f'Sending {bytes}')
         await self.process.stdin.send_all((request.to_json()+'\n').encode())
         await self.response_events[request.seq_num].wait()
         self.response_events.pop(request.seq_num)
@@ -59,9 +63,14 @@ async def receiver(self):
         (tasks and messages) and triggering events when a response comes."""
         if not self.process:
             raise ValueError('No Lean server')
+        unfinished_message = b''
         async for data in self.process.stdout:
-            for line in data.decode().strip().split('\n'):
-                resp = parse_response(line)
+            lines = (unfinished_message + data).split(b'\n')
+            unfinished_message = lines.pop()  # usually empty, but can be half a message
+            for line in lines:
+                if self.debug_bytes:
+                    print(f'Received {line}')
+                resp = parse_response(line.decode())
                 if self.debug:
                     print(f'Received {resp}')
                 if isinstance(resp, CurrentTasksResponse):
@@ -77,9 +86,13 @@ async def receiver(self):
     async def full_sync(self, filename, content=None) -> None:
         """Fully compile a Lean file before returning."""
         # Waiting for the response is not enough, so we prepare another event
-        await self.send(SyncRequest(filename, content))
-        self.is_fully_ready = trio.Event()
-        await self.is_fully_ready.wait()
+        resp = await self.send(SyncRequest(filename, content))
+
+        if isinstance(resp, SyncResponse) and resp.message == "file invalidated":
+            self.is_fully_ready = trio.Event()
+            await self.is_fully_ready.wait()
+        elif isinstance(resp, ErrorResponse):
+            raise ValueError(f"Lean error during syncing:\n{resp}")  # TODO(jasonrute): this should be a better error type
 
     async def state(self, filename, line, col) -> str:
         """Tactic state"""

test/test_trio_server/mock_lean.py

@@ -0,0 +1,152 @@
+"""
+This makes it possible to have tests for the Lean Python server
+interface which do not depend on having Lean installed in a certain manner.
+
+Instead one can build a "lean script" which is run by a fake lean server.
+"""
+
+import trio  # type: ignore
+from typing import List, Dict
+import json
+from collections import deque
+from dataclasses import dataclass
+import trio.testing
+
+from lean_client.trio_server import TrioLeanServer
+
+
+class LeanScriptStep:
+    pass
+
+
+@dataclass
+class LeanTakesTime(LeanScriptStep):
+    """
+    Simulate taking a while to start up or processes a request.
+    """
+    seconds: float
+
+
+@dataclass
+class LeanShouldGetRequest(LeanScriptStep):
+    """
+    Used to check that Lean gets the request it is looking for from Lean-Python interface.
+    """
+    message: Dict  # should be JSON encodable
+
+
+@dataclass
+class LeanSendsResponse(LeanScriptStep):
+    """
+    Simulate Lean's output behaviour
+    """
+    message: Dict  # should be JSON encodable
+
+
+@dataclass
+class LeanSendsBytes(LeanScriptStep):
+    """
+    Simulate Lean's output behaviour at the byte level.
+    Doesn't include new line characters unless passed in.
+    """
+    message_bytes: bytes
+
+
+@dataclass
+class LeanShouldNotGetRequest(LeanScriptStep):
+    """
+    Check that Lean has not received any requests (perhaps sent prematurely).
+    """
+    pass
+
+
+
+class MockLeanServerProcess(trio.Process):
+
+    def __init__(self, script: List[LeanScriptStep]):
+        self.stdin = trio.testing.MemorySendStream()      # a stream for mock lean to read from
+        self.stdout = trio.testing.MemoryReceiveStream()  # a stream for mock lean to write to
+        self.messages: deque[Dict] = deque()
+        self.partial_message: bytes = b""
+        self.script: List[LeanScriptStep] = script
+
+    def kill(self):
+        pass
+
+    @staticmethod
+    def parse_message(b: bytes) -> Dict:
+        return json.loads(b.decode())
+
+    @staticmethod
+    def messages_are_equal(m1: Dict, m2: Dict):
+        s1 = json.dumps(m1, sort_keys=True)
+        s2 = json.dumps(m2, sort_keys=True)
+        return s1 == s2
+
+    def collect_stdin_messages(self):
+        try:
+            data = self.stdin.get_data_nowait()
+        except trio.WouldBlock:  # no data
+            return
+
+        raw_messages = (self.partial_message + data).split(b"\n")
+        self.partial_message = raw_messages.pop()
+        self.messages.extend(self.parse_message(m) for m in raw_messages)
+
+    async def assert_message_is_received(self, message_expected):
+        await trio.sleep(0.01)
+        self.collect_stdin_messages()
+
+        assert self.messages, f"Mock Lean was expecting\n{message_expected}\nbut no messages were received."
+
+        message_received = self.messages.pop()
+        assert self.messages_are_equal(message_expected, message_received), \
+            f"Mock Lean was expecting\n{message_expected}\nbut received\n{message_received}"
+
+    async def assert_no_messages_received(self):
+        await trio.sleep(0.01)
+        self.collect_stdin_messages()
+
+        assert not self.messages, f"Mock Lean was not expecting as message, but \n{self.messages[0]}\nwas received."
+
+    def send_bytes(self, message_bytes: bytes):
+        self.stdout.put_data(message_bytes)
+
+    def send_message(self, message):
+        message_bytes = json.dumps(message).encode() + b"\n"
+        self.stdout.put_data(message_bytes)
+
+    async def follow_script(self):
+        for step in self.script:
+            if isinstance(step, LeanTakesTime):
+                print(f"\nLean is taking {step.seconds} seconds before doing anything.")
+                await trio.sleep(step.seconds)
+            elif isinstance(step, LeanShouldGetRequest):
+                print(f"\nLean should receive the following request:\n{step.message}")
+                await self.assert_message_is_received(step.message)
+            elif isinstance(step, LeanSendsResponse):
+                print(f"\nLean sends the following response:\n{step.message}")
+                self.send_message(step.message)
+            elif isinstance(step, LeanSendsBytes):
+                print(f"\nLean sends the following bytes:\n{step.message_bytes}")
+                self.send_bytes(step.message_bytes)
+            elif isinstance(step, LeanShouldNotGetRequest):
+                print(f"\nLean should not have received any requests yet.")
+                await self.assert_no_messages_received()
+
+
+async def start_with_mock_lean(lean_server: TrioLeanServer, script: List[LeanScriptStep]):
+    """
+    Call this in place of TrioLeanServer.start().  It will run a mock Lean server following the script,
+    in place of the real Lean server.
+    """
+
+    # start up the mock lean process
+    mock_lean_process = MockLeanServerProcess(script)
+    lean_server.nursery.start_soon(mock_lean_process.follow_script)
+
+    # attach to the lean interface
+    lean_server.process = mock_lean_process
+
+    # perform the remainder of the start up processes as normal
+    lean_server.nursery.start_soon(lean_server.receiver)

test/test_trio_server/test_full_sync.py

@@ -0,0 +1,118 @@
+from test.test_trio_server.mock_lean import \
+    LeanShouldGetRequest, LeanShouldNotGetRequest, LeanTakesTime, LeanSendsResponse, start_with_mock_lean
+from lean_client.trio_server import TrioLeanServer
+import trio
+import trio.testing
+
+
+def test_full_sync_waits_until_lean_ready():
+    """
+    Check that full_sync waits until the Lean server is ready.
+    In particular, it must first get a "file invalidated" response, and then an "all_tasks" response
+    before continuing.
+    """
+    mock_lean_script = [
+        LeanShouldGetRequest({"file_name": "test.lean", "content": '--', "seq_num": 1, "command": "sync"}),
+
+        # current_tasks response is sent BEFORE the ok response
+        LeanSendsResponse({"is_running": False, "response": "current_tasks", "tasks": []}),
+        LeanSendsResponse({"message": "file invalidated", "response": "ok", "seq_num": 1}),
+
+        # shouldn't be receiving anything yet
+        LeanShouldNotGetRequest(),
+
+        LeanSendsResponse({"is_running": False, "response": "current_tasks", "tasks": []}),
+
+        # now it is ok to get a new request
+        LeanShouldGetRequest({"file_name": "test.lean", "line": 1, "column": 0, "seq_num": 2, "command": "info"}),
+        LeanSendsResponse({"response": "ok", "seq_num": 2}),
+    ]
+
+    async def check_waiting_behavior():
+        async with trio.open_nursery() as nursery:
+            server = TrioLeanServer(nursery)
+            await start_with_mock_lean(server, mock_lean_script)
+
+            await server.full_sync('test.lean', content='--')
+            await server.state(filename="test.lean", line=1, col=0)
+
+            nursery.cancel_scope.cancel()
+
+    trio.run(check_waiting_behavior)
+
+
+def test_syncing_same_file_again():
+    """
+    If the same file is synced with no changes, then Lean won't send the same sort of responses.
+    """
+
+    mock_lean_script = [
+        # initial sync
+        LeanShouldGetRequest({"file_name": "test.lean", "seq_num": 1, "command": "sync"}),
+        LeanSendsResponse({"message": "file invalidated", "response": "ok", "seq_num": 1}),
+        LeanTakesTime(.01),
+        LeanSendsResponse({"is_running": False, "response": "current_tasks", "tasks": []}),
+
+        # sync same file again which hasn't changed.  Lean WON'T send a current_tasks response
+        LeanShouldGetRequest({"file_name": "test.lean", "seq_num": 2, "command": "sync"}),
+        LeanSendsResponse({"message": "file unchanged", "response": "ok", "seq_num": 2}),
+        LeanTakesTime(.01),
+
+        # The python-lean interface should not block and instead send an info request right away
+        LeanShouldGetRequest({"file_name": "test.lean", "line": 1, "column": 0, "seq_num": 3, "command": "info"}),
+        LeanSendsResponse({"response": "ok", "seq_num": 3}),
+    ]
+
+    async def check_behavior():
+        async with trio.open_nursery() as nursery:
+            server = TrioLeanServer(nursery)
+            await start_with_mock_lean(server, mock_lean_script)
+
+            await server.full_sync("test.lean")
+            await server.full_sync("test.lean")  # sync same file twice
+
+            await server.state(filename="test.lean", line=1, col=0)
+
+            nursery.cancel_scope.cancel()
+
+    trio.run(check_behavior)
+
+
+def test_error_in_sync():
+    """
+    If there is an error in syncing (such as the file not existing), then one shouldn't wait
+    for a current_tasks response.
+    """
+
+    mock_lean_script = [
+        # initial sync
+        LeanShouldGetRequest({"file_name": "bad_file_name", "seq_num": 1, "command": "sync"}),
+        LeanSendsResponse({"message": "file 'bad_file_name' not found in the LEAN_PATH", "response": "error", "seq_num": 1}),
+        LeanTakesTime(.01),
+
+        # the lean process should throw an error (which will be caught and handled)
+
+        # If this part fails, that means the interface blocked waiting for a current_tasks response
+        LeanShouldGetRequest({"file_name": "test.lean", "seq_num": 2, "command": "sync"}),
+        LeanSendsResponse({"message": "file unchanged", "response": "ok", "seq_num": 2}),
+        LeanTakesTime(.01),
+        LeanSendsResponse({"is_running": False, "response": "current_tasks", "tasks": []}),
+    ]
+
+    async def check_behavior():
+        async with trio.open_nursery() as nursery:
+            server = TrioLeanServer(nursery)
+            await start_with_mock_lean(server, mock_lean_script)
+
+            # for this test to pass it has to (1) not block forever and (2) throw an error
+            try:
+                await server.full_sync("bad_file_name")
+                assert False, "An error should have been thrown here"
+            except ValueError:
+                pass
+
+            await server.full_sync("test.lean")  # sync a different file
+
+            nursery.cancel_scope.cancel()
+
+    trio.run(check_behavior)