pysabelle.session package

Submodules

pysabelle.session.callbacks module

Callback helpers for converting raw NOTE replies into typed callbacks.

pysabelle.session.callbacks.ProgressCallback

Callback for progress updates during session build/start. Receives either a TheoryProgress or a generic Message.

alias of Callable[[TheoryProgress | Message], Awaitable[None]]

pysabelle.session.callbacks.NodesStatusCallback

Callback for periodic node status updates during use_theories. Receives a list of NodeWithStatus.

alias of Callable[[list[NodeWithStatus]], Awaitable[None]]

pysabelle.session.callbacks.build_note_handler(on_progress)

Convert a ProgressCallback into a NoteCallback for session build/start.

Parameters:

on_progress (Callable[[TheoryProgress | Message], Awaitable[None]]) – User‑provided callback that expects either a TheoryProgress or a Message.

Return type:

Callable[[RawReply], Awaitable[None]]

Returns:

A NoteCallback suitable for passing to session_build or session_start.

pysabelle.session.callbacks.use_theories_note_handler(on_progress, on_nodes_status)

Combine optional progress and nodes_status callbacks into a single NoteCallback.

Parameters:

• on_progress (Callable[[TheoryProgress | Message], Awaitable[None]] | None) – Optional progress callback.

• on_nodes_status (Callable[[list[NodeWithStatus]], Awaitable[None]] | None) – Optional nodes‑status callback.

Return type:

Callable[[RawReply], Awaitable[None]] | None

Returns:

A NoteCallback that dispatches NOTE messages to the appropriate user callback, or None if both callbacks are None.

pysabelle.session.exceptions module

Exceptions specific to the high‑level session API.

exception pysabelle.session.exceptions.IsabelleSessionError

Bases: IsabelleError

Base class for errors raised by IsabelleSession.

exception pysabelle.session.exceptions.SessionAlreadyClosed

Bases: IsabelleSessionError

Raised when a method is called on an already‑closed session.

Return type:

None

exception pysabelle.session.exceptions.TheoryLoadError(errors)

Bases: IsabelleSessionError

Raised by use_theories() when ok=False and raise_on_error=True.

Variables:

errors – List of error messages collected during theory loading.

Parameters:

errors (list[Message])

Return type:

None

pysabelle.session.session module

High‑level Isabelle session facade with convenience methods.

class pysabelle.session.session.IsabelleSession(client, session_id, tmp_dir)

Bases: object

High‑level session wrapper.

This class provides a convenient interface to an Isabelle PIDE session. It manages the underlying client, dispatcher and server process, and offers methods for building, loading theories, purging, etc.

Use the class methods start() (spawn a new server) or connect() (attach to an existing server) to create an instance. It is designed to be used as an async context manager.

Variables:

• session_id – The UUID of the session.

• tmp_dir – Temporary directory created for this session.

Parameters:

• client (IsabelleClient)

• session_id (SessionId)

• tmp_dir (str)

property session_id: SessionId

Session UUID.

property tmp_dir: str

Temporary directory path.

async classmethod start(session, *, server_name='isabelle', reuse_server=True, server_env=None, options=(), dirs=(), include_sessions=(), verbose=False, print_mode=(), on_progress=None, timeout=None)

Start a new Isabelle server and create a session.

Parameters:

• session (str) – Name of the session to start (e.g., “HOL”).

• server_name (str) – Name for the server process.

• reuse_server (bool) – If True, attach to an existing server with the same name instead of starting a new one.

• server_env (dict[str, str] | None) – Environment for the isabelle server subprocesses (default: inherit os.environ).

• options (Sequence[str]) – List of Isabelle options (e.g., [“timeout=60”]).

• dirs (Sequence[str]) – Additional directories containing ROOT files.

• include_sessions (Sequence[str]) – Sessions whose theories should be included.

• verbose (bool) – Enable verbose output.

• print_mode (Sequence[str]) – Print mode for output (e.g., [“ASCII”]).

• on_progress (Callable[[TheoryProgress | Message], Awaitable[None]] | None) – Optional callback for progress messages during startup.

• timeout (float | None) – Optional timeout for the session_start command.

Return type:

IsabelleSession

Returns:

A new IsabelleSession instance.

Raises:

• IsabelleConnectionError – If server connection fails.

• IsabelleCommandError – If the session_start command fails.

async classmethod connect(session, *, host='127.0.0.1', port=4711, password='', options=(), dirs=(), include_sessions=(), verbose=False, print_mode=(), on_progress=None, timeout=None)

Connect to an already‑running Isabelle server and create a session.

Parameters:

• session (str) – Name of the session to start.

• host (str) – Server hostname.

• port (int) – Server port.

• password (str) – Password for handshake.

• options (Sequence[str]) – List of Isabelle options.

• dirs (Sequence[str]) – Additional directories.

• include_sessions (Sequence[str]) – Sessions to include.

• verbose (bool) – Enable verbose output.

• print_mode (Sequence[str]) – Print mode.

• on_progress (Callable[[TheoryProgress | Message], Awaitable[None]] | None) – Optional progress callback.

• timeout (float | None) – Optional timeout for session_start.

Return type:

IsabelleSession

Returns:

A new IsabelleSession instance.

Raises:

• IsabelleConnectionError – If connection/handshake fails.

• IsabelleCommandError – If session_start fails.

async build(session, *, options=(), dirs=(), include_sessions=(), verbose=False, on_progress=None, timeout=None)

Build a session hierarchy (without starting it).

Parameters:

• session (str) – Session name to build.

• options (Sequence[str]) – List of Isabelle options.

• dirs (Sequence[str]) – Additional directories.

• include_sessions (Sequence[str]) – Sessions to include.

• verbose (bool) – Enable verbose output.

• on_progress (Callable[[TheoryProgress | Message], Awaitable[None]] | None) – Optional progress callback.

• timeout (float | None) – Optional timeout.

Return type:

SessionBuildResults

Returns:

Build results for all required sessions.

Raises:

• SessionAlreadyClosed – If the session is already closed.

• IsabelleCommandError – If the build fails.

async use_theories(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, on_progress=None, on_nodes_status=None, raise_on_error=False, timeout=None)

Load and process a list of theories.

Parameters:

• theories (list[str]) – List of theory names or file paths.

• options (Sequence[str] | None) – Option updates for this invocation (Isabelle2026+).

• master_dir (str | None) – Base directory for resolving relative paths.

• pretty_margin (float | None) – Output line width.

• unicode_symbols (bool | None) – Use Unicode symbols in output.

• export_pattern (str | None) – Pattern for theory exports.

• check_delay (float | None) – Seconds between status checks.

• check_limit (int | None) – Maximum number of checks (0 = unbounded).

• watchdog_timeout (float | None) – Seconds of inactivity before abort.

• nodes_status_delay (float | None) – Seconds between node status updates.

• on_progress (Callable[[TheoryProgress | Message], Awaitable[None]] | None) – Callback for progress messages.

• on_nodes_status (Callable[[list[NodeWithStatus]], Awaitable[None]] | None) – Callback for periodic node status lists.

• raise_on_error (bool) – If True, raise TheoryLoadError when ok is False.

• timeout (float | None) – Optional timeout in seconds for the whole command; on expiry the task is cancelled on the server and IsabelleTimeoutError is raised.

Return type:

UseTheoriesResults

Returns:

UseTheoriesResults containing per‑node status, messages and exports.

Raises:

• SessionAlreadyClosed – If session is closed.

• TheoryLoadError – If raise_on_error=True and errors occurred.

• IsabelleCommandError – For other command failures.

async purge_theories(theories=(), *, master_dir=None, all=False)

Unload theories from the session.

Theories are resolved like imports (relative to master_dir). node_name values from UseTheoriesResults.nodes may be passed as well (§4.4.9): their .thy suffix is removed automatically. Imported dependencies are not added: pass the whole nodes list returned by use_theories to release them too.

Warning

With Isabelle2025-2 a purged theory cannot be loaded again in the same session (use_theories then reports “Illegal theory header”); this also happens with all=True. Purge only theories you will not need again, or start a new session.

Parameters:

• theories (Sequence[str]) – Theory names or node names to purge.

• master_dir (str | None) – Base directory for resolving relative names.

• all (bool) – If True, purge all currently loaded theories.

Return type:

PurgeTheoriesResults

Returns:

PurgeTheoriesResults listing purged and retained nodes.

Raises:

• SessionAlreadyClosed – If session is closed.

• IsabelleCommandError – If the command fails.

async check_theories(theories, **kwargs)

Load theories and return only the error messages.

This is a convenience wrapper around use_theories that discards success information and returns only the error list.

Parameters:

• theories (list[str]) – List of theory names.

• **kwargs (Any) – Additional arguments passed to use_theories.

Return type:

list[Message]

Returns:

List of error messages (empty if no errors).

async load_and_purge(theories, **kwargs)

Load theories and then immediately purge them, with all their imports.

Useful for checking theories with minimal memory footprint. Every node reported by use_theories (the requested theories and their imports outside the session image) is purged. If use_theories raises (e.g. raise_on_error=True), the requested theories are purged anyway and the original exception is re-raised.

Warning

See purge_theories(): with Isabelle2025-2 the purged theories (including their imports) cannot be reloaded in the same session.

Parameters:

• theories (list[str]) – List of theory names.

• **kwargs (Any) – Additional arguments passed to use_theories; master_dir is also used for purging.

Return type:

UseTheoriesResults

Returns:

The results of the use_theories command (before purging).

async close(*, timeout=60.0)

Stop the session and clean up resources.

The connection, the dispatcher and (if owned) the server process are always released, even when session_stop fails or times out.

Parameters:

timeout (float | None) – Maximum seconds to wait for session_stop.

Return type:

SessionStopResult

Returns:

SessionStopResult indicating success and return code.

Raises:

IsabelleCommandError – If session_stop fails (resources are released anyway).

Module contents

High‑level session API: IsabelleSession and associated callback types.