Merge pull request #4 from inpefess/add-tests

Add tests

.circleci/config.yml

@@ -29,7 +29,7 @@ jobs:
           name: run tests
           command: |
             . venv/bin/activate
-            pytest --cov isabelle_client --cov-report xml --cov-fail-under=33\
+            pytest --cov isabelle_client --cov-report xml --cov-fail-under=99\
                    --junit-xml test-results/isabelle-client.xml\
                    --doctest-modules isabelle_client tests
       - run:

doc/source/conf.py

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

doc/source/index.rst

@@ -1,7 +1,7 @@
 Welcome to Isabelle client documentation!
 ===========================================
 
-A client for [Isabelle](https://isabelle.in.tum.de) server. For more information about the server see part 4 of [the Isabelle system manual](https://isabelle.in.tum.de/dist/Isabelle2021/doc/system.pdf).
+A client for `Isabelle`_ server. For more information about the server see part 4 of `the Isabelle system manual`_.
 
 Basic use-case:
 
@@ -21,3 +21,6 @@ Indices and tables
 * :ref:`genindex`
 * :ref:`modindex`
 * :ref:`search`
+
+.. _Isabelle: https://isabelle.in.tum.de
+.. _the Isabelle system manual: https://isabelle.in.tum.de/dist/Isabelle2021/doc/system.pdf

isabelle_client/isabelle_client.py

@@ -53,6 +53,37 @@ def get_all_responses(
         log_file: Optional[io.TextIOWrapper] = None,
     ) -> List[str]:
         """
+        gets responses from ``isabelle`` server until a message of specified
+        'final' type arrives
+
+        >>> from unittest.mock import Mock
+        >>> isabelle_client = IsabelleClient("test", "localhost", 1000, "test")
+        >>> tcp_socket = Mock()
+        >>> tcp_socket.recv = Mock(
+        ...    side_effect=[
+        ...        b"4",
+        ...        b"2",
+        ...        b"\\n",
+        ...        b'FINISHED {"session_id": "session_id__42"}\\n',
+        ...    ]
+        ... )
+        >>> log_file = Mock()
+        >>> log_file.write = Mock()
+        >>> print(isabelle_client.get_all_responses(
+        ...     tcp_socket, {"FINISHED"}, log_file)
+        ... )
+        ['42', 'FINISHED', '{"session_id": "session_id__42"}']
+        >>> print(log_file.write.mock_calls)
+        [call('42\\nFINISHED {"session_id": "session_id__42"}\\n')]
+        >>> tcp_socket.recv = Mock(
+        ...     side_effect=[b"5", b"\\n", b"wrong"]
+        ... )
+        >>> print(isabelle_client.get_all_responses(tcp_socket, {"FINISHED"}))
+        Traceback (most recent call last):
+            ...
+        ValueError: Unexpected response from Isabelle: 5
+        wrong
+
         :param tcp_socket:  a TCP socket to ``isabelle`` server
         :param final_message: a set of possible final message types
         :param log_file: a file for writing a copy of all messages
@@ -81,6 +112,33 @@ def execute_command(
         """
         executes an (asynchronous) command and waits for results
 
+        >>> from unittest.mock import Mock, patch, mock_open
+        >>> isabelle_client = IsabelleClient("test", "localhost", 1000, "test")
+        >>> isabelle_client.get_all_responses = Mock(
+        ...    side_effect=[
+        ...         ["42", "FINISHED", '{"session_id": "session_id__42"}']
+        ...     ]
+        ... )
+        >>> connect = Mock()
+        >>> send = Mock()
+        >>> open_mock = mock_open()
+        >>> with patch("socket.socket.connect", connect), patch(
+        ...    "socket.socket.send", send
+        ... ), patch("builtins.open", open_mock):
+        ...    response = isabelle_client.execute_command("test", "test")
+        >>> print(response.response_type)
+        FINISHED
+        >>> print(response.response_body)
+        {"session_id": "session_id__42"}
+        >>> print(response.response_length)
+        42
+        >>> print(connect.mock_calls)
+        [call(('localhost', 1000))]
+        >>> print(send.mock_calls)
+        [call(b'test\\ntest\\n')]
+        >>> print(open_mock.mock_calls)
+        [call('test', 'w'), call().close()]
+
         :param command: a full text of a command to ``isabelle``
         :param log_filename: a file for saving a copy of all data received from
             the server
@@ -113,7 +171,25 @@ def execute_command(
         )
 
     def session_start(self, session_image: str = "HOL") -> str:
-        """start a new session
+        """
+        start a new session
+
+        >>> from unittest.mock import Mock
+        >>> isabelle_client = IsabelleClient("test", "localhost", 1000, "test")
+        >>> isabelle_client.execute_command = Mock(
+        ...     return_value=IsabelleResponse(
+        ...     "FINISHED", '{"session_id": "test"}'
+        ...     )
+        ... )
+        >>> print(isabelle_client.session_start())
+        test
+        >>> isabelle_client.execute_command = Mock(
+        ...     return_value=IsabelleResponse("OK", "OK")
+        ... )
+        >>> print(isabelle_client.session_start())
+        Traceback (most recent call last):
+            ...
+        ValueError: Unexpected response type: OK
 
         :param session: a name of a session image
         :returns: a ``session_id``
@@ -122,10 +198,20 @@ def session_start(self, session_image: str = "HOL") -> str:
         response = self.execute_command(f"session_start {arguments}")
         if response.response_type == "FINISHED":
             return json.loads(response.response_body)["session_id"]
-        raise ValueError(response)
+        raise ValueError(f"Unexpected response type: {response.response_type}")
 
     def session_stop(self, session_id: str) -> IsabelleResponse:
-        """stop session with given ID
+        """
+        stop session with given ID
+
+        >>> from unittest.mock import Mock
+        >>> isabelle_client = IsabelleClient("test", "localhost", 1000, "test")
+        >>> isabelle_client.execute_command = Mock(
+        ...     return_value=IsabelleResponse("FAILED", "")
+        ... )
+        >>> response = isabelle_client.session_stop("test")
+        >>> print(response.response_type)
+        FAILED
 
         :param session_id: a string ID of a session
         :returns: ``isabelle`` server response
@@ -141,7 +227,21 @@ def use_theories(
         master_dir: Optional[str] = None,
         log_filename: Optional[str] = None,
     ) -> IsabelleResponse:
-        """run the engine on theory files
+        """
+        run the engine on theory files
+
+        >>> from unittest.mock import Mock
+        >>> isabelle_client = IsabelleClient("test", "localhost", 1000, "test")
+        >>> isabelle_client.execute_command = Mock(
+        ...     return_value=IsabelleResponse(
+        ...         "FINISHED", '{"session_id": "test"}'
+        ...     )
+        ... )
+        >>> response = isabelle_client.use_theories(
+        ...     ["test"], master_dir="test"
+        ... )
+        >>> print(response.response_type)
+        FINISHED
 
         :param theories: names of theory files (without extensions!)
         :param session_id: an ID of a session; if ``None``, a new session is

isabelle_client/utils.py

@@ -27,8 +27,14 @@ 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))
+    42
+
     :param tcp_socket: a TCP socket to receive data from
-    :param response_end_char: a character which marks the end of response
+    :param delimiter: a character which marks the end of response
     :param encoding: a socket encoding
     :returns: decoded string response
     """
@@ -47,6 +53,14 @@ 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(
+    ...     side_effect=[b'FINISHED {"session_id": "session_id__42"}\\n']
+    ... )
+    >>> print(get_fixed_length_message(tcp_socket, 42))
+    FINISHED {"session_id": "session_id__42"}
+
     :param tcp_socket: a TCP socket to receive data from
     :param message_length: a number of bytes to read as a message
     :param chunk_size: the maximal number of bytes to get at one time
@@ -67,6 +81,20 @@ def get_response_from_isabelle(tcp_socket: socket.socket) -> str:
     """
     get a response of a fixed length from a TCP socket
 
+    >>> from unittest.mock import Mock
+    >>> tcp_socket = Mock()
+    >>> tcp_socket.recv = Mock(
+    ...     side_effect=[
+    ...         b"4",
+    ...         b"2",
+    ...         b"\\n",
+    ...         b'FINISHED {"session_id": "session_id__42"}\\n',
+    ...     ]
+    ... )
+    >>> print(get_response_from_isabelle(tcp_socket))
+    42
+    FINISHED {"session_id": "session_id__42"}
+
     :param tcp_socket: a TCP socket to receive data from
     :returns: decoded string response
     """

pyproject.toml

@@ -1,6 +1,6 @@
 [tool.poetry]
 name = "isabelle-client"
-version = "0.0.4"
+version = "0.0.5"
 description = "A client to Isabelle proof assistant server"
 authors = ["Boris Shminke <boris@shminke.ml>"]
 license = "Apache-2.0"

show_report.sh

@@ -2,11 +2,14 @@
 
 set -e
 PACKAGE_NAME=isabelle_client
+cd doc
+make clean html
+cd ..
 pycodestyle --max-doc-length 160 --ignore E203,E501,W503 \
 	    ${PACKAGE_NAME} tests
 pylint --rcfile=.pylintrc ${PACKAGE_NAME} tests
 mypy --config-file mypy.ini ${PACKAGE_NAME} tests
-pytest --cov ${PACKAGE_NAME} --cov-report term-missing --cov-fail-under=33 \
+pytest --cov ${PACKAGE_NAME} --cov-report term-missing --cov-fail-under=99 \
        --junit-xml test-results/isabelle-client.xml \
        --doctest-modules ${PACKAGE_NAME}
 cloc ${PACKAGE_NAME}