Merge pull request #19 from inpefess/start-server

Start server

.gitignore

@@ -5,4 +5,5 @@ venv/
 __pycache__/
 .*~
 *~
-doc/build/
+doc/build/
+.idea/

.pylintrc

@@ -3,3 +3,4 @@
 max-line-length=79
 disable=bad-continuation
 max-statements=10
+generated-members=asyncio.subprocess.*

README.md

@@ -6,6 +6,64 @@ A client for [Isabelle](https://isabelle.in.tum.de) server. For more information
 
 For information on using this client see [documentation](https://isabelle-client.readthedocs.io).
 
+# How to install
+
+```bash
+pip install isabelle-client
+```
+
+# How to start Isabelle server
+
+```bash
+isabelle server > server.info
+```
+
+since we'll need server info for connecting to it with this client. Or:
+
+```Python
+from isabelle_client.utils import start_isabelle_server
+
+server_info, server_process = start_isabelle_server()
+``` 
+
+# How to connect to the server
+
+```Python
+from isabelle_client.utils import get_isabelle_client
+
+isabelle = get_isabelle_client(server_info)
+```
+
+# How to send a command to the server
+
+```Python
+isabelle.session_build(dirs=["."], session="examples")
+```
+
+Note that this method returns only the last reply from the server.
+
+# How to log all replies from the server
+
+We can add a standard Python logger to the client:
+
+```Python
+import logging
+
+isabelle.logger = logging.getLogger()
+isabelle.logger.setLevel(logging.INFO)
+isabelle.logger.addHandler(logging.FileHandler("out.log"))
+```
+
+Then all replies from the server will go to the file ``out.log``.
+
+# Examples
+
+An example of using this package is located in ``examples`` directory.
+
+# Video example
+
 ![video tutorial](https://github.com/inpefess/isabelle-client/blob/master/examples/tty.gif).
 
+# Contributing
+
 Issues and PRs are welcome.

doc/source/conf.py

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

doc/source/package-documentation.rst

@@ -30,12 +30,21 @@ Isabelle Client
    :special-members: __init__
    :members:
 
-utils
------
-.. currentmodule:: isabelle_client.utils
+socket_communication
+--------------------
+.. currentmodule:: isabelle_client.socket_communication
 
-A collection of different functions used by other modules.
+A collection of functions for TCP communication.
 
 .. autofunction:: get_delimited_message
 .. autofunction:: get_fixed_length_message
 .. autofunction:: get_response_from_isabelle
+
+utils
+-----
+.. currentmodule:: isabelle_client.utils
+
+A collection of different useful functhions.
+
+.. autofunction:: start_isabelle_server
+.. autofunction:: get_isabelle_client

examples/example.py

@@ -15,25 +15,26 @@
 """
 import logging
 
-from isabelle_client import get_isabelle_client_from_server_info
+from isabelle_client.utils import get_isabelle_client, start_isabelle_server
 
 
 def main():
     """ using ``isabelle`` client """
-    # first, run Isabelle server in the same directory as this script:
-    # isabelle server > server.info
-    isabelle = get_isabelle_client_from_server_info("server.info")
+    # first, we start Isabelle server
+    server_info, _ = start_isabelle_server()
+    isabelle = get_isabelle_client(server_info)
     # we will log all the messages from the server to stdout
-    logging.basicConfig(filename="out.log")
     isabelle.logger = logging.getLogger()
     isabelle.logger.setLevel(logging.INFO)
+    isabelle.logger.addHandler(logging.FileHandler("out.log"))
     # now we can send a theory file from this directory to the server
     # and get a response
     # isabelle.use_theories(theories=["Dummy"], master_dir=".")
     # or we can build a session document using ROOT and root.tex files from it
     isabelle.session_build(dirs=["."], session="examples")
     # or we can issue a free-text command through TCP
     isabelle.execute_command("echo 42", asynchronous=False)
+    isabelle.shutdown()
 
 
 if __name__ == "__main__":

isabelle_client/__init__.py

@@ -13,8 +13,6 @@
 See the License for the specific language governing permissions and
 limitations under the License.
 """
-from isabelle_client.isabelle_client import (
-    IsabelleClient,
-    get_isabelle_client_from_server_info,
-)
-from isabelle_client.utils import IsabelleResponse
+from isabelle_client.isabelle__client import IsabelleClient
+from isabelle_client.socket_communication import IsabelleResponse
+from isabelle_client.utils import get_isabelle_client

isabelle_client/isabelle_client.py → isabelle_client/isabelle__client.py

@@ -14,12 +14,14 @@
 limitations under the License.
 """
 import json
-import re
 import socket
 from logging import Logger
 from typing import Dict, List, Optional, Union
 
-from isabelle_client.utils import IsabelleResponse, get_final_message
+from isabelle_client.socket_communication import (
+    IsabelleResponse,
+    get_final_message,
+)
 
 
 class IsabelleClient:
@@ -60,7 +62,10 @@ def execute_command(
         >>> with (
         ...     patch("socket.socket.connect", connect),
         ...     patch("socket.socket.send", send),
-        ...     patch("isabelle_client.isabelle_client.get_final_message", res)
+        ...     patch(
+        ...         "isabelle_client.isabelle__client.get_final_message",
+        ...         res
+        ...     )
         ... ):
         ...    test_response = isabelle_client.execute_command("test")
         >>> print(test_response.response_type)
@@ -183,6 +188,7 @@ def use_theories(
         theories: List[str],
         session_id: Optional[str] = None,
         master_dir: Optional[str] = None,
+        watchdog_timeout: Optional[int] = None,
     ) -> IsabelleResponse:
         """
         run the engine on theory files
@@ -195,7 +201,7 @@ def use_theories(
         ...     )
         ... )
         >>> test_response = isabelle_client.use_theories(
-        ...     ["test"], master_dir="test"
+        ...     ["test"], master_dir="test", watchdog_timeout=0
         ... )
         >>> print(test_response.response_type)
         FINISHED
@@ -205,21 +211,25 @@ def use_theories(
             created and then destroyed after trying to process theories
         :param master_dir: where to look for theory files; if ``None``, uses a
             temp folder of the session
+        :param watchdog_timeout: for how long to wait a response from server
         :returns: ``isabelle`` server response
         """
         new_session_id = (
             self.session_start() if session_id is None else session_id
         )
-        try:
-            arguments = {"session_id": new_session_id, "theories": theories}
-            if master_dir is not None:
-                arguments["master_dir"] = master_dir
-            response = self.execute_command(
-                f"use_theories {json.dumps(arguments)}"
-            )
-        finally:
-            if session_id is None:
-                self.session_stop(new_session_id)
+        arguments: Dict[str, Union[List[str], int, str]] = {
+            "session_id": new_session_id,
+            "theories": theories,
+        }
+        if watchdog_timeout is not None:
+            arguments["watchdog_timeout"] = watchdog_timeout
+        if master_dir is not None:
+            arguments["master_dir"] = master_dir
+        response = self.execute_command(
+            f"use_theories {json.dumps(arguments)}"
+        )
+        if session_id is None:
+            self.session_stop(new_session_id)
         return response
 
     def echo(self, message: str) -> IsabelleResponse:
@@ -335,34 +345,3 @@ def shutdown(self) -> IsabelleResponse:
         """
         response = self.execute_command("shutdown", asynchronous=False)
         return response
-
-
-def get_isabelle_client_from_server_info(server_file: str) -> IsabelleClient:
-    """
-    get an instance of ``IsabelleClient`` from a server info file
-
-    >>> from unittest.mock import mock_open, patch
-    >>> with patch("builtins.open", mock_open(read_data="wrong")):
-    ...     print(get_isabelle_client_from_server_info("test"))
-    Traceback (most recent call last):
-        ...
-    ValueError: Unexpected server info: wrong
-    >>> 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
-
-    :param server_file: a file with server info (a line returned by a server
-    on start)
-    :returns: an ``isabelle`` client
-    """
-    with open(server_file, "r") as server_info_file:
-        server_info = server_info_file.read()
-    match = re.compile(
-        r"server \"(.*)\" = (.*):(.*) \(password \"(.*)\"\)"
-    ).match(server_info)
-    if match is None:
-        raise ValueError(f"Unexpected server info: {server_info}")
-    _, address, port, password = match.groups()
-    isabelle_client = IsabelleClient(address, int(port), password)
-    return isabelle_client