Package Documentation#

Isabelle Client#

A Python client to Isabelle server

class isabelle_client.isabelle__client.AsynchronousResultType(value)#: Asynchronous results of a server reply.

class isabelle_client.isabelle__client.IsabelleClient(address: str, port: int, password: str, logger: Logger | None = None)#

A TCP client for an Isabelle server.

cancel(task: str) → List[IsabelleResponse]#

Ask a server to try to cancel a task with a given ID.

>>> isabelle_client = IsabelleClient("localhost", 9999, "test")
>>> test_response = isabelle_client.cancel("test_task")
>>> print(test_response[-1].response_body)

Parameters:: task – a task ID
Returns:: Isabelle server response

echo(message: Any) → List[IsabelleResponse]#

Ask a server to echo a message.

>>> isabelle_client = IsabelleClient("localhost", 9999, "test")
>>> test_response = isabelle_client.echo("test_message")
>>> print(test_response[-1].response_body)
"test_message"

Parameters:: message – any text
Returns:: Isabelle server response

async execute_command(command: str, asynchronous: bool = True) → List[IsabelleResponse]#

Execute a command and waits for results.

>>> logger = getfixture("mock_logger")  # noqa: F821
>>> isabelle_client = IsabelleClient(
...     "localhost", 9999, "test_password", logger
... )
>>> test_response = asyncio.run(
...     isabelle_client.execute_command("unknown command")
... )
>>> print(test_response[-1].response_type)
ERROR
>>> print(test_response[-1].response_body)
"Bad command 'unknown'"
>>> # error messages don't return the response length
>>> print(test_response[-1].response_length)
None
>>> print(logger.info.mock_calls)
[call('test_password\nunknown command\n'),
 call('OK {"isabelle_id":"mock","isabelle_name":"Isabelle2022"}'),
 call('ERROR "Bad command \'unknown\'"')]

Parameters:

command – a full text of a command to Isabelle
asynchronous – if False, waits for OK; else waits for FINISHED

Returns:

a list of Isabelle server responses

help() → List[IsabelleResponse]#

Ask a server to display the list of available commands.

>>> isabelle_client = IsabelleClient("localhost", 9999, "test")
>>> test_response = isabelle_client.help()
>>> print(test_response[-1].response_body)
["cancel","echo","help","purge_theories","session_build",...]

Returns:: Isabelle server response

purge_theories(session_id: str, theories: List[str], master_dir: str | None = None, purge_all: bool | None = None) → List[IsabelleResponse]#

Ask a server to purge listed theories from it.

>>> isabelle_client = IsabelleClient("localhost", 9999, "test")
>>> test_response = isabelle_client.purge_theories(
...     "test", [], "dir", True
... )
>>> print(test_response[-1].response_body)
{"purged":[{"node_name":"/tmp/Mock.thy",...}],"retained":[]}

Parameters:

session_id – an ID of the session from which to purge theories
theories – a list of theory names to purge from the server
master_dir – the master directory as in use_theories
purge_all – set to True attempts to purge all presently loaded theories

Returns:

Isabelle server response

session_build(session: str, dirs: List[str] | None = None, verbose: bool = False, **kwargs) → List[IsabelleResponse]#

Build a session from ROOT file.

>>> isabelle_client = IsabelleClient(
...     "localhost", 9999, "test_password"
... )
>>> print(isabelle_client.session_build(
...     session="test_session", dirs=["."], verbose=True, options=[]
... )[-1])
400
FINISHED {"ok":true,"return_code":0,"sessions":[{"session":"Pure",...}

Parameters:

session – a name of the session from ROOT file
dirs – where to look for ROOT files
verbose – set to True for extra verbosity
kwargs – additional arguments (see Isabelle System manual for details)

Returns:

an Isabelle response

session_start(session: str = 'Main', **kwargs) → str#

Start a new session.

>>> isabelle_client = IsabelleClient("localhost", 9998, "test")
>>> print(isabelle_client.session_start(verbose=True))
Traceback (most recent call last):
    ...
ValueError: Unexpected response type: ERROR
>>> isabelle_client = IsabelleClient("localhost", 9999, "test")
>>> print(isabelle_client.session_start())
167dd6d8-1eeb-4315-8022-c8c527d9bd87

Parameters:

session – a name of a session to start
kwargs – additional arguments (see Isabelle System manual for details)

Returns:

a session_id

Raises:

ValueError – if the server response is malformed

session_stop(session_id: str) → List[IsabelleResponse]#

Stop session with given ID.

>>> isabelle_client = IsabelleClient("localhost", 9999, "test")
>>> test_response = isabelle_client.session_stop("test")
>>> print(test_response[-1].response_type)
FINISHED

Parameters:: session_id – a string ID of a session
Returns:: Isabelle server response

shutdown() → List[IsabelleResponse]#

Ask a server to shutdown immediately.

>>> isabelle_client = IsabelleClient("localhost", 9999, "test")
>>> test_response = isabelle_client.shutdown()
>>> print(test_response[-1].response_body)

Returns:: Isabelle server response

use_theories(theories: List[str], session_id: str | None = None, master_dir: str | None = None, **kwargs) → List[IsabelleResponse]#

Run the engine on theory files.

>>> isabelle_client = IsabelleClient("localhost", 9999, "test")
>>> test_response = isabelle_client.use_theories(
...     ["Mock"], master_dir="test", watchdog_timeout=0
... )
>>> print(test_response[-1].response_type)
FINISHED

Parameters:

theories – names of theory files (without extensions!)
session_id – an ID of a session; if None, a new session is created and then destroyed after trying to process theories
master_dir – where to look for theory files; if None, uses a temp folder of the session
kwargs – additional arguments (see Isabelle System manual for details)

Returns:

Isabelle server response

class isabelle_client.isabelle__client.SynchronousResultType(value)#: Synchronous results of a server reply.

Socket Communication#

A collection of functions for TCP communication.

class isabelle_client.socket_communication.IsabelleResponse(response_type: str, response_body: str, response_length: int | None = None)#

A response from an Isabelle server.

Parameters:

response_type – an all capitals word like FINISHED or ERROR
response_body – a JSON-formatted response
response_length – a length of JSON response

async isabelle_client.socket_communication.get_final_message(reader: StreamReader, final_message: Set[str], logger: Logger | None = None) → List[IsabelleResponse]#

Get responses from Isabelle server.

(until a message of specified ‘final’ type arrives)

>>> test_logger = getfixture("mock_logger")  # noqa: F821
>>> async def awaiter():
...     test_reader, test_writer = await asyncio.open_connection(
...     "localhost", 9999
... )
...     test_writer.write(b"test_password\nhelp\n")
...     result = await get_final_message(
...         test_reader, {"OK"}, test_logger
...     )
...     return result
>>> for response in asyncio.run(awaiter()):
...     print(response)
OK {"isabelle_id":"mock","isabelle_name":"Isabelle2022"}
118
OK ["cancel","echo","help","purge_theories","session_build",...]
>>> print(test_logger.info.mock_calls)
[call('OK {"isabelle_id":"mock","isabelle_name":"Isabelle2022"}'),
 call('118\nOK ["cancel","echo","help","purge_theories","session_buil...')]

Parameters:

reader – a StreamReader connected to Isabelle server
final_message – a set of possible final message types
logger – a logger where to send all server replies

Returns:

the final response from Isabelle server

async isabelle_client.socket_communication.get_response_from_isabelle(reader: StreamReader) → IsabelleResponse#

Get a response from Isabelle server.

Format:

a carriage-return delimited message or
a fixed length message after a carriage-return delimited message with only one integer number denoting length

>>> async def awaiter():
...     test_reader, test_writer = await asyncio.open_connection(
...     "localhost", 9999
... )
...     test_writer.write(b"test_password\nhelp\n")
...     result = [str(await get_response_from_isabelle(test_reader))]
...     result += [str(await get_response_from_isabelle(test_reader))]
...     return result
>>> print(asyncio.run(awaiter()))
['OK {"isabelle_id":"mock","isabelle_name":"Isabelle2022"}', '118\nOK [...]
>>> async def awaiter():
...     test_reader, test_writer = await asyncio.open_connection(
...     "localhost", 9998
... )
...     test_writer.write(b"test_password\nhelp\n")
...     result = [str(await get_response_from_isabelle(test_reader))]
...     result += [str(await get_response_from_isabelle(test_reader))]
...     return result
>>> print(asyncio.run(awaiter()))
Traceback (most recent call last):
  ...
ValueError: Unexpected response from Isabelle: # !!!

Parameters:: reader – a StreamReader connected to a server
Returns:: a response from Isabelle
Raises:: ValueError – if the server response is malformed

Utilities#

A collection of different useful functions.

class isabelle_client.utils.BuggyDummyTCPHandler(request, client_address, server)#

A dummy handler to mock bugs in Isabelle server response.

handle()#: Return something weird.

class isabelle_client.utils.DummyTCPHandler(request, client_address, server)#

A dummy handler to mock Isabelle server.

handle()#: Return something similar to what Isabelle server does.

class isabelle_client.utils.IsabelleServerCommands(value)#: Supported Isabelle server commands.

class isabelle_client.utils.ReusableDummyTCPServer(server_address, RequestHandlerClass, bind_and_activate=True)#: Ignore TIME-WAIT during testing.

isabelle_client.utils.get_isabelle_client(server_info: str) → IsabelleClient#

Get an instance of IsabelleClient from server info.

>>> server_inf = 'server "test" = 127.0.0.1:10000 (password "pass")'
>>> print(get_isabelle_client(server_inf).port)
10000
>>> get_isabelle_client("wrong")
Traceback (most recent call last):
    ...
ValueError: Unexpected server info: wrong

Parameters:: server_info – a line returned by a server on start
Returns:: an Isabelle client
Raises:: ValueError – if the server response is malformed

isabelle_client.utils.start_isabelle_server(log_file: str | None = None, name: str | None = None, port: int | None = None) → Tuple[str, Process]#

Start Isabelle server.

>>> os.environ["PATH"] = "isabelle_client/resources:$PATH"
>>> print(start_isabelle_server()[0])
server "isabelle" = 127.0.0.1:9999 (password "test_password")

Parameters:

log_file – a log file for exceptional output of internal server and session operations
name – explicit server name (default: isabelle)
port – explicit server port

Returns:

a line of server info and server process

isabelle_client.utils.start_isabelle_server_win32(args: str) → Tuple[str, Process]#

Start Isabelle server on Windows.

Parameters:: args – Isabelle server arguments string
Returns:: a line of server info and server process

Isabelle Connector#

A connector to the Isabelle server, hiding server interactions.

class isabelle_client.isabelle_connector.IsabelleConnector(working_directory: str | None = None)#

A connector to the Isabelle server, hiding server interactions.

>>> os.environ["PATH"] = "isabelle_client/resources:$PATH"
>>> connector = IsabelleConnector()
>>> print(connector.working_directory)
/...
>>> connector.verify_lemma(
...     "\<forall> x. \<exists> y. x = y", theory="Mock")
True
>>> connector.verify_lemma(
...     "\<forall> x. \<forall> y. x = y", theory="Fail")
Traceback (most recent call last):
 ...
isabelle...Error: Failed to finish proof\<^here>:
goal (1 subgoal):
 1. \<And>x y. x = y

verify_lemma(lemma_text: str, task: str = 'by auto', theory: str | None = None) → bool#

Verify a lemma statement using the Isabelle server.

Parameters:

lemma_text – (hopefully) syntactically valid Isabelle lemma
task – how to prove lemma. "by auto" by default
theory – (for tests) fixed named for theory file

Returns:

True if validation successful

Raises:

IsabelleTheoryError – if validation failed

property working_directory: str#: Get working directory.

exception isabelle_client.isabelle_connector.IsabelleTheoryError#: Raised when the Isabelle response contains errors.