Skip to content

Commit

Permalink
Merge pull request #27 from inpefess/use-fixtures
Browse files Browse the repository at this point in the history
Use fixtures
  • Loading branch information
inpefess committed Apr 9, 2021
2 parents 2e7ee90 + ef69b35 commit c530c32
Show file tree
Hide file tree
Showing 14 changed files with 332 additions and 308 deletions.
4 changes: 2 additions & 2 deletions .circleci/config.yml
Original file line number Diff line number Diff line change
Expand Up @@ -30,8 +30,8 @@ jobs:
command: |
. venv/bin/activate
pytest --cov isabelle_client --cov-report xml --cov-fail-under=99\
--junit-xml test-results/isabelle-client.xml\
--doctest-modules isabelle_client tests
--junit-xml test-results/isabelle-client.xml isabelle_client\
tests
- run:
name: run linters
command: |
Expand Down
91 changes: 91 additions & 0 deletions conftest.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,91 @@
"""
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 socketserver
import threading
from unittest.mock import Mock

from pytest import fixture


class BuggyTCPHandler(socketserver.BaseRequestHandler):
""" a dummy handler to mock bugs in Isabelle server response """

def handle(self):
request = self.request.recv(1024).decode("utf-8").split("\n")[0]
if request == "ping":
self.request.sendall(b"5\n")
self.request.sendall(b"# !!!")
else:
self.request.sendall(b'OK "connection OK"\n')
self.request.sendall(b"7\n")
self.request.sendall(b"FAILED\n")


class DummyTCPHandler(socketserver.BaseRequestHandler):
""" a dummy handler to mock Isabelle server """

# pylint: disable=too-many-statements
def handle(self):
request = self.request.recv(1024).decode("utf-8").split("\n")[1]
command = request.split(" ")[0]
self.request.sendall(b'OK "connection OK"\n')

if command == "echo":
self.request.sendall(
f"OK{request.split(' ')[1]}\n".encode("utf-8")
)
elif command in {"shutdown", "cancel"}:
self.request.sendall(b"OK")
elif command == "purge_theories":
self.request.sendall(b'OK {"purged": [], "retained": []}')
elif command == "help":
self.request.sendall(b'OK ["echo", "help"]')
else:
self.request.sendall(b"43\n")
self.request.sendall(
b'FINISHED {"session_id": "test_session_id"}\n'
)


class ReusableTCPServer(socketserver.TCPServer):
""" 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 """
with ReusableTCPServer(
("localhost", 9999), DummyTCPHandler
) as server, ReusableTCPServer(
("localhost", 9998), BuggyTCPHandler
) as buggy_server:
thread = threading.Thread(target=server.serve_forever)
thread.daemon = True
thread.start()
buggy_thread = threading.Thread(target=buggy_server.serve_forever)
buggy_thread.daemon = True
buggy_thread.start()
yield server, buggy_server


@fixture
def mock_logger():
""" a mock for logger to spy on ``info`` calls """
logger = Mock()
logger.info = Mock()
return logger
2 changes: 1 addition & 1 deletion doc/source/conf.py
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@
author = "Boris Shminke"

# The full version, including alpha/beta/rc tags
release = "0.2.0"
release = "0.2.1"


# -- General configuration ---------------------------------------------------
Expand Down
18 changes: 9 additions & 9 deletions doc/source/usage-example.rst
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
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
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,
Expand All @@ -20,28 +20,28 @@ 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::

isabelle server > server.pid
isabelle server > server.pid

Now we can get an instance of Isabelle client to talk to this server from Python in a very simple way::

from isabelle_client import get_isabelle_client_from_server_info
from isabelle_client import get_isabelle_client_from_server_info
isabelle = get_isabelle_client_from_server_info("server.pid")
isabelle = get_isabelle_client_from_server_info("server.pid")

It might be useful to log all replies from the server somewhere, e.g.::

import logging
import logging

logging.basicConfig(filename="out.log")
isabelle.logger = logging.getLogger()
logging.basicConfig(filename="out.log")
isabelle.logger = logging.getLogger()

This client has several methods implemented to communicate with the server Python-style, e.g.::

isabelle.use_theories(theories=["Dummy"], master_dir=".")
isabelle.use_theories(theories=["Dummy"], master_dir=".")

In this command it's supposed that we have a ``Dummy.thy`` theory file in our working directory which we, e.g. generated with another Python script.

One can also issue a free-form command, e.g.::

isabelle.execute_command("echo 42", asynchronous=False)
isabelle.execute_command("echo 42", asynchronous=False)

2 changes: 1 addition & 1 deletion examples/example.py
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ def main():
""" using ``isabelle`` client """
# first, we start Isabelle server
server_info, _ = start_isabelle_server(
name="test", port="9999", log_file="server.log"
name="test", port=9999, log_file="server.log"
)
isabelle = get_isabelle_client(server_info)
# we will log all the messages from the server to a file
Expand Down
2 changes: 1 addition & 1 deletion examples/video_example/example.txt
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ 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
# we could also start the server outside this script and use its info
# now let's create a client to our server
from isabelle_client import get_isabelle_client

Expand Down
126 changes: 30 additions & 96 deletions isabelle_client/isabelle__client.py
Original file line number Diff line number Diff line change
Expand Up @@ -52,38 +52,23 @@ async def execute_command(
"""
executes a command and waits for results
>>> from unittest.mock import Mock, patch, AsyncMock
>>> logger = Mock()
>>> logger.info = Mock()
>>> isabelle_client = IsabelleClient("localhost", 1000, "test", logger)
>>> res = AsyncMock(return_value=IsabelleResponse(
... "FINISHED", '{"session_id": "session_id__42"}', 42
... ))
>>> test_writer = Mock()
>>> test_writer.drain = AsyncMock()
>>> connection = AsyncMock(return_value=(Mock(), test_writer))
>>> with (
... patch("asyncio.open_connection", connection),
... patch(
... "isabelle_client.isabelle__client.get_final_message",
... res
... )
... ):
... test_response = asyncio.run(
... isabelle_client.execute_command("test")
>>> logger = getfixture("mock_logger")
>>> isabelle_client = IsabelleClient(
... "localhost", 9999, "test_password", logger
... )
>>> test_response = asyncio.run(
... isabelle_client.execute_command("test_command")
... )
>>> print(test_response.response_type)
FINISHED
>>> print(test_response.response_body)
{"session_id": "session_id__42"}
{"session_id": "test_session_id"}
>>> print(test_response.response_length)
42
>>> print(connection.mock_calls)
[call('localhost', 1000)]
>>> print(test_writer.write.mock_calls)
[call(b'test\\ntest\\n')]
43
>>> print(logger.info.mock_calls)
[call('test\\ntest\\n')]
[call('test_password\\ntest_command\\n'),
call('OK "connection OK"'),
call('43\\nFINISHED {"session_id": "test_session_id"}')]
:param command: a full text of a command to ``isabelle``
:param asynchronous: if ``False``, waits for ``OK``; else waits for
Expand Down Expand Up @@ -114,17 +99,14 @@ def session_build(
"""
build a session from ROOT file
>>> from unittest.mock import AsyncMock
>>> isabelle_client = IsabelleClient("localhost", 1000, "test")
>>> isabelle_client.execute_command = AsyncMock(
... return_value=IsabelleResponse(
... "FINISHED", '{"ok": true}', None
... )
>>> isabelle_client = IsabelleClient(
... "localhost", 9999, "test_password"
... )
>>> print(isabelle_client.session_build(
... session="test_session", dirs=["."], verbose=True, options=[]
... ))
FINISHED {"ok": true}
43
FINISHED {"session_id": "test_session_id"}
:param session: a name of the session from ROOT file
:param dirs: where to look for ROOT files
Expand All @@ -150,22 +132,14 @@ def session_start(self, session: str = "HOL", **kwargs) -> str:
"""
start a new session
>>> from unittest.mock import AsyncMock
>>> isabelle_client = IsabelleClient("localhost", 1000, "test")
>>> isabelle_client.execute_command = AsyncMock(
... return_value=IsabelleResponse(
... "FINISHED", '{"session_id": "test_session"}', None
... )
... )
>>> print(isabelle_client.session_start())
test_session
>>> isabelle_client.execute_command = AsyncMock(
... return_value=IsabelleResponse("OK", "OK")
... )
>>> isabelle_client = IsabelleClient("localhost", 9998, "test")
>>> print(isabelle_client.session_start(verbose=True))
Traceback (most recent call last):
...
ValueError: Unexpected response type: OK
ValueError: Unexpected response type: FAILED
>>> isabelle_client = IsabelleClient("localhost", 9999, "test")
>>> print(isabelle_client.session_start())
test_session_id
:param session: a name of a session to start
:param kwargs: additional arguments
Expand All @@ -186,14 +160,10 @@ def session_stop(self, session_id: str) -> IsabelleResponse:
"""
stop session with given ID
>>> from unittest.mock import AsyncMock
>>> isabelle_client = IsabelleClient("localhost", 1000, "test")
>>> isabelle_client.execute_command = AsyncMock(
... return_value=IsabelleResponse("FAILED", "")
... )
>>> isabelle_client = IsabelleClient("localhost", 9999, "test")
>>> test_response = isabelle_client.session_stop("test")
>>> print(test_response.response_type)
FAILED
FINISHED
:param session_id: a string ID of a session
:returns: ``isabelle`` server response
Expand All @@ -214,13 +184,7 @@ def use_theories(
"""
run the engine on theory files
>>> from unittest.mock import AsyncMock
>>> isabelle_client = IsabelleClient("localhost", 1000, "test")
>>> isabelle_client.execute_command = AsyncMock(
... return_value=IsabelleResponse(
... "FINISHED", '{"session_id": "test"}'
... )
... )
>>> isabelle_client = IsabelleClient("localhost", 9999, "test")
>>> test_response = isabelle_client.use_theories(
... ["test"], master_dir="test", watchdog_timeout=0
... )
Expand Down Expand Up @@ -258,16 +222,10 @@ def echo(self, message: Any) -> IsabelleResponse:
"""
asks a server to echo a message
>>> from unittest.mock import AsyncMock
>>> isabelle_client = IsabelleClient("localhost", 1000, "test")
>>> isabelle_client.execute_command = AsyncMock(
... return_value=IsabelleResponse(
... "OK", json.dumps("test message")
... )
... )
>>> isabelle_client = IsabelleClient("localhost", 9999, "test")
>>> test_response = isabelle_client.echo("test_message")
>>> print(test_response.response_body)
"test message"
"test_message"
:param message: any text
:returns: ``isabelle`` server response
Expand All @@ -283,16 +241,10 @@ def help(self) -> IsabelleResponse:
"""
asks a server to display the list of available commands
>>> from unittest.mock import AsyncMock
>>> isabelle_client = IsabelleClient("localhost", 1000, "test")
>>> isabelle_client.execute_command = AsyncMock(
... return_value=IsabelleResponse(
... "OK", json.dumps(["help", "echo"])
... )
... )
>>> isabelle_client = IsabelleClient("localhost", 9999, "test")
>>> test_response = isabelle_client.help()
>>> print(test_response.response_body)
["help", "echo"]
["echo", "help"]
:returns: ``isabelle`` server response
"""
Expand All @@ -311,13 +263,7 @@ def purge_theories(
"""
asks a server to purge listed theories from it
>>> from unittest.mock import AsyncMock
>>> isabelle_client = IsabelleClient("localhost", 1000, "test")
>>> isabelle_client.execute_command = AsyncMock(
... return_value=IsabelleResponse(
... "OK", json.dumps({"purged": [], "retained": []})
... )
... )
>>> isabelle_client = IsabelleClient("localhost", 9999, "test")
>>> test_response = isabelle_client.purge_theories(
... "test", [], "dir", True
... )
Expand Down Expand Up @@ -350,13 +296,7 @@ def cancel(self, task: str) -> IsabelleResponse:
"""
asks a server to try to cancel a task with a given ID
>>> from unittest.mock import AsyncMock
>>> isabelle_client = IsabelleClient("localhost", 1000, "test")
>>> isabelle_client.execute_command = AsyncMock(
... return_value=IsabelleResponse(
... "OK", ""
... )
... )
>>> isabelle_client = IsabelleClient("localhost", 9999, "test")
>>> test_response = isabelle_client.cancel("test_task")
>>> print(test_response.response_body)
<BLANKLINE>
Expand All @@ -376,13 +316,7 @@ def shutdown(self) -> IsabelleResponse:
"""
asks a server to shutdown immediately
>>> from unittest.mock import AsyncMock
>>> isabelle_client = IsabelleClient("localhost", 1000, "test")
>>> isabelle_client.execute_command = AsyncMock(
... return_value=IsabelleResponse(
... "OK", ""
... )
... )
>>> isabelle_client = IsabelleClient("localhost", 9999, "test")
>>> test_response = isabelle_client.shutdown()
>>> print(test_response.response_body)
<BLANKLINE>
Expand Down

0 comments on commit c530c32

Please sign in to comment.