Merge pull request #23 from inpefess/all-arguments

All arguments

doc/source/conf.py

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

examples/example.py

@@ -16,7 +16,7 @@
 import asyncio
 import logging
 
-from isabelle_client.utils import get_isabelle_client, start_isabelle_server
+from isabelle_client import get_isabelle_client, start_isabelle_server
 
 
 def main():

isabelle_client/__init__.py

@@ -15,4 +15,4 @@
 """
 from isabelle_client.isabelle__client import IsabelleClient
 from isabelle_client.socket_communication import IsabelleResponse
-from isabelle_client.utils import get_isabelle_client
+from isabelle_client.utils import get_isabelle_client, start_isabelle_server

isabelle_client/isabelle__client.py

@@ -16,7 +16,7 @@
 import asyncio
 import json
 from logging import Logger
-from typing import Dict, List, Optional, Union
+from typing import Any, Dict, List, Optional, Union
 
 from isabelle_client.socket_communication import (
     IsabelleResponse,
@@ -53,7 +53,9 @@ async def execute_command(
         executes a command and waits for results
 
         >>> from unittest.mock import Mock, patch, AsyncMock
-        >>> isabelle_client = IsabelleClient("localhost", 1000, "test")
+        >>> logger = Mock()
+        >>> logger.info = Mock()
+        >>> isabelle_client = IsabelleClient("localhost", 1000, "test", logger)
         >>> res = AsyncMock(return_value=IsabelleResponse(
         ...    "FINISHED", '{"session_id": "session_id__42"}', 42
         ... ))
@@ -80,6 +82,8 @@ async def execute_command(
         [call('localhost', 1000)]
         >>> print(test_writer.write.mock_calls)
         [call(b'test\\ntest\\n')]
+        >>> print(logger.info.mock_calls)
+        [call('test\\ntest\\n')]
 
         :param command: a full text of a command to ``isabelle``
         :param asynchronous: if ``False``, waits for ``OK``; else waits for
@@ -92,16 +96,20 @@ async def execute_command(
             else {"OK", "ERROR"}
         )
         reader, writer = await asyncio.open_connection(self.address, self.port)
-        writer.write(f"{self.password}\n{command}\n".encode("utf-8"))
+        command = f"{self.password}\n{command}\n"
+        writer.write(command.encode("utf-8"))
         await writer.drain()
+        if self.logger is not None:
+            self.logger.info(command)
         response = await get_final_message(reader, final_message, self.logger)
         return response
 
     def session_build(
         self,
         session: str,
         dirs: List[str] = None,
-        options: List[str] = None,
+        verbose: bool = False,
+        **kwargs,
     ) -> IsabelleResponse:
         """
         build a session from ROOT file
@@ -114,26 +122,31 @@ def session_build(
         ...     )
         ... )
         >>> print(isabelle_client.session_build(
-        ...     session="test_session", dirs=["."], options=[]
+        ...     session="test_session", dirs=["."], verbose=True, options=[]
         ... ))
         FINISHED {"ok": true}
 
         :param session: a name of the session from ROOT file
         :param dirs: where to look for ROOT files
-        :param options: additional options
+        :param verbose: set to ``True`` for extra verbosity
+        :param kwargs: additional arguments
+            (see Isabelle System manual for details)
         :returns: an ``isabelle`` response
         """
-        arguments: Dict[str, Union[str, List[str]]] = {"session": session}
+        arguments: Dict[str, Union[str, List[str], bool]] = {
+            "session": session,
+            "verbose": verbose,
+        }
         if dirs is not None:
             arguments["dirs"] = dirs
-        if options is not None:
-            arguments["options"] = options
+        for name in kwargs:
+            arguments[name] = kwargs[name]
         response = asyncio.run(
             self.execute_command(f"session_build {json.dumps(arguments)}")
         )
         return response
 
-    def session_start(self, session_image: str = "HOL") -> str:
+    def session_start(self, session: str = "HOL", **kwargs) -> str:
         """
         start a new session
 
@@ -149,17 +162,21 @@ def session_start(self, session_image: str = "HOL") -> str:
         >>> isabelle_client.execute_command = AsyncMock(
         ...     return_value=IsabelleResponse("OK", "OK")
         ... )
-        >>> print(isabelle_client.session_start())
+        >>> print(isabelle_client.session_start(verbose=True))
         Traceback (most recent call last):
             ...
         ValueError: Unexpected response type: OK
 
-        :param session_image: a name of a session image
+        :param session: a name of a session to start
+        :param kwargs: additional arguments
+            (see Isabelle System manual for details)
         :returns: a ``session_id``
         """
-        arguments = json.dumps({"session": session_image})
+        arguments = {"session": session}
+        for name in kwargs:
+            arguments[name] = kwargs[name]
         response = asyncio.run(
-            self.execute_command(f"session_start {arguments}")
+            self.execute_command(f"session_start {json.dumps(arguments)}")
         )
         if response.response_type == "FINISHED":
             return json.loads(response.response_body)["session_id"]
@@ -192,7 +209,7 @@ def use_theories(
         theories: List[str],
         session_id: Optional[str] = None,
         master_dir: Optional[str] = None,
-        watchdog_timeout: Optional[int] = None,
+        **kwargs,
     ) -> IsabelleResponse:
         """
         run the engine on theory files
@@ -215,7 +232,8 @@ 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
+        :param kwargs: additional arguments
+            (see Isabelle System manual for details)
         :returns: ``isabelle`` server response
         """
         new_session_id = (
@@ -225,8 +243,8 @@ def use_theories(
             "session_id": new_session_id,
             "theories": theories,
         }
-        if watchdog_timeout is not None:
-            arguments["watchdog_timeout"] = watchdog_timeout
+        for name in kwargs:
+            arguments[name] = kwargs[name]
         if master_dir is not None:
             arguments["master_dir"] = master_dir
         response = asyncio.run(
@@ -236,7 +254,7 @@ def use_theories(
             self.session_stop(new_session_id)
         return response
 
-    def echo(self, message: str) -> IsabelleResponse:
+    def echo(self, message: Any) -> IsabelleResponse:
         """
         asks a server to echo a message
 
@@ -284,7 +302,11 @@ def help(self) -> IsabelleResponse:
         return response
 
     def purge_theories(
-        self, session_id: str, theories: List[str]
+        self,
+        session_id: str,
+        theories: List[str],
+        master_dir: Optional[str] = None,
+        purge_all: Optional[bool] = None,
     ) -> IsabelleResponse:
         """
         asks a server to purge listed theories from it
@@ -296,15 +318,27 @@ def purge_theories(
         ...         "OK", json.dumps({"purged": [], "retained": []})
         ...     )
         ... )
-        >>> test_response = isabelle_client.purge_theories("test", [])
+        >>> test_response = isabelle_client.purge_theories(
+        ...     "test", [], "dir", True
+        ... )
         >>> print(test_response.response_body)
         {"purged": [], "retained": []}
 
         :param session_id: an ID of the session from which to purge theories
         :param theories: a list of theory names to purge from the server
+        :param master_dir:  the master directory as in ``use_theories``
+        :param purge_all: set to ``True`` attempts to purge all presently
+            loaded theories
         :returns: ``isabelle`` server response
         """
-        arguments = {"session_id": session_id, "theories": theories}
+        arguments: Dict[str, Union[str, List[str], bool]] = {
+            "session_id": session_id,
+            "theories": theories,
+        }
+        if master_dir is not None:
+            arguments["master_dir"] = master_dir
+        if purge_all is not None:
+            arguments["all"] = purge_all
         response = asyncio.run(
             self.execute_command(
                 f"purge_theories {json.dumps(arguments)}", asynchronous=False

pyproject.toml

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