IsabelleClientFull (isabelle_elixir v0.2.0)

View Source

GenServer-backed Isabelle client.

The process owns the TCP socket, so callers may safely use the same client from multiple processes. Operations are serialized deliberately: Isabelle's server can run asynchronous tasks, but a single TCP stream is still easiest to reason about when one process owns reads and writes.

Summary

Functions

Builds an Isabelle session image and waits for the task result.

Returns a specification to start this module under a supervisor.

Stops the client process and closes its socket.

Runs a synchronous Isabelle command through the client process.

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

Returns the server command names supported by Isabelle.

Purges theories from the active session.

Asks the Isabelle server process to shut down.

Starts a GenServer-backed Isabelle client.

Starts an Isabelle session and stores its session_id in the client process.

Stops the active Isabelle session.

Checks theories in the active session and waits for the task result.

Functions

build_session(server, args, timeout \\ :infinity)

Builds an Isabelle session image and waits for the task result.

child_spec(init_arg)

Returns a specification to start this module under a supervisor.

See Supervisor.

close(server)

Stops the client process and closes its socket.

command(server, name, arg \\ nil, timeout \\ :infinity)

Runs a synchronous Isabelle command through the client process.

connect(opts)

Alias for start_link/1.

echo(server, value)

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

help(server)

Returns the server command names supported by Isabelle.

purge_theories(server, args, timeout \\ :infinity)

Purges theories from the active session.

shutdown_server(server)

Asks the Isabelle server process to shut down.

start_link(opts)

Starts a GenServer-backed Isabelle client.

start_session(server, args, timeout \\ :infinity)

Starts an Isabelle session and stores its session_id in the client process.

stop_session(server, timeout \\ :infinity)

Stops the active Isabelle session.

use_theories(server, args, timeout \\ :infinity)

Checks theories in the active session and waits for the task result.