IsabelleClient.Raw

Intro

This notebook uses IsabelleClient.Raw. It exposes the TCP socket, keeps no session state, and leaves async task waiting explicit. It also exposes some basic server management functionality.

Read IsabelleClient.livemd first if you are new to the library. The raw API is useful when you want to see or control the Isabelle server protocol directly: you send a command, receive a task id, then wait for the task yourself.

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

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

IsabelleClient.Server.executable()

Server Management

Resident Isabelle servers are named. list_servers/0 shows local resident servers known to Isabelle, and kill_server/1 can force-kill one by name. This is mainly useful after interrupted runs.

{:ok, servers_before_demo} = IsabelleClient.Raw.list_servers()
servers_before_demo

We start two short-lived servers. Passing port 0 asks Isabelle to choose a free local port.

kill_demo_names =
  for n <- 1..2 do
    name = "livebook_raw_kill_demo_#{n}_#{System.unique_integer([:positive])}"
    {:ok, _server} = IsabelleClient.Raw.new_server(name, 0)
    name
  end

{:ok, servers_after_start} = IsabelleClient.Raw.list_servers()

Enum.filter(servers_after_start, &(&1.name in kill_demo_names))

kill_results = Enum.map(kill_demo_names, &IsabelleClient.Raw.kill_server/1)

{:ok, servers_after_kill} = IsabelleClient.Raw.list_servers()

%{
  kill_statuses: Enum.map(kill_results, fn {_output, status} -> status end),
  remaining_demo_servers: Enum.filter(servers_after_kill, &(&1.name in kill_demo_names))
}

Let’s leave one server running for the rest of the tutorial:

server_name = "livebook_raw_#{System.unique_integer([:positive])}"
{:ok, server} = IsabelleClient.Raw.new_server(server_name, 0)

Session-less Commands

Let’s connect to a running server (running locally or elsewhere):

{:ok, socket} = IsabelleClient.Raw.connect(server["password"], server["host"], server["port"])

Using the socket connection we can invoke some synchronous (“sessionless”) commands.

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

payload = %{client: "raw", framed: String.duplicate("x", 120)}
{:ok, %{"client" => "raw", "framed" => framed}} = IsabelleClient.Raw.echo(socket, payload)

{:ok, %{"via" => "command/4"}} = IsabelleClient.Raw.command(socket, "echo", %{via: "command/4"})

command/4 is the escape hatch for server commands without a dedicated helper. It sends one request and waits for one OK or ERROR response. cancel_task/2 sends the protocol-level cancellation command; cancelling an unknown task is harmless on the Isabelle side.

{:ok, nil} = IsabelleClient.Raw.cancel_task(socket, "00000000-0000-0000-0000-000000000000")

Session Tasks

Asynchronous commands first return OK {"task": ...}. Raw helpers return that task id as an %IsabelleClient.Task{status: :running}. Call await_task/3 to collect NOTE messages and the final FINISHED or FAILED payload.

{:ok, build_task} =
  IsabelleClient.Raw.async_command(socket, "session_build", session: "HOL", verbose: true)

{:ok, build_task} = IsabelleClient.Raw.await_task(socket, build_task, 120_000)

%{
  status: build_task.status,
  ok?: build_task.result["ok"],
  messages: IsabelleClient.messages(build_task)
}

Dedicated helpers such as start_session/3 and use_theories/3 are thin wrappers around async_command/4. start_session/3 accepts Isabelle session_start arguments such as session, preferences, options, dirs, include_sessions, verbose, and print_mode.

{:ok, start_task} =
  IsabelleClient.Raw.start_session(socket,
    session: "HOL",
    verbose: true,
    print_mode: ["ASCII"]
  )

{:ok, start_task} = IsabelleClient.Raw.poll_status(socket, start_task, 120_000)

session_id = IsabelleClient.extract_session(start_task)

%{
  status: start_task.status,
  session_id: session_id,
  messages: IsabelleClient.messages(start_task)
}

Check A Theory

The raw socket does not remember an active session. Every session command that needs a live session must receive session_id explicitly.

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

File.mkdir_p!(theory_dir)

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

lemma "x = x"
  sledgehammer
  by simp

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

end
""")

{:ok, use_task} =
  IsabelleClient.Raw.use_theories(socket,
    session_id: session_id,
    theories: ["RawExample"],
    master_dir: theory_dir,
    pretty_margin: 80.0,
    unicode_symbols: true,
    export_pattern: "*",
    check_delay: 0.1,
    check_limit: 100,
    watchdog_timeout: 60.0,
    nodes_status_delay: 0.5
  )

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

The result helpers work with raw-socket task results too. Result.decode/1 turns common Isabelle result maps into small Elixir structs when that is useful.

typed = IsabelleClient.Result.decode(use_task)

%{
  typed_ok?: typed.ok,
  node_names: Enum.map(IsabelleClient.nodes(use_task), & &1.node_name),
  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))
}

Build And Start A Custom Session

The raw profile is also the clearest place to see Isabelle’s session_build and session_start arguments. session_start accepts the session_build arguments plus print_mode.

We first write a minimal Isabelle session: one ROOT file and one theory.

custom_suffix = System.unique_integer([:positive])
custom_session = "RawBuild#{custom_suffix}"
custom_dir = Path.join(System.tmp_dir!(), "isabelle_elixir_livebook_raw_build_#{custom_suffix}")
File.mkdir_p!(custom_dir)

File.write!(Path.join(custom_dir, "ROOT"), """
session "#{custom_session}" = "HOL" +
  options [document = false, show_question_marks = false]
  theories
    RawBuildTheory
""")

File.write!(Path.join(custom_dir, "RawBuildTheory.thy"), """
theory RawBuildTheory imports Main
begin

lemma raw_build_example: "x = x"
  by simp

end
""")

Build the reusable session image first.

{:ok, custom_build_task} =
  IsabelleClient.Raw.build_session(socket,
    session: custom_session,
    dirs: [custom_dir],
    options: ["document=false", "show_question_marks=false"],
    include_sessions: [],
    preferences: "",
    verbose: true
  )

{:ok, custom_build_task} =
  IsabelleClient.Raw.await_task(socket, custom_build_task, 120_000)

%{
  result: IsabelleClient.session_build_result(custom_build_task),
  messages: IsabelleClient.messages(custom_build_task)
}

Start a live session from the built image. Keep dirs, so Isabelle can resolve the custom session name.

{:ok, custom_start_task} =
  IsabelleClient.Raw.start_session(socket,
    session: custom_session,
    dirs: [custom_dir],
    options: ["document=false"],
    include_sessions: [],
    preferences: "",
    verbose: true,
    print_mode: ["ASCII"]
  )

{:ok, custom_start_task} =
  IsabelleClient.Raw.await_task(socket, custom_start_task, 120_000)

custom_session_id = IsabelleClient.extract_session(custom_start_task)

%{
  session_id: custom_session_id,
  messages: IsabelleClient.messages(custom_start_task)
}

Use the returned session id explicitly. Raw commands do not remember an active session for you.

File.write!(Path.join(custom_dir, "RawBuildUse.thy"), """
theory RawBuildUse imports RawBuildTheory
begin

lemma raw_build_use: "x = x"
  by (rule raw_build_example)

end
""")

{:ok, custom_use_task} =
  IsabelleClient.Raw.use_theories(socket,
    session_id: custom_session_id,
    theories: ["RawBuildUse"],
    master_dir: custom_dir
  )

{:ok, custom_use_task} =
  IsabelleClient.Raw.await_task(socket, custom_use_task, 120_000)

%{
  ok?: custom_use_task.result["ok"],
  messages: IsabelleClient.messages(custom_use_task)
}

Stop And Shutdown

# Stop the custom session before the original one.
{:ok, custom_stop_task} = IsabelleClient.Raw.stop_session(socket, custom_session_id)
{:ok, custom_stop_task} = IsabelleClient.Raw.await_task(socket, custom_stop_task, 120_000)

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

{stop_task.status, custom_stop_task.status}

{:ok, nil} = IsabelleClient.Raw.shutdown_server(socket)
:ok = IsabelleClient.Raw.close(socket)
:ok