IsabelleClientMini

IsabelleClientMini is the low-level client. It exposes the TCP socket, keeps no session state, and leaves async task waiting explicit. Use it when you want to drive the Isabelle server protocol directly.

This notebook starts a local server, connects to it, runs a few commands, starts HOL, checks a small theory, extracts messages, and cleans up.

Setup

When using the published package, replace the dependency with {:isabelle_elixir, "~> 0.2"}.

Mix.install([
  {:isabelle_elixir, path: Path.expand("..", __DIR__)}
])

IsabelleClient.Server.executable()

Start And Connect

Passing port 0 asks Isabelle to choose a free local port.

server_name = "livebook_mini_#{System.unique_integer([:positive])}"
{:ok, [server]} = IsabelleClientMini.new_server(server_name, 0)
{:ok, socket} = IsabelleClientMini.connect(server["password"], server["host"], server["port"])

{:ok, servers} = IsabelleClientMini.list_servers()
Enum.any?(servers, &(&1["name"] == server_name))

Synchronous Commands

{:ok, commands} = IsabelleClientMini.help(socket)

for command <- ~w(cancel echo help purge_theories session_build session_start session_stop shutdown use_theories) do
  true = command in commands
end

payload = %{client: "mini", framed: String.duplicate("x", 120)}
{:ok, %{"client" => "mini", "framed" => framed}} = IsabelleClientMini.echo(socket, payload)
String.length(framed)

command/4 is the escape hatch for server commands without a dedicated helper.

{:ok, %{"raw" => true}} = IsabelleClientMini.command(socket, "echo", raw: true)

Session Tasks

Asynchronous commands first return OK {"task": ...}. Mini returns that task id as an %IsabelleClient.Task{} and leaves await_task/3 explicit.

{:ok, build_task} = IsabelleClientMini.build_session(socket, session: "HOL")
{:ok, build_task} = IsabelleClientMini.await_task(socket, build_task, 120_000)

{build_task.status, build_task.result["ok"], length(build_task.notes)}

{:ok, start_task} = IsabelleClientMini.start_session(socket, session: "HOL")
{:ok, start_task} = IsabelleClientMini.await_task(socket, start_task, 120_000)

session_id = IsabelleClientMini.extract_session(start_task)
{start_task.status, is_binary(session_id)}

Check A Theory

Mini does not remember the active session, so session_id is passed explicitly.

theory_dir =
  Path.join(System.tmp_dir!(), "isabelle_elixir_livebook_mini_#{System.unique_integer([:positive])}")

File.mkdir_p!(theory_dir)

File.write!(Path.join(theory_dir, "MiniExample.thy"), """
theory MiniExample imports Main
begin

lemma "x = x"
  sledgehammer
  by simp

lemma "xs @ [] = xs"
  sledgehammer
  by simp

end
""")

{:ok, use_task} =
  IsabelleClientMini.use_theories(socket,
    session_id: session_id,
    theories: ["MiniExample"],
    master_dir: theory_dir
  )

{:ok, use_task} = IsabelleClientMini.await_task(socket, use_task, 120_000)
true = use_task.result["ok"]

The result helpers live on IsabelleClient and work with Mini task results too.

%{
  messages: IsabelleClient.messages(use_task),
  sledgehammer_lines: IsabelleClient.messages(use_task, line: [5, 9]),
  proof_lines: IsabelleClient.messages(use_task, line: [6, 10]),
  first_proof_at_offset:
    use_task
    |> IsabelleClient.diagnostics(line: 6)
    |> List.first()
    |> get_in(["pos", "offset"])
    |> then(&IsabelleClient.messages(use_task, line: 6, offset: &1))
}

{:ok, purge_result} =
  IsabelleClientMini.purge_theories(socket,
    session_id: session_id,
    theories: ["MiniExample"],
    master_dir: theory_dir
  )

{purge_result["purged"], purge_result["retained"]}

Stop And Shutdown

{:ok, stop_task} = IsabelleClientMini.stop_session(socket, session_id)
{:ok, stop_task} = IsabelleClientMini.await_task(socket, stop_task, 120_000)
stop_task.status

{:ok, nil} = IsabelleClientMini.shutdown_server(socket)
:ok = IsabelleClientMini.close(socket)
IsabelleClientMini.kill_server(server_name)