Merge pull request #44 from inpefess/maintenance

Maintenance

.circleci/config.yml

@@ -26,20 +26,19 @@ jobs:
           command: |
             . venv/bin/activate
             pytest --cov isabelle_client --cov-report xml --cov-fail-under=99\
-                   --junit-xml test-results/isabelle-client.xml isabelle_client\
-                   tests
+                   --junit-xml test-results/isabelle-client.xml isabelle_client
       - run:
           name: run linters
           command: |
             . venv/bin/activate
             pycodestyle --max-doc-length 160 --ignore E203,E501,W503\
-                        isabelle_client tests examples
+                        isabelle_client examples
             pylint --rcfile=.pylintrc isabelle_client examples
       - run:
           name: run type checks
           command: |
             . venv/bin/activate
-            mypy --config-file mypy.ini isabelle_client tests examples
+            mypy --config-file mypy.ini isabelle_client examples
       - run:
           name: upload data to codecov
           command: |

.dockerignore

@@ -11,7 +11,7 @@ examples/document/
 ./**/*.log
 ./**/*.*~
 ./**/*~
-show_report.sh
+local-build.sh
 ./**/.ini
 ./**/.yml
 ./**/.toml

.gitignore

@@ -15,3 +15,5 @@ doc/build/
 *.aux
 *.cicmauthinsts
 .ipynb_checkpoints/
+flycheck_*.*
+.dir-locals.el

README.rst

@@ -6,7 +6,7 @@ Python client for Isabelle server
 ``isabelle-client`` is a TCP 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>`__.
+manual <https://isabelle.in.tum.de/dist/Isabelle2021-1/doc/system.pdf>`__.
 
 How to Install
 ==============
@@ -56,7 +56,7 @@ are welcome. To start:
 
 To check the code quality before creating a pull request, one might run
 the script
-`show_report.sh <https://github.com/inpefess/isabelle-client/blob/master/show_report.sh>`__.
+`local-build.sh <https://github.com/inpefess/isabelle-client/blob/master/local-build.sh>`__.
 It locally does nearly the same as the CI pipeline after the PR is
 created.
 

doc/source/usage-example.rst

@@ -21,22 +21,41 @@ In what case to use
 
 This client might be useful if:
 
-* you have an Isabelle server instance running
+* you have a machine with Isabelle installed
 * you have scripts for automatic generation of theory files in Python
 * you want to communicate with the server not using Scala and/or StandardML
 
-First, we need to start an Isabelle server::
+In what environment to use
+==========================
+
+The client works well in scripts and in Jupyter notebooks. For the latter, one have to first enable nested event loops::
+
+
+    import nest_asyncio
+
+    nest_asyncio.apply()
+    
+.. warning::
+   When using `start_isabelle_server <package-documentation.html#isabelle_client.utils.start_isabelle_server>`__ utility function in Python REPL or terminal IPython, shutting the server down within the same session is known to cause a runtime error on exit from the session. This behavious is related to a `well known issue <https://ipython.readthedocs.io/en/stable/interactive/autoawait.html#difference-between-terminal-ipython-and-ipykernel>`__.
+
+Starting Isabelle server
+========================
+
+First, we need to start an Isabelle server (doesn't work on Windows)::
   
     from isabelle_client import start_isabelle_server
 
     server_info, _ = start_isabelle_server(
         name="test", port=9999, log_file="server.log"
     )
 
-We could also start the server outside this script and use its info::
+We could also start the server outside this script and use its info (on Windows, this is done in Cygwin)::
 
     isabelle server > server.info
-    
+
+Interacting with Isabelle server
+================================
+
 Now let's create a client to our server ::
 
     from isabelle_client import get_isabelle_client

conftest.py → isabelle_client/conftest.py

@@ -20,7 +20,7 @@
 
 
 class BuggyTCPHandler(socketserver.BaseRequestHandler):
-    """ a dummy handler to mock bugs in Isabelle server response """
+    """a dummy handler to mock bugs in Isabelle server response"""
 
     def handle(self):
         request = self.request.recv(1024).decode("utf-8").split("\n")[0]
@@ -34,7 +34,7 @@ def handle(self):
 
 
 class DummyTCPHandler(socketserver.BaseRequestHandler):
-    """ a dummy handler to mock Isabelle server """
+    """a dummy handler to mock Isabelle server"""
 
     # pylint: disable=too-many-statements
     def handle(self):
@@ -60,14 +60,14 @@ def handle(self):
 
 
 class ReusableTCPServer(socketserver.TCPServer):
-    """ ignore TIME-WAIT during testing """
+    """ignore TIME-WAIT during testing"""
 
     allow_reuse_address = True
 
 
 @fixture(autouse=True, scope="session")
 def tcp_servers():
-    """ a simplistic TCP server mocking Isabelle server behaviour """
+    """a simplistic TCP server mocking Isabelle server behaviour"""
     with ReusableTCPServer(
         ("localhost", 9999), DummyTCPHandler
     ) as server, ReusableTCPServer(
@@ -84,7 +84,7 @@ def tcp_servers():
 
 @fixture
 def mock_logger():
-    """ a mock for logger to spy on ``info`` calls """
+    """a mock for logger to spy on ``info`` calls"""
     logger = Mock()
     logger.info = Mock()
     return logger

isabelle_client/isabelle__client.py

@@ -104,7 +104,7 @@ def session_build(
         dirs: List[str] = None,
         verbose: bool = False,
         **kwargs,
-    ) -> IsabelleResponse:
+    ) -> List[IsabelleResponse]:
         """
         build a session from ROOT file
 
@@ -165,7 +165,7 @@ def session_start(self, session: str = "HOL", **kwargs) -> str:
             f"Unexpected response type: {response_list[-1].response_type}"
         )
 
-    def session_stop(self, session_id: str) -> IsabelleResponse:
+    def session_stop(self, session_id: str) -> List[IsabelleResponse]:
         """
         stop session with given ID
 
@@ -187,7 +187,7 @@ def use_theories(
         session_id: Optional[str] = None,
         master_dir: Optional[str] = None,
         **kwargs,
-    ) -> IsabelleResponse:
+    ) -> List[IsabelleResponse]:
         """
         run the engine on theory files
 
@@ -224,7 +224,7 @@ def use_theories(
             self.session_stop(new_session_id)
         return response
 
-    def echo(self, message: Any) -> IsabelleResponse:
+    def echo(self, message: Any) -> List[IsabelleResponse]:
         """
         asks a server to echo a message
 
@@ -243,7 +243,7 @@ def echo(self, message: Any) -> IsabelleResponse:
         )
         return response
 
-    def help(self) -> IsabelleResponse:
+    def help(self) -> List[IsabelleResponse]:
         """
         asks a server to display the list of available commands
 
@@ -263,7 +263,7 @@ def purge_theories(
         theories: List[str],
         master_dir: Optional[str] = None,
         purge_all: Optional[bool] = None,
-    ) -> IsabelleResponse:
+    ) -> List[IsabelleResponse]:
         """
         asks a server to purge listed theories from it
 
@@ -296,7 +296,7 @@ def purge_theories(
         )
         return response
 
-    def cancel(self, task: str) -> IsabelleResponse:
+    def cancel(self, task: str) -> List[IsabelleResponse]:
         """
         asks a server to try to cancel a task with a given ID
 
@@ -316,7 +316,7 @@ def cancel(self, task: str) -> IsabelleResponse:
         )
         return response
 
-    def shutdown(self) -> IsabelleResponse:
+    def shutdown(self) -> List[IsabelleResponse]:
         """
         asks a server to shutdown immediately
 

isabelle_client/utils.py

@@ -59,7 +59,7 @@ def start_isabelle_server(
     start Isabelle server
 
     >>> import os
-    >>> os.environ["PATH"] = "tests:$PATH"
+    >>> os.environ["PATH"] = "isabelle_client/resources:$PATH"
     >>> print(start_isabelle_server()[0])
     server "isabelle" = 127.0.0.1:9999 (password "test_password")
     <BLANKLINE>

show_report.sh → local-build.sh

@@ -7,9 +7,9 @@ make clean html coverage
 cat build/coverage/python.txt
 cd ..
 pycodestyle --max-doc-length 160 --ignore E203,E501,W503 \
-	    ${PACKAGE_NAME} tests examples
-pylint --rcfile=.pylintrc ${PACKAGE_NAME} tests examples
-mypy --config-file mypy.ini ${PACKAGE_NAME} tests examples
+	    ${PACKAGE_NAME} examples
+pylint --rcfile=.pylintrc ${PACKAGE_NAME} examples
+mypy --config-file mypy.ini ${PACKAGE_NAME} examples
 pytest --cov ${PACKAGE_NAME} --cov-report term-missing --cov-fail-under=99 \
        --junit-xml test-results/isabelle-client.xml ${PACKAGE_NAME}
 scc -i py ${PACKAGE_NAME}