Merge pull request #24 from inpefess/server-start-parameters

Server start parameters

Author: inpefess

doc/source/conf.py

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

examples/example.py

@@ -22,12 +22,14 @@
 def main():
     """ using ``isabelle`` client """
     # first, we start Isabelle server
-    server_info, _ = start_isabelle_server()
+    server_info, _ = start_isabelle_server(
+        name="test", port="9999", log_file="server.log"
+    )
     isabelle = get_isabelle_client(server_info)
-    # we will log all the messages from the server to stdout
+    # we will log all the messages from the server to a file
     isabelle.logger = logging.getLogger()
     isabelle.logger.setLevel(logging.INFO)
-    isabelle.logger.addHandler(logging.FileHandler("out.log"))
+    isabelle.logger.addHandler(logging.FileHandler("session.log"))
     # now we can send a theory file from this directory to the server
     # and get a response
     isabelle.use_theories(

examples/tty.gif

@@ -0,0 +1,27 @@
+"""
+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 time
+
+with open("video_example/example.txt", "r") as example:
+    lines = example.readlines()
+
+for line in lines:
+    if line[:6] == "SLEEP ":
+        time.sleep(int(line[6:]))
+    else:
+        for char in line:
+            print(char, end="", flush=True)
+            time.sleep(60 / 600)

examples/video_example/char_by_char.py

@@ -0,0 +1,36 @@
+# Hi! This is an example of using ``isabelle-client`` package
+python
+# first, we need to start an Isabelle server
+from isabelle_client import start_isabelle_server
+
+server_info, _ = start_isabelle_server(
+    name="test", port=9999, log_file="server.log"
+)
+SLEEP 1
+# we could also start the server outside this scrit and use its info
+# now let's create a client to our server
+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
+
+isabelle.logger = logging.getLogger()
+isabelle.logger.setLevel(logging.INFO)
+isabelle.logger.addHandler(logging.FileHandler("session.log"))
+# let's suppose that we also have another Python script which generates some
+# theory files
+# now we can build a session document using ROOT and root.tex files
+isabelle.session_build(dirs=["."], session="examples")
+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
+
+asyncio.run(isabelle.execute_command("echo 42", asynchronous=False))
+exit()
+# our sessions was logged to the file:
+cat session.log & sleep 3
+SLEEP 3
+bye

examples/video_example/example.txt

@@ -15,7 +15,7 @@
 """
 import asyncio
 import re
-from typing import Tuple
+from typing import Optional, Tuple
 
 from isabelle_client.isabelle__client import IsabelleClient
 
@@ -45,9 +45,11 @@ def get_isabelle_client(server_info: str) -> IsabelleClient:
     return isabelle_client
 
 
-async def async_start_isabelle_server() -> Tuple[
-    str, asyncio.subprocess.Process
-]:
+async def async_start_isabelle_server(
+    log_file: Optional[str] = None,
+    name: Optional[str] = None,
+    port: Optional[int] = None,
+) -> Tuple[str, asyncio.subprocess.Process]:
     """
     a technical function
 
@@ -64,21 +66,39 @@ async def async_start_isabelle_server() -> Tuple[
     >>> server.stdout = None
     >>> server_builder = AsyncMock(return_value=server)
     >>> with patch("asyncio.create_subprocess_exec", server_builder):
-    ...     print(asyncio.run(async_start_isabelle_server())[0])
+    ...     print(asyncio.run(
+    ...     async_start_isabelle_server("out.log", "isabelle", 10000)
+    ... )[0])
     Traceback (most recent call last):
         ...
     ValueError: Failed to start server
+
+    :param log_file: a log file for exceptional output of internal server and
+        session operations
+    :param name: explicit server name (default: isabelle)
+    :param port: explicit server port
+    :returns: a line of server info and server process
     """
+    args = (
+        "server"
+        + (f" -L {log_file}" if log_file is not None else "")
+        + (f" -p {str(port)}" if port is not None else "")
+        + (f" -n {name}" if name is not None else "")
+    )
     isabelle_server = await asyncio.create_subprocess_exec(
-        "isabelle", "server", stdout=asyncio.subprocess.PIPE
+        "isabelle", *(args.split(" ")), stdout=asyncio.subprocess.PIPE
     )
     if isabelle_server.stdout is None:
         raise ValueError("Failed to start server")
     server_info = (await isabelle_server.stdout.readline()).decode("utf-8")
     return server_info, isabelle_server
 
 
-def start_isabelle_server() -> Tuple[str, asyncio.subprocess.Process]:
+def start_isabelle_server(
+    log_file: Optional[str] = None,
+    name: Optional[str] = None,
+    port: Optional[int] = None,
+) -> Tuple[str, asyncio.subprocess.Process]:
     """
     start ``isabelle`` server
 
@@ -90,6 +110,10 @@ def start_isabelle_server() -> Tuple[str, asyncio.subprocess.Process]:
     ...     print(start_isabelle_server())
     TestIsabelleServer
 
+    :param log_file: a log file for exceptional output of internal server and
+        session operations
+    :param name: explicit server name (default: isabelle)
+    :param port: explicit server port
     :return: a line of server info and server process
     """
-    return asyncio.run(async_start_isabelle_server())
+    return asyncio.run(async_start_isabelle_server(log_file, name, port))

isabelle_client/utils.py

@@ -1,6 +1,6 @@
 [tool.poetry]
 name = "isabelle-client"
-version = "0.1.5"
+version = "0.2.0"
 description = "A client to Isabelle proof assistant server"
 authors = ["Boris Shminke <boris@shminke.ml>"]
 license = "Apache-2.0"
@@ -11,7 +11,7 @@ classifiers=[
 	"License :: OSI Approved :: Apache Software License",
 	"Operating System :: OS Independent",
 	"Intended Audience :: Science/Research",
-	"Development Status :: 2 - Pre-Alpha",
+	"Development Status :: 3 - Alpha",
 	"Environment :: Console",
 	"Natural Language :: English",
 	"Topic :: Scientific/Engineering :: Artificial Intelligence",