Package Documentation

Isabelle Client

A Python client to Isabelle server

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

A TCP client for an Isabelle server.

Parameters:

  • address – IP or a domain name

  • port – a port number on which the server listens

  • password – a password to access the server through TCP

  • logger – a Python logger to store all requests to and replies from the server

cancel(task: str) → SimpleIsabelleResponse

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)
response_type=<IsabelleResponseType.OK: 'OK'>
Parameters:

task – a task ID

Returns:

Isabelle server response

echo(message: str | list | dict) → 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")
>>> isabelle_client = IsabelleClient(
...     "localhost", 9999, "test_password", logger
... )
>>> test_response = asyncio.run(
...     isabelle_client.execute_command("unknown command")
... )
>>> print(test_response[-1].response_type.value)
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":"Isabelle2025-2"}'),
 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[HelpResult]

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[PurgeTheoriesResponse]

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.model_dump())
{'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, preferences: str | None = None, options: list[str] | None = None, dirs: list[str] | None = None, include_sessions: list[str] | None = None, verbose: bool = False) → list[TaskOK | SessionBuildRegularResponse | SessionBuildErrorResponse | NotificationResponse | NodesStatusResponse]

Build a session from ROOT file.

>>> isabelle_client = IsabelleClient(
...     "localhost", 9999, "test_password"
... )
>>> print(isabelle_client.session_build(
...     session="test_session", preferences=""
... )[-1])
403
FINISHED {"ok":true,"return_code":0,"sessions":[{"session":"Pure",...}
Parameters:

  • session – a name of the session from ROOT file

  • preferences – references are loaded from the file $ISABELLE_HOME_USER/etc/preferences by default

  • options – individual updates to preferences of the form the name=value or name (the latter abbreviates name=true); see also command-line option -o for isabelle build.

  • dirs – additional directories for session ROOT and ROOTS files

  • include_sessions – field specifies sessions whose theories should be included in the overall name space of session-qualified theory names.

  • verbose – set to True for extra verbosity

Returns:

an Isabelle response

session_start(session: str = 'Main', preferences: str | None = None, options: list[str] | None = None, dirs: list[str] | None = None, include_sessions: list[str] | None = None, verbose: bool = False, print_mode: list[str] | None = None) → list[TaskOK | SessionStartRegularResponse | SessionStartErrorResponse | NotificationResponse | NodesStatusResponse]

Start a new session.

>>> isabelle_client = IsabelleClient("localhost", 9999, "test")
>>> print(
...    isabelle_client.session_start(
...        preferences=[])[-1].response_body.session_id)
167dd6d8-1eeb-4315-8022-c8c527d9bd87
Parameters:

  • session – a name of a session to start

  • preferences – references are loaded from the file $ISABELLE_HOME_USER/etc/preferences by default

  • options – individual updates to preferences of the form the name=value or name (the latter abbreviates name=true); see also command-line option -o for isabelle build.

  • dirs – additional directories for session ROOT and ROOTS files

  • include_sessions – field specifies sessions whose theories should be included in the overall name space of session-qualified theory names.

  • verbose – set to True for extra verbosity

  • print_mode – identifiers of print modes to be made active for this session

Returns:

Isabelle server response

session_stop(session_id: str) → list[TaskOK | SessionStopErrorResponse | SessionStopRegularResponse | NotificationResponse]

Stop session with given ID.

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

session_id – a string ID of a session

Returns:

Isabelle server response

shutdown() → SimpleIsabelleResponse

Ask a server to shutdown immediately.

>>> isabelle_client = IsabelleClient("localhost", 9999, "test")
>>> test_response = isabelle_client.shutdown()
>>> print(test_response)
response_type=<IsabelleResponseType.OK: 'OK'>
Returns:

Isabelle server response

use_theories(session_id: str, theories: list[str], master_dir: str | None = None, pretty_margin: float = 76.0, unicode_symbols: bool | None = None, export_pattern: str | None = None, check_delay: float = 0.5, check_limit: int | None = None, watchdog_timeout: float = 600.0, nodes_status_delay: float = -1.0) → list[TaskOK | UseTheoriesResponse | UseTheoriesErrorResponse | NodesStatusResponse]

Run the engine on theory files.

>>> isabelle_client = IsabelleClient("localhost", 9999, "test")
>>> test_response = isabelle_client.use_theories(
...     session_id="test", theories=["Mock"], master_dir="test"
... )
>>> print(test_response[-1].response_type.value)
FINISHED
Parameters:

  • session_id – an ID of a session; if None, a new session is created and then destroyed after trying to process theories

  • theories – names of theory files (without extensions!)

  • master_dir – where to look for theory files; if None, uses a temp folder of the session

  • pretty_margin – pretty formatting of emitted messages

  • unicode_symbols – use Unicode symbols in emitted messages

  • export_pattern – see the Isabelle server manual for details

  • check_delay – status of PIDE processing is checked every check_delay seconds

  • check_limit – bound on PIDE processing check attempts, 0 for unbounded

  • watchdog_timeout – the timespan (in seconds) after the last command status change of Isabelle/PIDE, before finishing with a potentially non-terminating or deadlocked execution

  • nodes_status_delay – enables continuous notifications if positive (in seconds)

Returns:

Isabelle server response

Socket Communication

A collection of functions for TCP communication.

async isabelle_client.socket_communication.get_final_message(reader: StreamReader, final_message: set[IsabelleResponseType], logger: Logger | None = None) → AsyncGenerator[IsabelleResponse]

Get responses from Isabelle server.

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

>>> test_logger = getfixture("mock_logger")
>>> async def awaiter():
...     test_reader, test_writer = await asyncio.open_connection(
...     "localhost", 9999
... )
...     test_writer.write(b"test_password\nhelp\n")
...     await get_response_from_isabelle(test_reader)
...     result = []
...     async for message in get_final_message(
...         test_reader, {IsabelleResponseType.OK}, test_logger
...     ):
...         result.append(message)
...     return result
>>> for response in asyncio.run(awaiter()):
...     print(response)
118
OK ["cancel","echo","help","purge_theories","session_build",...]
>>> print(test_logger.info.mock_calls)
[call('118\nOK ["cancel","echo","help","purge_theories","session...')]
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

Yields:

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":"Isabelle2025-2"}', '118\nO...]
>>> 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() → None

Return something weird.

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

A dummy handler to mock Isabelle server.

handle() → None

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.get_or_create_working_directory(working_directory: str | None) → Path

Get existing or create a randomly named directory.

Parameters:

working_directory – directory name

Returns:

(possibly new) directory name

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.

>>> import os
>>> os.environ["PATH"] = "src/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.

Parameters:

working_directory – a directory for storing the server logs, temporary theory files etc.

>>> import os
>>> os.environ["PATH"] = "src/isabelle_client/resources:$PATH"
>>> connector = IsabelleConnector()
>>> print(connector.working_directory)
/...
>>> connector.build_theory(
...     'lemma "\<forall> x. \<exists> y. x = y" by auto', theory="Mock")
>>> connector.build_theory(
...     'lemma "\<forall> x. \<forall> y. x = y" by auto', theory="Fail")
Traceback (most recent call last):
 ...
isabelle...Error: Failed to finish proof\<^here>:
goal (1 subgoal):
 1. \<And>x y. x = y
build_theory(theory_body: str, imports: Sequence[str] = ('Main',), theory: str | None = None) → None

Build a theory using the Isabelle server.

Parameters:

  • theory_body – theory body (goes between begin and end keywords)

  • imports – which theories to import

  • theory – (for tests) fixed named for theory file

Raises:

IsabelleTheoryError – if validation failed

property working_directory: str

Working directory.

exception isabelle_client.isabelle_connector.IsabelleTheoryError

Raised when the Isabelle response contains errors.

Data Models

class isabelle_client.data_models.ErrorMessage(*, kind: str = 'error', message: str)

Error message.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

class isabelle_client.data_models.Export(*, name: str, base64: bool, body: str)

Export.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

class isabelle_client.data_models.HelpResult(*, response_type: IsabelleResponseType, response_body: list[str], response_length: int | None = None)

Result of the help command.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

class isabelle_client.data_models.IsabelleResponse(*, response_type: IsabelleResponseType, response_body: Any, response_length: int | None = None)

A response from an Isabelle server.

response_body

a JSON-formatted response

response_length

a length of JSON response

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

class isabelle_client.data_models.IsabelleResponseType(value)

Isabelle server response type.

class isabelle_client.data_models.Message(*, kind: str, message: str, pos: Position | None = None)

Message.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

class isabelle_client.data_models.MessageNotification(*, kind: str, message: str, pos: Position | None = None, task: str)

Message notification.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

class isabelle_client.data_models.Node(*, node_name: str, theory_name: str)

Theory node.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

class isabelle_client.data_models.NodeResult(*, node_name: str, theory_name: str, status: NodeStatus, messages: list[Message], exports: list[Export])

Node result.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

class isabelle_client.data_models.NodeStatus(*, ok: bool, total: int, unprocessed: int, running: int, warned: int, failed: int, finished: int, canceled: bool, consolidated: bool, percentage: int)

Represents a formal theory node status.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

class isabelle_client.data_models.NodeStatusWithName(*, node_name: str, theory_name: str, status: NodeStatus)

Node status for nodes_status notes.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

class isabelle_client.data_models.NodesStatus(*, kind: str = 'nodes_status', nodes_status: list[NodeStatusWithName])

Nodes status notification.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

class isabelle_client.data_models.NodesStatusResponse(*, response_type: IsabelleResponseType, response_body: NodesStatus, response_length: int | None = None)

Response with nodes_status notification.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

class isabelle_client.data_models.NotificationResponse(*, response_type: IsabelleResponseType, response_body: TheoryProgressNotification | MessageNotification, response_length: int | None = None)

Notification response.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

class isabelle_client.data_models.Position(*, line: int | None = None, offset: int | None = None, end_offset: int | None = None, file: str | None = None, id: int | None = None)

Describes a source position within Isabelle text.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

class isabelle_client.data_models.PurgeTheoriesResponse(*, response_type: IsabelleResponseType, response_body: PurgeTheoriesResult, response_length: int | None = None)

Response of purge_theories command.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

class isabelle_client.data_models.PurgeTheoriesResult(*, purged: list[Node], retained: list[Node])

Result of purge_theories command.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

class isabelle_client.data_models.SessionBuildErrorResponse(*, response_type: IsabelleResponseType, response_body: SessionBuildErrorResult, response_length: int | None = None)

Error response of session_build command.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

class isabelle_client.data_models.SessionBuildErrorResult(*, ok: bool, return_code: int, sessions: list[SessionBuildResult], kind: str = 'error', message: str, task: str, response_type: IsabelleResponseType = IsabelleResponseType.FAILED)

Session build error result.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

class isabelle_client.data_models.SessionBuildRegularResponse(*, response_type: IsabelleResponseType, response_body: SessionBuildRegularResult, response_length: int | None = None)

Regular response of session_build command.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

class isabelle_client.data_models.SessionBuildRegularResult(*, ok: bool, return_code: int, sessions: list[SessionBuildResult], task: str, response_type: IsabelleResponseType = IsabelleResponseType.FINISHED)

Session build regular result.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

class isabelle_client.data_models.SessionBuildResult(*, session: str, ok: bool, return_code: int, timeout: bool, timing: Timing)

Session build result.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

class isabelle_client.data_models.SessionBuildResults(*, ok: bool, return_code: int, sessions: list[SessionBuildResult])

Session build results.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

class isabelle_client.data_models.SessionStartErrorResponse(*, response_type: IsabelleResponseType, response_body: SessionStartErrorResult, response_length: int | None = None)

Error response of session_start command.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

class isabelle_client.data_models.SessionStartErrorResult(*, kind: str = 'error', message: str, task: str, response_type: IsabelleResponseType = IsabelleResponseType.FAILED)

Session start error result.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

class isabelle_client.data_models.SessionStartRegularResponse(*, response_type: IsabelleResponseType, response_body: SessionStartRegularResult, response_length: int | None = None)

Regular response of session_start command.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

class isabelle_client.data_models.SessionStartRegularResult(*, task: str, session_id: str, tmp_dir: str)

Regular result of session_start command.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

class isabelle_client.data_models.SessionStopErrorResponse(*, response_type: IsabelleResponseType, response_body: SessionStopErrorResult, response_length: int | None = None)

Error response of session_stop command.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

class isabelle_client.data_models.SessionStopErrorResult(*, ok: bool, return_code: int, kind: str = 'error', message: str, task: str, response_type: IsabelleResponseType = IsabelleResponseType.FAILED)

Session stop regular result.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

class isabelle_client.data_models.SessionStopRegularResponse(*, response_type: IsabelleResponseType, response_body: SessionStopRegularResult, response_length: int | None = None)

Regular response of session_stop command.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

class isabelle_client.data_models.SessionStopRegularResult(*, ok: bool, return_code: int, task: str, response_type: IsabelleResponseType = IsabelleResponseType.FINISHED)

Session stop regular result.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

class isabelle_client.data_models.SessionStopResult

Session stop result.

class isabelle_client.data_models.SimpleIsabelleResponse(*, response_type: IsabelleResponseType)

Isabelle response with no body.

response_type

an all capitals word like FINISHED or ERROR

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

class isabelle_client.data_models.Task(*, task: str)

Identifies a newly created asynchronous task.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

class isabelle_client.data_models.TaskOK(*, response_type: IsabelleResponseType, response_body: Task, response_length: int | None = None)

Immediate result of task creation.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

class isabelle_client.data_models.TheoryProgress(*, kind: str = 'writeln', message: str, theory: str, session: str, percentage: int | None = None)

Theory progress.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

class isabelle_client.data_models.TheoryProgressNotification(*, kind: str = 'writeln', message: str, theory: str, session: str, percentage: int | None = None, task: str)

Theory progress notification.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

class isabelle_client.data_models.Timing(*, elapsed: float, cpu: float, gc: float)

Isabelle timing information in seconds.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

class isabelle_client.data_models.UseTheoriesErrorResponse(*, response_type: IsabelleResponseType, response_body: UseTheoriesErrorResult, response_length: int | None = None)

Error response of use_theories command.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

class isabelle_client.data_models.UseTheoriesErrorResult(*, kind: str = 'error', message: str, task: str, response_type: IsabelleResponseType = IsabelleResponseType.FAILED)

Error result of use_theories command.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

class isabelle_client.data_models.UseTheoriesResponse(*, response_type: IsabelleResponseType, response_body: UseTheoriesResults, response_length: int | None = None)

Final response of use_theories command.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

class isabelle_client.data_models.UseTheoriesResults(*, ok: bool, errors: list[Message], nodes: list[NodeResult])

Regular result of use_theories command.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].