Merge pull request #28 from inpefess/python-versions

Python versions

.gitignore

@@ -1,7 +1,7 @@
 .coverage
 dist/
 test-results/
-venv/
+venv*/
 __pycache__/
 .*~
 *~

doc/source/conf.py

@@ -33,10 +33,6 @@
 copyright = "2021, Boris Shminke"
 author = "Boris Shminke"
 
-# The full version, including alpha/beta/rc tags
-release = "0.2.1"
-
-
 # -- General configuration ---------------------------------------------------
 
 # Add any Sphinx extension module names here, as strings. They can be
@@ -59,8 +55,3 @@
 # a list of builtin themes.
 #
 html_theme = "sphinx_rtd_theme"
-
-# Add any paths that contain custom static files (such as style sheets) here,
-# relative to this directory. They are copied after the builtin static files,
-# so a file named "default.css" will overwrite the builtin "default.css".
-html_static_path = ["_static"]

doc/source/index.rst

@@ -18,6 +18,16 @@ Welcome to Isabelle client documentation!
 
 A client for `Isabelle`_ server. For more information about the server see part 4 of `the Isabelle system manual`_.
 
+How to install
+===============
+
+The best way to install this client is to use ``pip``::
+
+    pip install isabelle-client
+
+In what case to use
+====================
+
 This client might be useful if:
 
 * you have an Isabelle server instance running
@@ -26,6 +36,23 @@ This client might be useful if:
 
 See also :ref:`usage-example`.
 
+How to contribute
+==================
+
+Pull requests on are welcome. To start::
+
+    git clone https://github.com/inpefess/isabelle-client
+    cd isabelle-client
+    # activate python virtual environment with Python 3.6+
+    pip install -U pip
+    pip install -U setuptools wheel poetry
+    poetry install
+    # recommended but not necessary
+    pre-commit install
+
+To check the code quality before creating a pull request, one might run the script ``show_report.sh``. It locally does nearly the same as the CI pipeline after the PR is created.
+
+
 .. toctree::
    :maxdepth: 2
    :caption: Contents:

doc/source/usage-example.rst

@@ -18,22 +18,29 @@
 Basic usage example
 ====================
 
-Let's suppose that Isabelle binary is on our ``PATH`` and we started an Isabelle server in working directory with the following command::
+First, we need to start an Isabelle server::
+  
+    from isabelle_client import start_isabelle_server
 
-    isabelle server > server.pid
+    server_info, _ = start_isabelle_server(
+        name="test", port=9999, log_file="server.log"
+    )
 
-Now we can get an instance of Isabelle client to talk to this server from Python in a very simple way::
+We could also start the server outside this script and use its info.
 
-    from isabelle_client import get_isabelle_client_from_server_info
-  
-    isabelle = get_isabelle_client_from_server_info("server.pid")
+Now let's create a client to our server ::
 
-It might be useful to log all replies from the server somewhere, e.g.::
+    from isabelle_client import get_isabelle_client
 
+    isabelle = get_isabelle_client(server_info)
+
+We will log all the messages from the server to a file ::
+  
     import logging
 
-    logging.basicConfig(filename="out.log")
     isabelle.logger = logging.getLogger()
+    isabelle.logger.setLevel(logging.INFO)
+    isabelle.logger.addHandler(logging.FileHandler("session.log"))
 
 This client has several methods implemented to communicate with the server Python-style, e.g.::
 
@@ -43,5 +50,6 @@ In this command it's supposed that we have a ``Dummy.thy`` theory file in our wo
 
 One can also issue a free-form command, e.g.::
 
-    isabelle.execute_command("echo 42", asynchronous=False)
+    from isabelle_client import async_run
 
+    async_run(isabelle.execute_command("echo 42", asynchronous=False))

examples/example.py

@@ -13,10 +13,13 @@
 See the License for the specific language governing permissions and
 limitations under the License.
 """
-import asyncio
 import logging
 
-from isabelle_client import get_isabelle_client, start_isabelle_server
+from isabelle_client import (
+    async_run,
+    get_isabelle_client,
+    start_isabelle_server,
+)
 
 
 def main():
@@ -38,7 +41,7 @@ def main():
     # 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
-    asyncio.run(isabelle.execute_command("echo 42", asynchronous=False))
+    async_run(isabelle.execute_command("echo 42", asynchronous=False))
     isabelle.shutdown()
 
 

examples/video_example/example.txt

@@ -26,9 +26,9 @@ SLEEP 3
 # note that the client returns only the last reply from the server
 # all other messages are saved to the log file
 # we also can issue a free-form command through TCP
-import asyncio
+from isabelle_client import async_run
 
-asyncio.run(isabelle.execute_command("echo 42", asynchronous=False))
+async_run(isabelle.execute_command("echo 42", asynchronous=False))
 exit()
 # our sessions was logged to the file:
 cat session.log & sleep 3

isabelle_client/__init__.py

@@ -13,6 +13,7 @@
 See the License for the specific language governing permissions and
 limitations under the License.
 """
+from isabelle_client.compatibility_helper import async_run
 from isabelle_client.isabelle__client import IsabelleClient
 from isabelle_client.socket_communication import IsabelleResponse
 from isabelle_client.utils import get_isabelle_client, start_isabelle_server

isabelle_client/compatibility_helper.py

@@ -0,0 +1,34 @@
+"""
+Copyright 2021 Boris Shminke
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    http://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+"""
+import asyncio
+import sys
+from typing import Any, Coroutine
+
+
+def async_run(a_coroutine: Coroutine) -> Any:
+    """
+    a simple function which models the behaviour of `asyncio.run` method for
+    Python 3.6
+
+    :param a_coroutine: some coroutine to await for
+    :returns: whatever the coroutine returns
+    """
+    if sys.version_info.major == 3 and sys.version_info.minor >= 7:
+        # pylint: disable=no-member
+        result = asyncio.run(a_coroutine)  # type: ignore
+    else:
+        result = asyncio.get_event_loop().run_until_complete(a_coroutine)
+    return result

isabelle_client/isabelle__client.py

@@ -18,6 +18,7 @@
 from logging import Logger
 from typing import Any, Dict, List, Optional, Union
 
+from isabelle_client.compatibility_helper import async_run
 from isabelle_client.socket_communication import (
     IsabelleResponse,
     get_final_message,
@@ -56,7 +57,7 @@ async def execute_command(
         >>> isabelle_client = IsabelleClient(
         ...     "localhost", 9999, "test_password", logger
         ... )
-        >>> test_response = asyncio.run(
+        >>> test_response = async_run(
         ...     isabelle_client.execute_command("test_command")
         ... )
         >>> print(test_response.response_type)
@@ -123,7 +124,7 @@ def session_build(
             arguments["dirs"] = dirs
         for name in kwargs:
             arguments[name] = kwargs[name]
-        response = asyncio.run(
+        response = async_run(
             self.execute_command(f"session_build {json.dumps(arguments)}")
         )
         return response
@@ -149,7 +150,7 @@ def session_start(self, session: str = "HOL", **kwargs) -> str:
         arguments = {"session": session}
         for name in kwargs:
             arguments[name] = kwargs[name]
-        response = asyncio.run(
+        response = async_run(
             self.execute_command(f"session_start {json.dumps(arguments)}")
         )
         if response.response_type == "FINISHED":
@@ -169,9 +170,7 @@ def session_stop(self, session_id: str) -> IsabelleResponse:
         :returns: ``isabelle`` server response
         """
         arguments = json.dumps({"session_id": session_id})
-        response = asyncio.run(
-            self.execute_command(f"session_stop {arguments}")
-        )
+        response = async_run(self.execute_command(f"session_stop {arguments}"))
         return response
 
     def use_theories(
@@ -211,7 +210,7 @@ def use_theories(
             arguments[name] = kwargs[name]
         if master_dir is not None:
             arguments["master_dir"] = master_dir
-        response = asyncio.run(
+        response = async_run(
             self.execute_command(f"use_theories {json.dumps(arguments)}")
         )
         if session_id is None:
@@ -230,7 +229,7 @@ def echo(self, message: Any) -> IsabelleResponse:
         :param message: any text
         :returns: ``isabelle`` server response
         """
-        response = asyncio.run(
+        response = async_run(
             self.execute_command(
                 f"echo {json. dumps(message)}", asynchronous=False
             )
@@ -248,9 +247,7 @@ def help(self) -> IsabelleResponse:
 
         :returns: ``isabelle`` server response
         """
-        response = asyncio.run(
-            self.execute_command("help", asynchronous=False)
-        )
+        response = async_run(self.execute_command("help", asynchronous=False))
         return response
 
     def purge_theories(
@@ -285,7 +282,7 @@ def purge_theories(
             arguments["master_dir"] = master_dir
         if purge_all is not None:
             arguments["all"] = purge_all
-        response = asyncio.run(
+        response = async_run(
             self.execute_command(
                 f"purge_theories {json.dumps(arguments)}", asynchronous=False
             )
@@ -305,7 +302,7 @@ def cancel(self, task: str) -> IsabelleResponse:
         :returns: ``isabelle`` server response
         """
         arguments = {"task": task}
-        response = asyncio.run(
+        response = async_run(
             self.execute_command(
                 f"cancel {json.dumps(arguments)}", asynchronous=False
             )
@@ -323,7 +320,7 @@ def shutdown(self) -> IsabelleResponse:
 
         :returns: ``isabelle`` server response
         """
-        response = asyncio.run(
+        response = async_run(
             self.execute_command("shutdown", asynchronous=False)
         )
         return response

isabelle_client/socket_communication.py

@@ -56,6 +56,7 @@ async def get_response_from_isabelle(
     * a fixed length message after a carriage-return delimited message with
     only one integer number denoting length
 
+    >>> from isabelle_client.compatibility_helper import async_run
     >>> async def awaiter():
     ...     test_reader, test_writer = await asyncio.open_connection(
     ...     "localhost", 9999
@@ -64,7 +65,7 @@ async def get_response_from_isabelle(
     ...     result = [str(await get_response_from_isabelle(test_reader))]
     ...     result += [str(await get_response_from_isabelle(test_reader))]
     ...     return result
-    >>> print(asyncio.run(awaiter()))
+    >>> print(async_run(awaiter()))
     ['OK "connection OK"', '43\\nFINISHED {"session_id": "test_session_id"}']
     >>> async def awaiter():
     ...     test_reader, test_writer = await asyncio.open_connection(
@@ -74,7 +75,7 @@ async def get_response_from_isabelle(
     ...     result = [str(await get_response_from_isabelle(test_reader))]
     ...     result += [str(await get_response_from_isabelle(test_reader))]
     ...     return result
-    >>> print(asyncio.run(awaiter()))
+    >>> print(async_run(awaiter()))
     Traceback (most recent call last):
       ...
     ValueError: Unexpected response from Isabelle: # !!!
@@ -102,6 +103,7 @@ async def get_final_message(
     gets responses from ``isabelle`` server until a message of specified
     'final' type arrives
 
+    >>> from isabelle_client.compatibility_helper import async_run
     >>> test_logger = getfixture("mock_logger")
     >>> async def awaiter():
     ...     test_reader, test_writer = await asyncio.open_connection(
@@ -112,7 +114,7 @@ async def get_final_message(
     ...         test_reader, {"FINISHED"}, test_logger
     ...     ))
     ...     return result
-    >>> print(asyncio.run(awaiter()))
+    >>> print(async_run(awaiter()))
     43
     FINISHED {"session_id": "test_session_id"}
     >>> print(test_logger.info.mock_calls)

isabelle_client/utils.py

@@ -17,6 +17,7 @@
 import re
 from typing import Optional, Tuple
 
+from isabelle_client.compatibility_helper import async_run
 from isabelle_client.isabelle__client import IsabelleClient
 
 
@@ -80,4 +81,4 @@ async def async_call():
             "utf-8"
         ), isabelle_server
 
-    return asyncio.run(async_call())
+    return async_run(async_call())