pysabelle.raw package

Submodules

pysabelle.raw.commands module

Raw command wrappers corresponding to each Isabelle server command.

Each method sends the appropriate command and returns a typed result.

class pysabelle.raw.commands.RawCommands(dispatcher)[source]

Bases: object

Low-level interface to Isabelle server commands.

Each method corresponds to one command defined in §§4.4 of the Isabelle System Manual. Synchronous commands return a RawReply whose payload has been parsed into the appropriate dataclass. Asynchronous commands accept an optional on_note callback for progress updates and return the final result after the task completes.

Parameters:: dispatcher (TaskDispatcher) – The TaskDispatcher used to send commands and wait for replies.

async help()[source]

Send the help command.

Return type:: list[str]
Returns:: List of available command names.

async echo(value)[source]

Send the echo command.

Parameters:: value (Any) – Any JSON-serializable value to echo.
Return type:: Any
Returns:: The same value, as echoed by the server.

async shutdown()[source]

Send the shutdown command.

Shuts down the server. No reply is expected.

Return type:: None

async cancel(task_id)[source]

Send the cancel command to interrupt a running task.

Parameters:: task_id (TaskId) – Identifier of the task to cancel.
Return type:: None

async session_build(args, on_note=None, timeout=None)[source]

Send the session_build command to build a session hierarchy.

Parameters:

args (SessionBuildArgs) – Build arguments (session name, options, …).
on_note (Callable[[RawReply], Awaitable[None]] | None) – Optional callback invoked for each NOTE message during the build.
timeout (float | None) – Optional limit in seconds (raises IsabelleTimeoutError).

Return type:

SessionBuildResults

Returns:

Aggregated build results for all required sessions.

async session_start(args, on_note=None, timeout=None)[source]

Send the session_start command to start a new PIDE session.

Parameters:

args (SessionBuildArgs) – Start arguments (session name, options, print mode, …).
on_note (Callable[[RawReply], Awaitable[None]] | None) – Optional callback invoked for each NOTE message during startup.
timeout (float | None) – Optional limit in seconds (raises IsabelleTimeoutError).

Return type:

SessionStartResult

Returns:

Result containing the new session ID and temporary directory.

async session_stop(session_id, on_note=None, timeout=None)[source]

Send the session_stop command to terminate a running session.

Parameters:

session_id (SessionId) – Identifier of the session to stop.
on_note (Callable[[RawReply], Awaitable[None]] | None) – Optional callback for NOTE messages during shutdown.
timeout (float | None) – Optional limit in seconds (raises IsabelleTimeoutError).

Return type:

SessionStopResult

Returns:

Stop result indicating success and return code.

async use_theories(args, on_note=None, timeout=None)[source]

Send the use_theories command to load and check theories.

Parameters:

args (UseTheoriesArgs) – Use-theories arguments (session ID, theory list, options, …).
on_note (Callable[[RawReply], Awaitable[None]] | None) – Optional callback for NOTE messages (progress, nodes status).
timeout (float | None) – Optional limit in seconds (raises IsabelleTimeoutError).

Return type:

UseTheoriesResults

Returns:

Results containing per-node status, messages and exports.

async purge_theories(args)[source]

Send the purge_theories command to unload theories from a session.

Parameters:: args (PurgeTheoriesArgs) – Purge arguments (session ID, theory list, all flag).
Return type:: PurgeTheoriesResults
Returns:: Result listing which theories were purged and which retained.

pysabelle.raw.dispatcher module

Asynchronous task dispatcher for multiplexing replies.

The dispatcher runs a background reader loop that receives raw replies from the transport, classifies them (OK, ERROR, NOTE, FINISHED, FAILED) and routes them to the appropriate waiting futures or callbacks.

class pysabelle.raw.dispatcher.TaskDispatcher(transport)[source]

Bases: object

Multiplexes incoming server replies to waiting callers.

The dispatcher owns a background task that continuously reads from the transport. It maintains: - a single _sync_reply future for the next synchronous reply (OK/ERROR) - a dictionary _pending mapping task UUIDs to (future, callback) for async tasks

For asynchronous commands the task is registered in _pending by the reader loop itself, at the moment it reads the immediate OK {"task": id} reply. This guarantees that NOTE/FINISHED/FAILED messages that follow immediately on the wire (possibly in the same TCP segment) are never lost.

Once the reader loop has crashed (e.g. connection lost) or the dispatcher has been stopped, new commands fail immediately with IsabelleConnectionError.

Use run_sync() for commands that return a single immediate reply. Use run_async() for commands that first return an OK with a task ID, then later a FINISHED/FAILED, possibly with intermediate NOTE messages.

Parameters:: transport (Transport) – Open transport to the server.

async start()[source]

Public API to start the dispatcher.

Return type:: None

async stop()[source]

Public API to stop the dispatcher.

Return type:: None

async run_sync(command, arg=None)[source]

Execute a synchronous command and return its immediate reply.

The command is sent while holding the command lock. The reply must be either OK or ERROR; any other kind is considered a protocol error.

Parameters:

command (str) – Name of the command (e.g., “help”, “echo”).
arg (Any) – Optional JSON-serializable argument.

Return type:

RawReply

Returns:

The raw reply (OK or ERROR).

Raises:

IsabelleCommandError – If the server replies with ERROR.
IsabelleProtocolError – If the reply is neither OK nor ERROR.

async run_async(command, arg=None, on_note=None, timeout=None)[source]

Execute an asynchronous command and wait for its terminal reply.

The command is sent; the first reply must be OK containing a task ID. Subsequent NOTE messages are delivered to on_note, and the future returned completes when FINISHED or FAILED arrives.

Parameters:

command (str) – Name of the command (e.g., “session_build”).
arg (Any) – Optional JSON-serializable argument.
on_note (Callable[[RawReply], Awaitable[None]] | None) – Callback invoked for each NOTE message belonging to this task.
timeout (float | None) – Maximum seconds to wait for the terminal reply. On timeout, and also when the awaiting coroutine is cancelled, a best-effort cancel command is sent to the server for this task.

Return type:

RawReply

Returns:

The terminal reply (FINISHED or FAILED).

Raises:

IsabelleCommandError – If the immediate reply is ERROR or the task fails.
IsabelleProtocolError – If the immediate reply is OK but lacks a task ID.
IsabelleTimeoutError – If the terminal reply does not arrive within timeout.
IsabelleTaskCancelled – If the task ends with FAILED {“message”: “Interrupt”}.

pysabelle.raw.exceptions module

Exception hierarchy for the raw protocol layer.

exception pysabelle.raw.exceptions.IsabelleError[source]

Bases: Exception

Root exception for all pYsabelle errors (protocol, server process, session).

exception pysabelle.raw.exceptions.IsabelleConnectionError[source]

Bases: IsabelleError

Raised on TCP-level failures: connection refused, EOF, or write error.

exception pysabelle.raw.exceptions.IsabelleProtocolError[source]

Bases: IsabelleError

Raised when a server message violates the §4.2 framing rules.

exception pysabelle.raw.exceptions.IsabelleCommandError(kind, argument, payload=None)[source]

Bases: IsabelleError

Raised when the server replies with ERROR or a task ends with FAILED.

Parameters:

kind (str)
argument (str)
payload (object)

Return type:

None

exception pysabelle.raw.exceptions.IsabelleTimeoutError(task_id, timeout)[source]

Bases: IsabelleError

Raised when a task does not complete within the allotted time.

Parameters:

task_id (str)
timeout (float)

Return type:

None

exception pysabelle.raw.exceptions.IsabelleTaskCancelled[source]

Bases: IsabelleError

Raised when a task ends with FAILED {"message": "Interrupt"}.

pysabelle.raw.protocol module

Low-level parsing and encoding of Isabelle server messages (§4.2, §4.3).

class pysabelle.raw.protocol.ReplyKind(value)[source]

Bases: str, Enum

Kind of server reply as defined in §4.2.3.

OK = 'OK'

ERROR = 'ERROR'

FINISHED = 'FINISHED'

FAILED = 'FAILED'

NOTE = 'NOTE'

class pysabelle.raw.protocol.RawReply(kind, argument_raw)[source]

Bases: object

A raw server reply before semantic interpretation.

Variables:

kind – The reply kind (OK, ERROR, FINISHED, FAILED, NOTE).
argument_raw – The raw argument string following the kind tag.

Parameters:

kind (ReplyKind)
argument_raw (str)

kind: ReplyKind

argument_raw: str

classmethod parse(line)[source]

Parse a single line (or the first line of a long message) into a RawReply.

Parameters:: line (str) – The reply line as received from the server (without trailing newline).
Return type:: RawReply
Returns:: A RawReply instance.
Raises:: ValueError – If the line cannot be parsed or the kind is unknown.

json()[source]

Parse argument_raw as JSON and cache the result.

Return type:: Any
Returns:: The parsed JSON object, or None if argument_raw is empty.

get(key, default=None)[source]

Convenience method to extract a key from the JSON payload.

Parameters:

key (str) – The key to look up.
default (Any) – Value to return if the payload is not a dict or key is missing.

Return type:

Any

Returns:

The value for key, or default.

property task_id: str | None: Extract the task UUID from the JSON payload, if present.

property is_ok: bool: True if kind is OK.

property is_error: bool: True if kind is ERROR.

property is_finished: bool: True if kind is FINISHED.

property is_failed: bool: True if kind is FAILED.

property is_note: bool: True if kind is NOTE.

property is_terminal: bool: True for FINISHED or FAILED (terminal async replies).

property is_async: bool: True for NOTE, FINISHED, FAILED (all replies that belong to async tasks).

pysabelle.raw.protocol.encode_long_message(text)[source]

Encode a string as a long message according to §4.2.1.

Format: <length>\n<text>\n where <length> is the decimal byte count of <text> including the trailing newline, exactly as Isabelle’s own Byte_Message.write_line_message does. An uncounted trailing newline would be read by the server as a separate empty message (which it answers with a spurious NOTE).

Parameters:: text (str) – The message content (may contain newlines).
Return type:: bytes
Returns:: Encoded bytes ready to be sent over the wire.
Raises:: ValueError – If the text is too long (internal limit not enforced here).

pysabelle.raw.protocol.encode_short_message(text)[source]

Encode a string as a short message according to §4.2.1.

Short messages must not contain newline characters. The message is sent as a single line terminated by \n.

Parameters:: text (str) – The message content (no newlines allowed).
Return type:: bytes
Returns:: Encoded bytes ready to be sent over the wire.
Raises:: ValueError – If the text contains a newline.

pysabelle.raw.transport module

Async TCP transport for the Isabelle server protocol.

Async TCP transport implementing the Isabelle byte-message framing protocol (§4.2.1 - §4.2.2).

Transport wraps an asyncio StreamReader / StreamWriter pair and exposes two primitives:

send() — encode and write one command to the server.
receive() — read and decode one server reply.

Both short messages (single LF-terminated line) and long messages (decimal byte-count prefix followed by a body block) are handled transparently on receive, as required by §4.2.1.

Obtain an instance via the async factory Transport.open(), or supply an already-connected stream pair directly to the constructor.

class pysabelle.raw.transport.Transport(reader, writer)[source]

Bases: object

Async byte-level transport for the Isabelle server protocol (§4.2).

Do not instantiate directly — use Transport.open() or supply an existing (reader, writer) pair to the constructor.

Supports use as an async context manager:

async with await Transport.open(host, port) as t:
    await t.send(password, is_long_msg=False)
    reply = await t.receive()

Parameters:

reader (StreamReader) – An asyncio.StreamReader connected to the server.
writer (StreamWriter) – An asyncio.StreamWriter connected to the server.

async classmethod open(host='127.0.0.1', port=4711, timeout=30.0)[source]

Open a TCP connection to the Isabelle server.

Parameters:

host (str) – Server hostname or IP address (default "127.0.0.1").
port (int) – TCP port (default 4711).
timeout (float) – Connection-establishment timeout in seconds.

Return type:

Transport

Returns:

A connected Transport.

Raises:

IsabelleConnectionError – If the connection cannot be established within timeout seconds, or if the OS refuses it.

async send(command, *, is_long_msg=True)[source]

Write one command string to the server.

Parameters:

command (str) – Full command text, e.g. 'session_start {"session": "HOL"}'.
is_long_msg (bool) – When True (default) the message is framed as a long message (§4.2.1). Set False only for the initial password exchange (§4.2.4), which requires a plain LF-terminated line.

Raises:

IsabelleConnectionError – On write errors.

Return type:

None

async receive(timeout=None)[source]

Read and decode one server reply message.

Handles both §4.2.1 message framings transparently:

Short message — the first line is the complete reply.
Long message — the first line is a decimal byte-count; the body follows immediately.

Parameters:

timeout (float | None) – Optional per-call timeout in seconds. None waits indefinitely.

Return type:

RawReply

Returns:

Decoded RawReply.

Raises:

IsabelleConnectionError – If the server closes the connection.
IsabelleProtocolError – If the data violates §4.2 framing rules or contains an unknown reply name-tag.
asyncio.TimeoutError – If timeout is exceeded.

async close()[source]

Close the TCP connection gracefully.

Return type:: None

property is_closing: bool: True if the underlying transport is closing or already closed.

pysabelle.raw.types module

Typed dataclasses mirroring the JSON types defined in §4.3 of the Isabelle System Manual.

All types are pure data containers with from_dict / to_dict methods for JSON (de)serialisation.

pysabelle.raw.types.UUID: Isabelle UUID — a plain string on the wire.

class pysabelle.raw.types.TaskId(task)[source]

Bases: object

Wraps the UUID of a running asynchronous task (§4.3 type task).

Using a dedicated type prevents accidentally passing a task UUID where a session UUID is expected, and vice versa.

Variables:: task – Raw UUID string from an OK {"task": "<uuid>"} reply.
Parameters:: task (str)

task: str

class pysabelle.raw.types.SessionId(session_id)[source]

Bases: object

Wraps the UUID of an active PIDE session (§4.3 type session_id).

Variables:: session_id – Raw UUID string from a FINISHED {"session_id": "<uuid>", …} reply.
Parameters:: session_id (str)

session_id: str

pysabelle.raw.types.NoteCallback

Async callable invoked once for every NOTE message belonging to a task. Receives the raw RawReply so the caller can decode it into TheoryProgress, a generic Message, or any other appropriate type.

alias of Callable[[RawReply], Awaitable[None]]

class pysabelle.raw.types.Position(line=None, offset=None, end_offset=None, file=None, id=None)[source]

Bases: object

Source position within Isabelle text (§4.3 type position).

All fields are optional; only line and file are directly meaningful to external programs. Offset fields are counted in Isabelle symbol units, not bytes.

Variables:

line – 1‑based line number.
offset – Start offset in Isabelle symbol units.
end_offset – End offset in Isabelle symbol units.
file – Canonical file path.
id – PIDE command‑transaction identifier (rarely needed externally).

Parameters:

line (int | None)
offset (int | None)
end_offset (int | None)
file (str | None)
id (int | None)

line: int | None = None

offset: int | None = None

end_offset: int | None = None

file: str | None = None

id: int | None = None

classmethod from_dict(d)[source]

Deserialise from a JSON object.

Return type:: Position
Parameters:: d (dict[str, Any])

to_dict()[source]

Serialise to a JSON‑compatible dict; None fields are omitted.

Return type:: dict[str, Any]

class pysabelle.raw.types.MessageKind(value)[source]

Bases: str, Enum

Kind tag for Isabelle output messages (§4.3).

WRITELN = 'writeln'

WARNING = 'warning'

ERROR = 'error'

class pysabelle.raw.types.Message(kind, message, pos=None)[source]

Bases: object

General Isabelle output message (§4.3 type message).

Variables:

kind – Message category — "writeln", "warning", or "error".
message – Human‑readable text.
pos – Optional source position associated with the message.

Parameters:

kind (str)
message (str)
pos (Position | None)

kind: str

message: str

pos: Position | None = None

classmethod from_dict(d)[source]

Deserialise from a JSON object.

Return type:: Message
Parameters:: d (dict[str, Any])

property is_error: bool: True if kind == "error".

class pysabelle.raw.types.ErrorMessage(message)[source]

Bases: object

Error message whose kind is always "error" (§4.3 type error_message).

Variables:: message – Error description.
Parameters:: message (str)

message: str

kind: str = 'error'

classmethod from_dict(d)[source]

Deserialise from a JSON object.

The kind field in d is intentionally ignored — it is always "error" by definition.

Return type:: ErrorMessage
Parameters:: d (dict[str, Any])

class pysabelle.raw.types.TheoryProgress(message, theory, session, percentage=None)[source]

Bases: object

Theory‑loading progress notification (§4.3 type theory_progress).

Arrives as a NOTE message during session_build and session_start tasks. kind is always "writeln".

Variables:

message – Human‑readable progress description.
theory – Qualified theory name, e.g. "HOL.Nat".
session – Session name, e.g. "HOL".
percentage – Loading percentage in the range 0–100 (optional).

Parameters:

message (str)
theory (str)
session (str)
percentage (int | None)

message: str

theory: str

session: str

kind: str = 'writeln'

percentage: int | None = None

classmethod from_dict(d)[source]

Deserialise from a JSON object.

The kind field in d is intentionally ignored.

Return type:: TheoryProgress
Parameters:: d (dict[str, Any])

classmethod is_theory_progress(d)[source]

Return True if d contains the fields of a theory_progress payload.

Return type:: bool
Parameters:: d (dict[str, Any])

class pysabelle.raw.types.Timing(elapsed, cpu, gc)[source]

Bases: object

Wall‑clock timing reported by Isabelle in seconds (§4.3 type timing).

Variables:

elapsed – Total wall‑clock time.
cpu – CPU time consumed.
gc – Time spent in garbage collection.

Parameters:

elapsed (float)
cpu (float)
gc (float)

elapsed: float

cpu: float

gc: float

classmethod from_dict(d)[source]

Deserialise from a JSON object.

Return type:: Timing
Parameters:: d (dict[str, Any])

class pysabelle.raw.types.NodeStatus(ok, total, unprocessed, running, warned, failed, finished, canceled, consolidated, percentage)[source]

Bases: object

PIDE document‑model processing status for a theory node (§4.3 type node_status).

Variables:

ok – True iff failed == 0.
total – Total number of commands in the node.
unprocessed – Commands not yet started.
running – Commands currently executing.
warned – Commands that produced warnings.
failed – Commands that failed.
finished – Commands that completed successfully.
canceled – True if any command was spontaneously interrupted.
consolidated – True once the outermost theory structure has finished or failed and the final end command is checked.
percentage – Progress indicator in the range 0–100; reaches 100 when the node is consolidated.

Parameters:

ok (bool)
total (int)
unprocessed (int)
running (int)
warned (int)
failed (int)
finished (int)
canceled (bool)
consolidated (bool)
percentage (int)

ok: bool

total: int

unprocessed: int

running: int

warned: int

failed: int

finished: int

canceled: bool

consolidated: bool

percentage: int

classmethod from_dict(d)[source]

Deserialise from a JSON object.

Return type:: NodeStatus
Parameters:: d (dict[str, Any])

class pysabelle.raw.types.Node(node_name, theory_name)[source]

Bases: object

Internal theory node reference (§4.3 type node).

Variables:

node_name – Canonical file‑system path after normalisation, e.g. "~~/src/HOL/Examples/Seq.thy".
theory_name – Session‑qualified theory name, e.g. "HOL-Examples.Seq".

Parameters:

node_name (str)
theory_name (str)

node_name: str

theory_name: str

classmethod from_dict(d)[source]

Deserialise from a JSON object.

Return type:: Node
Parameters:: d (dict[str, Any])

class pysabelle.raw.types.NodeWithStatus(node, status)[source]

Bases: object

Theory node identity combined with its current processing status.

This is the element type of the nodes_status list emitted in NOTE messages when nodes_status_delay >= 0 is configured in UseTheoriesArgs. Corresponds to the spec type node ⊕ {status: node_status}.

Variables:

node – Theory node identity.
status – Current processing status.

Parameters:

node (Node)
status (NodeStatus)

node: Node

status: NodeStatus

classmethod from_dict(d)[source]

Deserialise from a flat merged JSON object (node ⊕ {status: …}).

Return type:: NodeWithStatus
Parameters:: d (dict[str, Any])

class pysabelle.raw.types.SessionBuildArgs(session, preferences=None, options=<factory>, dirs=<factory>, include_sessions=<factory>, verbose=False, print_mode=<factory>)[source]

Bases: object

Arguments shared by session_build (§4.4.5) and session_start (§4.4.6).

print_mode is accepted here for convenience; it is only meaningful for session_start and is silently ignored by session_build.

Variables:

session – Target session name, e.g. "HOL" or "HOL-Analysis".
preferences – Raw preferences text (the file content, not a path).
options – Individual option updates, e.g. ["timeout=60"].
dirs – Additional directories containing ROOT or ROOTS files.
include_sessions – Sessions whose theories should be included in the name space (for use with session‑qualified theory names).
verbose – Enable verbose build output.
print_mode – Print mode identifiers for session_start, e.g. ["ASCII"].

Parameters:

session (str)
preferences (str | None)
options (list[str])
dirs (list[str])
include_sessions (list[str])
verbose (bool)
print_mode (list[str])

session: str

preferences: str | None = None

options: list[str]

dirs: list[str]

include_sessions: list[str]

verbose: bool = False

print_mode: list[str]

to_dict()[source]

Serialise to a JSON‑compatible dict; empty and false fields are omitted.

Return type:: dict[str, Any]

class pysabelle.raw.types.SessionBuildResult(session, ok, return_code, timeout, timing)[source]

Bases: object

Build outcome for a single session within a session_build task (§4.4.5).

Variables:

session – Session name.
ok – True iff return_code == 0.
return_code – POSIX process exit code.
timeout – True if the build was aborted after exceeding the timeout.
timing – Wall‑clock timing for this session’s build.

Parameters:

session (str)
ok (bool)
return_code (int)
timeout (bool)
timing (Timing)

session: str

ok: bool

return_code: int

timeout: bool

timing: Timing

classmethod from_dict(d)[source]

Deserialise from a JSON object.

Return type:: SessionBuildResult
Parameters:: d (dict[str, Any])

class pysabelle.raw.types.SessionBuildResults(ok, return_code, sessions)[source]

Bases: object

Aggregate result of a completed session_build task (§4.4.5).

Variables:

ok – True iff all required sessions were built successfully.
return_code – Highest POSIX return code across all sessions.
sessions – Individual build results, one per session in the hierarchy.

Parameters:

ok (bool)
return_code (int)
sessions (list[SessionBuildResult])

ok: bool

return_code: int

sessions: list[SessionBuildResult]

classmethod from_dict(d)[source]

Deserialise from a JSON object.

Return type:: SessionBuildResults
Parameters:: d (dict[str, Any])

class pysabelle.raw.types.SessionStartResult(session_id, tmp_dir)[source]

Bases: object

Result of a successful session_start task (§4.4.6).

Variables:

session_id – Identifier of the newly created PIDE session.
tmp_dir – Path to a temporary directory created for this session; deleted when the session is stopped.

Parameters:

session_id (SessionId)
tmp_dir (str)

session_id: SessionId

tmp_dir: str

classmethod from_dict(d)[source]

Deserialise from a JSON object.

Return type:: SessionStartResult
Parameters:: d (dict[str, Any])

class pysabelle.raw.types.SessionStopResult(ok, return_code)[source]

Bases: object

Result of a session_stop task (§4.4.7).

Variables:

ok – True iff the underlying ML process terminated cleanly.
return_code – POSIX process exit code.

Parameters:

ok (bool)
return_code (int)

ok: bool

return_code: int

classmethod from_dict(d)[source]

Deserialise from a JSON object.

Return type:: SessionStopResult
Parameters:: d (dict[str, Any])

class pysabelle.raw.types.UseTheoriesArgs(session_id, theories, options=None, master_dir=None, pretty_margin=None, unicode_symbols=None, export_pattern=None, check_delay=None, check_limit=None, watchdog_timeout=None, nodes_status_delay=None)[source]

Bases: object

Arguments for the use_theories command (§4.4.8).

Variables:

session_id – Identifier of the target session.
theories – Theory names or absolute file paths to load.
options – Individual option updates for this invocation, e.g. ["show_states"] (Isabelle2026, §4.4.8; ignored by older servers).
master_dir – Base directory for resolving relative theory paths; defaults to the session tmp_dir.
pretty_margin – Line width used for pretty‑printing output messages; default is 76.
unicode_symbols – When True, render Isabelle symbols as Unicode in output rather than keeping their symbolic representation.
export_pattern – Pattern selecting theory exports (e.g. "*:*"); empty or None disables export retrieval.
check_delay – Seconds between consolidation status checks; default 0.5.
check_limit – Maximum number of checks; 0 means unbounded.
watchdog_timeout – Seconds of PIDE inactivity before aborting; default 600; 0 disables the watchdog.
nodes_status_delay – Seconds between NOTE nodes_status messages; negative disables them (default −1).

Parameters:

session_id (SessionId)
theories (list[str])
options (list[str] | None)
master_dir (str | None)
pretty_margin (float | None)
unicode_symbols (bool | None)
export_pattern (str | None)
check_delay (float | None)
check_limit (int | None)
watchdog_timeout (float | None)
nodes_status_delay (float | None)

session_id: SessionId

theories: list[str]

options: list[str] | None = None

master_dir: str | None = None

pretty_margin: float | None = None

unicode_symbols: bool | None = None

export_pattern: str | None = None

check_delay: float | None = None

check_limit: int | None = None

watchdog_timeout: float | None = None

nodes_status_delay: float | None = None

to_dict()[source]

Serialise to a JSON‑compatible dict; None fields are omitted.

Return type:: dict[str, Any]

class pysabelle.raw.types.Export(name, base64, body)[source]

Bases: object

Single theory export item returned by use_theories (§4.4.8).

Variables:

name – Compound export name in "theory/name" format.
base64 – True if body is base64‑encoded binary; False if it is plain UTF‑8 text.
body – Export content — either UTF‑8 text or a base64 string.

Parameters:

name (str)
base64 (bool)
body (str)

name: str

base64: bool

body: str

classmethod from_dict(d)[source]

Deserialise from a JSON object.

Return type:: Export
Parameters:: d (dict[str, Any])

class pysabelle.raw.types.NodeResults(status, messages, exports)[source]

Bases: object

Processing results for a single theory node (§4.4.8 type node_results).

Variables:

status – Final processing status of the node.
messages – All prover messages produced while checking this node.
exports – Theory exports matching the requested pattern.

Parameters:

status (NodeStatus)
messages (list[Message])
exports (list[Export])

status: NodeStatus

messages: list[Message]

exports: list[Export]

classmethod from_dict(d)[source]

Deserialise from a JSON object.

Return type:: NodeResults
Parameters:: d (dict[str, Any])

class pysabelle.raw.types.NodeResultEntry(node, results)[source]

Bases: object

One entry in use_theories_results.nodes (§4.4.8).

The spec type is node ⊕ node_results — a flat JSON merge of node identity and processing results. This class separates the two concerns into typed fields for clarity.

Variables:

node – Theory node identity.
results – Processing results for that node.

Parameters:

node (Node)
results (NodeResults)

node: Node

results: NodeResults

classmethod from_dict(d)[source]

Deserialise from a flat merged JSON object (node ⊕ node_results).

Return type:: NodeResultEntry
Parameters:: d (dict[str, Any])

class pysabelle.raw.types.UseTheoriesResults(ok, errors, nodes)[source]

Bases: object

Final result of a completed use_theories task (§4.4.8).

Variables:

ok – True iff all nodes were processed without errors.
errors – All error messages across every node (with position info).
nodes – Per‑node identity and detailed processing results.

Parameters:

ok (bool)
errors (list[Message])
nodes (list[NodeResultEntry])

ok: bool

errors: list[Message]

nodes: list[NodeResultEntry]

classmethod from_dict(d)[source]

Deserialise from a JSON object.

Return type:: UseTheoriesResults
Parameters:: d (dict[str, Any])

class pysabelle.raw.types.PurgeTheoriesArgs(session_id, theories=<factory>, master_dir=None, all=False)[source]

Bases: object

Arguments for the purge_theories command (§4.4.9).

Variables:

session_id – Identifier of the target session.
theories – Theory node names to remove — use node_name values from NodeResultEntry.node for precision.
master_dir – Base directory for relative paths; defaults to the session tmp_dir.
all – When True, attempt to purge all currently loaded theories.

Parameters:

session_id (SessionId)
theories (list[str])
master_dir (str | None)
all (bool)

session_id: SessionId

theories: list[str]

master_dir: str | None = None

all: bool = False

to_dict()[source]

Serialise to a JSON‑compatible dict; empty and false fields are omitted.

Return type:: dict[str, Any]

class pysabelle.raw.types.PurgeTheoriesResults(purged, retained)[source]

Bases: object

Result of a purge_theories command (§4.4.9).

The manual gives the type as {purged: [string]}, but the server (verified with Isabelle2025-2) returns lists of node objects for both fields; plain strings are still accepted for robustness.

Variables:

purged – Theory nodes that were actually removed from the session.
retained – Remaining loaded nodes (the complement of purged), e.g. those still imported by other theories or used by pending tasks.

Parameters:

purged (list[Node])
retained (list[Node])

purged: list[Node]

retained: list[Node]

classmethod from_dict(d)[source]

Deserialise from a JSON object.

Return type:: PurgeTheoriesResults
Parameters:: d (dict[str, Any])

Module contents

Raw protocol layer: transport, dispatcher, commands and types.

This package contains the low-level implementation of the Isabelle Server protocol. All public symbols are re-exported here for convenience.