IsabelleClientMini (isabelle_elixir v0.2.0)

Minimal stateless client for the Isabelle server.

The module intentionally exposes the TCP socket and keeps no process state. It does, however, implement Isabelle's real line-message framing: replies may be either a single line (OK ...) or a byte length line followed by exactly that many bytes.

Summary

Functions

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

Starts an asynchronous Isabelle command and returns an %IsabelleClient.Task{}.

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

Waits for an asynchronous Isabelle task to finish or fail.

build_session(socket, args)

Starts an Isabelle session_build task.

cancel_task(socket, task_id)

Requests cancellation of an Isabelle asynchronous task.

close(socket)

Closes a raw Isabelle TCP socket.

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

Runs a synchronous Isabelle server command and returns its OK body.

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

Connects to an Isabelle server and authenticates with its password.

echo(socket, value)

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

extract_results(arg1)

Extracts user-facing theory messages from a finished use_theories result.

extract_session(arg1)

Extracts the session_id from a finished session-start result.

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, kept for the original Mini workflow.

purge_theories(socket, args)

Runs Isabelle purge_theories for an active session.

recv(socket, timeout \\ 30000)

Receives one framed Isabelle server response.

shutdown_server(socket)

Asks the Isabelle server process to shut down.

start_session(socket, args)

Starts an Isabelle session_start task.

stop_session(socket, session_id)

Starts an Isabelle session_stop task for a session id.

use_theories(socket, args)

Starts an Isabelle use_theories task.