IsabelleClient.Raw (isabelle_elixir v0.3.0)

View Source

Raw-socket Isabelle client.

This profile exposes the TCP socket and leaves session ids and asynchronous task waiting explicit. It is useful for protocol-level control and for understanding Isabelle server messages directly.

Summary

Functions

Sends an async command and returns a running %IsabelleClient.Task{}.

Waits for an asynchronous task to finish or fail.

Starts a session_build task and returns its task handle.

Requests cancellation of an Isabelle asynchronous task by task id.

Closes a raw TCP socket.

Runs a synchronous Isabelle command and returns {:ok, body} or {:error, body}.

Connects to an Isabelle server and returns a raw TCP socket.

Round-trips a JSON value through Isabelle's echo command.

Returns the server command names supported by Isabelle.

Force-kills a local resident Isabelle server by name.

Lists local resident Isabelle servers known to Isabelle.

Starts a local resident Isabelle server via isabelle server.

Runs Isabelle's synchronous purge_theories command.

Receives one framed Isabelle server response from a raw socket.

Asks the Isabelle server process to shut down.

Starts a session_start task and returns its task handle.

Starts a session_stop task for a session struct or session id.

Starts a use_theories task and returns its task handle.

Functions

async_command(socket, name, arg, timeout \\ 30000)

Sends an async command and returns a running %IsabelleClient.Task{}.

Use await_task/3 to collect later NOTE messages and the final FINISHED or FAILED response.

Pending NOTE frames from earlier tasks are skipped while waiting for the command acknowledgement.

await_task(socket, task_or_id, timeout \\ :infinity)

Waits for an asynchronous task to finish or fail.

Returns {:ok, task} for FINISHED and {:error, task} for FAILED. Task notes received while waiting are stored in task.notes.

build_session(socket, args, timeout \\ 30000)

Starts a session_build task and returns its task handle.

cancel_task(socket, task_id)

Requests cancellation of an Isabelle asynchronous task by task id.

close(socket)

Closes a raw TCP socket.

command(socket, name, arg \\ nil, timeout \\ 30000)

Runs a synchronous Isabelle command and returns {:ok, body} or {:error, body}.

connect(password, host \\ "127.0.0.1", port \\ 9999, timeout \\ 30000)

Connects to an Isabelle server and returns a raw TCP socket.

Use the server password plus host/port from new_server/2, list_servers/0, or another Isabelle server process reachable on the network.

echo(socket, value)

Round-trips a JSON value through Isabelle's echo command.

help(socket)

Returns the server command names supported by Isabelle.

kill_server(name)

Force-kills a local resident Isabelle server by name.

list_servers()

Lists local resident Isabelle servers known to Isabelle.

new_server(name \\ "elixir", port \\ 9999)

Starts a local resident Isabelle server via isabelle server.

poll_status(socket, task_or_id, timeout \\ :infinity)

Alias for await_task/3.

purge_theories(socket, args, timeout \\ 30000)

Runs Isabelle's synchronous purge_theories command.

recv(socket, timeout \\ 30000)

Receives one framed Isabelle server response from a raw socket.

shutdown_server(socket)

Asks the Isabelle server process to shut down.

start_session(socket, args, timeout \\ 30000)

Starts a session_start task and returns its task handle.

Arguments are forwarded to Isabelle. session_start accepts session_build arguments (:session, :preferences, :options, :dirs, :include_sessions, :verbose) plus :print_mode.

stop_session(socket, session_or_id, timeout \\ 30000)

Starts a session_stop task for a session struct or session id.

use_theories(socket, args, timeout \\ 30000)

Starts a use_theories task and returns its task handle.

Arguments are forwarded to Isabelle and may include :session_id, :theories, :master_dir, :pretty_margin, :unicode_symbols, :export_pattern, :check_delay, :check_limit, :watchdog_timeout, and :nodes_status_delay.