Merge pull request #16 from inpefess/cancel-and-shutdown

Cancel and shutdown

doc/source/conf.py

@@ -34,7 +34,7 @@
 author = "Boris Shminke"
 
 # The full version, including alpha/beta/rc tags
-release = "0.1.0"
+release = "0.1.1"
 
 
 # -- General configuration ---------------------------------------------------

doc/source/usage-example.rst

@@ -37,7 +37,9 @@ It might be useful to log all replies from the server somewhere, e.g.::
 
 This client has several methods implemented to communicate with the server Python-style, e.g.::
 
-  isabelle.use_theories(theories=["dummy"], master_dir=".")
+  isabelle.use_theories(theories=["Dummy"], master_dir=".")
+
+In this command it's supposed that we have a ``Dummy.thy`` theory file in our working directory which we, e.g. generated with another Python script.
 
 One can also issue a free-form command, e.g.::
 

isabelle_client/isabelle_client.py

@@ -62,12 +62,12 @@ def execute_command(
         ...     patch("socket.socket.send", send),
         ...     patch("isabelle_client.isabelle_client.get_final_message", res)
         ... ):
-        ...    response = isabelle_client.execute_command("test", "test")
-        >>> print(response.response_type)
+        ...    test_response = isabelle_client.execute_command("test")
+        >>> print(test_response.response_type)
         FINISHED
-        >>> print(response.response_body)
+        >>> print(test_response.response_body)
         {"session_id": "session_id__42"}
-        >>> print(response.response_length)
+        >>> print(test_response.response_length)
         42
         >>> print(connect.mock_calls)
         [call(('localhost', 1000))]
@@ -113,7 +113,7 @@ def session_start(self, session_image: str = "HOL") -> str:
             ...
         ValueError: Unexpected response type: OK
 
-        :param session: a name of a session image
+        :param session_image: a name of a session image
         :returns: a ``session_id``
         """
         arguments = json.dumps({"session": session_image})
@@ -131,15 +131,16 @@ def session_stop(self, session_id: str) -> IsabelleResponse:
         >>> isabelle_client.execute_command = Mock(
         ...     return_value=IsabelleResponse("FAILED", "")
         ... )
-        >>> response = isabelle_client.session_stop("test")
-        >>> print(response.response_type)
+        >>> test_response = isabelle_client.session_stop("test")
+        >>> print(test_response.response_type)
         FAILED
 
         :param session_id: a string ID of a session
         :returns: ``isabelle`` server response
         """
         arguments = json.dumps({"session_id": session_id})
-        return self.execute_command(f"session_stop {arguments}")
+        response = self.execute_command(f"session_stop {arguments}")
+        return response
 
     def use_theories(
         self,
@@ -157,10 +158,10 @@ def use_theories(
         ...         "FINISHED", '{"session_id": "test"}'
         ...     )
         ... )
-        >>> response = isabelle_client.use_theories(
+        >>> test_response = isabelle_client.use_theories(
         ...     ["test"], master_dir="test"
         ... )
-        >>> print(response.response_type)
+        >>> print(test_response.response_type)
         FINISHED
 
         :param theories: names of theory files (without extensions!)
@@ -196,8 +197,8 @@ def echo(self, message: str) -> IsabelleResponse:
         ...         "OK", json.dumps("test message")
         ...     )
         ... )
-        >>> response = isabelle_client.echo("test_message")
-        >>> print(response.response_body)
+        >>> test_response = isabelle_client.echo("test_message")
+        >>> print(test_response.response_body)
         "test message"
 
         :param message: any text
@@ -219,8 +220,8 @@ def help(self) -> IsabelleResponse:
         ...         "OK", json.dumps(["help", "echo"])
         ...     )
         ... )
-        >>> response = isabelle_client.help()
-        >>> print(response.response_body)
+        >>> test_response = isabelle_client.help()
+        >>> print(test_response.response_body)
         ["help", "echo"]
 
         :returns: ``isabelle`` server response
@@ -241,8 +242,8 @@ def purge_theories(
         ...         "OK", json.dumps({"purged": [], "retained": []})
         ...     )
         ... )
-        >>> response = isabelle_client.purge_theories("test", [])
-        >>> print(response.response_body)
+        >>> test_response = isabelle_client.purge_theories("test", [])
+        >>> print(test_response.response_body)
         {"purged": [], "retained": []}
 
         :param session_id: an ID of the session from which to purge theories
@@ -255,6 +256,50 @@ def purge_theories(
         )
         return response
 
+    def cancel(self, task: str) -> IsabelleResponse:
+        """
+        asks a server to try to cancel a task with a given ID
+
+        >>> from unittest.mock import Mock
+        >>> isabelle_client = IsabelleClient("localhost", 1000, "test")
+        >>> isabelle_client.execute_command = Mock(
+        ...     return_value=IsabelleResponse(
+        ...         "OK", ""
+        ...     )
+        ... )
+        >>> test_response = isabelle_client.cancel("test_task")
+        >>> print(test_response.response_body)
+        <BLANKLINE>
+
+        :param task: a task ID
+        :returns: ``isabelle`` server response
+        """
+        arguments = {"task": task}
+        response = self.execute_command(
+            f"cancel {json.dumps(arguments)}", asynchronous=False
+        )
+        return response
+
+    def shutdown(self) -> IsabelleResponse:
+        """
+        asks a server to shutdown immediately
+
+        >>> from unittest.mock import Mock
+        >>> isabelle_client = IsabelleClient("localhost", 1000, "test")
+        >>> isabelle_client.execute_command = Mock(
+        ...     return_value=IsabelleResponse(
+        ...         "OK", ""
+        ...     )
+        ... )
+        >>> test_response = isabelle_client.shutdown()
+        >>> print(test_response.response_body)
+        <BLANKLINE>
+
+        :returns: ``isabelle`` server response
+        """
+        response = self.execute_command("shutdown", asynchronous=False)
+        return response
+
 
 def get_isabelle_client_from_server_info(server_file: str) -> IsabelleClient:
     """
@@ -266,8 +311,8 @@ def get_isabelle_client_from_server_info(server_file: str) -> IsabelleClient:
     Traceback (most recent call last):
         ...
     ValueError: Unexpected server info: wrong
-    >>> server_info = 'server "test" = 127.0.0.1:10000 (password "pass")'
-    >>> with patch("builtins.open", mock_open(read_data=server_info)):
+    >>> server_inf = 'server "test" = 127.0.0.1:10000 (password "pass")'
+    >>> with patch("builtins.open", mock_open(read_data=server_inf)):
     ...     print(get_isabelle_client_from_server_info("test").port)
     10000
 

isabelle_client/utils.py

@@ -42,7 +42,7 @@ def __str__(self):
                 else ""
             )
             + self.response_type
-            + " "
+            + (" " if self.response_body != "" else "")
             + self.response_body
         )
 
@@ -56,9 +56,9 @@ def get_delimited_message(
     get a delimited (not fixed-length)response from a TCP socket
 
     >>> from unittest.mock import Mock
-    >>> tcp_socket = Mock()
-    >>> tcp_socket.recv = Mock(side_effect=[b"4", b"2" b"\\n"])
-    >>> print(get_delimited_message(tcp_socket))
+    >>> test_socket = Mock()
+    >>> test_socket.recv = Mock(side_effect=[b"4", b"2" b"\\n"])
+    >>> print(get_delimited_message(test_socket))
     42
 
     :param tcp_socket: a TCP socket to receive data from
@@ -82,11 +82,11 @@ def get_fixed_length_message(
     get a response of a fixed length from a TCP socket
 
     >>> from unittest.mock import Mock
-    >>> tcp_socket = Mock()
-    >>> tcp_socket.recv = Mock(
+    >>> test_socket = Mock()
+    >>> test_socket.recv = Mock(
     ...     side_effect=[b'FINISHED {"session_id": "session_id__42"}\\n']
     ... )
-    >>> print(get_fixed_length_message(tcp_socket, 42))
+    >>> print(get_fixed_length_message(test_socket, 42))
     FINISHED {"session_id": "session_id__42"}
 
     :param tcp_socket: a TCP socket to receive data from
@@ -113,16 +113,16 @@ def get_response_from_isabelle(tcp_socket: socket.socket) -> IsabelleResponse:
     only one integer number denoting length
 
     >>> from unittest.mock import Mock
-    >>> tcp_socket = Mock()
-    >>> tcp_socket.recv = Mock(
+    >>> test_socket = Mock()
+    >>> test_socket.recv = Mock(
     ...     side_effect=[
     ...         b"4",
     ...         b"2",
     ...         b"\\n",
     ...         b'FINISHED {"session_id": "session_id__42"}\\n',
     ...     ]
     ... )
-    >>> print(str(get_response_from_isabelle(tcp_socket)))
+    >>> print(str(get_response_from_isabelle(test_socket)))
     42
     FINISHED {"session_id": "session_id__42"}
 
@@ -134,7 +134,7 @@ def get_response_from_isabelle(tcp_socket: socket.socket) -> IsabelleResponse:
     length = int(match.group(1)) if match is not None else None
     if length is not None:
         response = get_fixed_length_message(tcp_socket, length)
-    match = re.compile(r"(\w+) (.*)").match(response)
+    match = re.compile(r"(\w+) ?(.*)").match(response)
     if match is None:
         raise ValueError(f"Unexpected response from Isabelle: {response}")
     return IsabelleResponse(match.group(1), match.group(2), length)
@@ -150,30 +150,23 @@ def get_final_message(
     'final' type arrives
 
     >>> from unittest.mock import Mock
-    >>> tcp_socket = Mock()
-    >>> tcp_socket.recv = Mock(
+    >>> test_socket = Mock()
+    >>> test_socket.recv = Mock(
     ...    side_effect=[
-    ...        b"O", b"K", b" ", b"i", b"\\n",
+    ...        b"O", b"K", b"\\n",
     ...        b"4", b"0", b"\\n",
     ...        b'FINISHED {"session_id": "test_session"}\\n'
     ...    ]
     ... )
-    >>> logger = Mock()
-    >>> logger.info = Mock()
+    >>> test_logger = Mock()
+    >>> test_logger.info = Mock()
     >>> print(str(get_final_message(
-    ...     tcp_socket, {"FINISHED"}, logger
+    ...     test_socket, {"FINISHED"}, test_logger
     ... )))
     40
     FINISHED {"session_id": "test_session"}
-    >>> print(logger.info.mock_calls)
-    [call('OK i'), call('40\\nFINISHED {"session_id": "test_session"}')]
-    >>> tcp_socket.recv = Mock(
-    ...     side_effect=[b"5", b"\\n", b"wrong"]
-    ... )
-    >>> print(get_final_message(tcp_socket, {"FINISHED"}))
-    Traceback (most recent call last):
-        ...
-    ValueError: Unexpected response from Isabelle: wrong
+    >>> print(test_logger.info.mock_calls)
+    [call('OK'), call('40\\nFINISHED {"session_id": "test_session"}')]
 
     :param tcp_socket:  a TCP socket to ``isabelle`` server
     :param final_message: a set of possible final message types