IsabelleClient.Shared

Intro

IsabelleClient.Shared is the process-owning client. It wraps the stateful client in a GenServer, so many Elixir processes can share one Isabelle connection without racing on socket reads.

Read IsabelleClient.livemd first if you are new to the library. This notebook focuses on the extra coordination needed once multiple Elixir processes use one Isabelle connection.

The Shared client does two different kinds of coordination:

• synchronous command replies are read by one owner process and returned to the caller in command-stream order
• asynchronous Isabelle task messages are routed by task id, so concurrent callers waiting for different tasks get their own NOTE and FINISHED messages
• async calls can receive lightweight %{type:, task:, body:} events via on_event

It does not make Isabelle check dependent theories independently, and it does not promise FIFO completion for async tasks. Completion order belongs to Isabelle. Keep on_event callbacks lightweight; sending a message to another process is a good pattern.

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

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

IsabelleClient.Server.executable()

Start A Shared Client

Without a :password, start_link/1 starts a local Isabelle server. The returned pid is the shared client handle. We start sessions explicitly below so the lifecycle is visible.

{:ok, pid} =
  IsabelleClient.Shared.start_link(
    server_name: "livebook_shared_#{System.unique_integer([:positive])}",
    timeout: 120_000
  )

Process.alive?(pid)

For an already running server, including one reachable on another host, pass its connection details instead of :server_name:

# {:ok, pid} =
#   IsabelleClient.Shared.start_link(
#     password: "server-password",
#     host: "isabelle.example.org",
#     port: 9999,
#     timeout: 120_000
#   )

Concurrent Synchronous Commands

These calls are safe to run from many processes. They still pass through one socket owner, so this is caller-safety, not parallel TCP streams.

operations =
  (Enum.map(1..8, &{:echo, &1}) ++ Enum.map(1..2, &{:help, &1}))
  |> Enum.shuffle()

sync_tasks =
  for operation <- operations do
    Task.async(fn ->
      case operation do
        {:echo, n} ->
          payload = %{client: "shared", n: n, framed: String.duplicate("#{n}", 120)}
          {:ok, echoed} = IsabelleClient.Shared.echo(pid, payload)
          {:echo, echoed["n"]}

        {:help, n} ->
          {:ok, commands} = IsabelleClient.Shared.help(pid)
          true = "use_theories" in commands
          {:help, n}
      end
    end)
  end

sync_results = Task.await_many(sync_tasks, 30_000)
Enum.sort(sync_results) == Enum.sort(operations)

More Than One Session

The shared process keeps the same kind of LIFO session stack as the default client: the most recently started session is active. Isabelle sessions are still server resources, and you can route work to a specific one with session_id:. start_session/3 accepts Isabelle session_start arguments such as session, preferences, options, dirs, include_sessions, verbose, and print_mode. It also accepts a library-only label: that is stored locally and not sent to Isabelle.

{:ok, first_start_task} =
  IsabelleClient.Shared.start_session(
    pid,
    [session: "HOL", label: "shared-main", print_mode: ["ASCII"]],
    120_000
  )

{:ok, second_start_task} = IsabelleClient.Shared.start_session(pid, [session: "HOL"], 120_000)

first_session = IsabelleClient.Session.from_result(first_start_task.result)
second_session = IsabelleClient.Session.from_result(second_start_task.result)

%{
  first_session: first_session.id,
  second_session: second_session.id,
  different?: first_session.id != second_session.id,
  first_start_messages: IsabelleClient.messages(first_start_task),
  second_start_messages: IsabelleClient.messages(second_start_task)
}

Concurrent Theory Tasks

Here the interesting part is task routing. Each caller starts its own use_theories task and installs an on_event callback tagged with the theory it requested. Isabelle may finish tasks in any order, but every event receives the task id that belongs to that caller’s task.

When a client has more than one server session, pass session_id: in the use_theories arguments to target a specific session. The task routing is still based on Isabelle task ids.

parent = self()
event_ref = make_ref()
done_ref = make_ref()

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

File.mkdir_p!(theory_dir)

theories = [
  {"SharedExample1", "lemma \"x = x\"\n  by simp", "theorem ?x = ?x"},
  {"SharedExample2", "lemma \"xs @ [] = xs\"\n  by simp", "theorem ?xs @ [] = ?xs"},
  {"SharedExample3", "lemma \"(A \\ A) \\ True\"\n  by simp",
   "theorem (?A \\ ?A) \\ True"}
]

session_ids = [first_session.id, second_session.id, second_session.id]

for {theory, body, _expected} <- theories do
  File.write!(Path.join(theory_dir, "#{theory}.thy"), """
  theory #{theory} imports Main
  begin

  #{body}

  end
  """)
end

theory_tasks =
  theories
  |> Enum.zip(session_ids)
  |> Enum.shuffle()
  |> Enum.map(fn {{theory, _body, expected_message}, session_id} ->
    Task.async(fn ->
      on_event = fn event ->
        send(parent, {:shared_event, event_ref, theory, event.type, event.task, event.body})
      end

      {:ok, task} =
        IsabelleClient.Shared.use_theories(
          pid,
          [session_id: session_id, theories: [theory], master_dir: theory_dir],
          120_000,
          on_event: on_event
        )

      messages = IsabelleClient.messages(task)
      true = task.result["ok"]
      true = Enum.any?(messages, &String.contains?(&1, expected_message))

      result = %{theory: theory, task_id: task.id, messages: messages}
      send(parent, {:shared_done, done_ref, result})
      result
    end)
  end)

completion_order =
  for _ <- theory_tasks do
    receive do
      {:shared_done, ^done_ref, result} -> result.theory
    after
      120_000 -> raise "timed out waiting for theory result"
    end
  end

theory_results = Task.await_many(theory_tasks, 1_000)

events =
  Stream.repeatedly(fn ->
    receive do
      {:shared_event, ^event_ref, theory, type, task_id, body} -> {theory, type, task_id, body}
    after
      100 -> :done
    end
  end)
  |> Enum.take_while(&amp;(&amp;1 != :done))

results_by_theory = Map.new(theory_results, &amp;{&amp;1.theory, &amp;1})

notes = Enum.filter(events, fn {_theory, type, _task_id, _body} -> type == :note end)
notes_by_theory = Enum.group_by(notes, fn {theory, _type, _task_id, _body} -> theory end)

true = Map.keys(results_by_theory) |> Enum.sort() == ~w(SharedExample1 SharedExample2 SharedExample3)
true = Map.keys(notes_by_theory) |> Enum.sort() == ~w(SharedExample1 SharedExample2 SharedExample3)

true =
  Enum.all?(notes, fn {theory, _type, task_id, _body} ->
    task_id == results_by_theory[theory].task_id
  end)

%{
  completion_order: completion_order,
  checked_theories: Map.keys(results_by_theory) |> Enum.sort(),
  event_types: events |> Enum.map(fn {_theory, type, _task_id, _body} -> type end) |> Enum.uniq(),
  note_count: length(notes)
}

Check Text Helper

check_text/5 is available on Shared too. Use it when you do not need custom task callbacks. Like the default client, it writes snippets as:

theory SharedInlineExample imports Main begin

end

Line positions therefore shift by one line. Offsets are absolute Isabelle symbol offsets from the beginning of the written file, so they include the generated header before the snippet.

{:ok, inline_task} =
  IsabelleClient.Shared.check_text(
    pid,
    "SharedInlineExample",
    "lemma \"x = x\"\n  by simp",
    [],
    120_000
  )

IsabelleClient.messages(inline_task)

check_file/5 accepts the same explicit session_id: argument as use_theories/4, so we can target the first session even though the second session is active.

{:ok, file_task} =
  IsabelleClient.Shared.check_file(
    pid,
    Path.join(theory_dir, "SharedExample1.thy"),
    [session_id: first_session.id],
    120_000
  )

%{
  ok?: file_task.result["ok"],
  messages: IsabelleClient.messages(file_task, line: 5..6)
}

Failed tasks also go through the same event callback.

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

lemma "x = y"
  by simp

end
""")

failure_ref = make_ref()

failure_result =
  IsabelleClient.Shared.use_theories(
    pid,
    [theories: ["SharedBrokenExample"], master_dir: theory_dir],
    120_000,
    on_event: fn event -> send(parent, {:shared_failure_event, failure_ref, event}) end
  )

failed_task =
  case failure_result do
    {:ok, task} -> task
    {:error, task} -> task
  end

failure_events =
  Stream.repeatedly(fn ->
    receive do
      {:shared_failure_event, ^failure_ref, event} -> event.type
    after
      100 -> :done
    end
  end)
  |> Enum.take_while(&(&1 != :done))

%{
  status: failed_task.status,
  ok?: get_in(failed_task.result, ["ok"]),
  event_types: failure_events,
  errors: IsabelleClient.errors(failed_task)
}

{:ok, purge_result} =
  IsabelleClient.Shared.purge_theories(pid,
    theories: Enum.map(theories, fn {theory, _body, _expected} -> theory end),
    master_dir: theory_dir
  )

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

Stop And Shutdown

{:ok, first_stop_task} = IsabelleClient.Shared.stop_session(pid, first_session, 120_000)
{:ok, active_stop_task} = IsabelleClient.Shared.stop_session(pid, 120_000)

%{
  stopped_first: first_stop_task.status,
  stopped_active: active_stop_task.status
}

{:ok, nil} = IsabelleClient.Shared.shutdown_server(pid)
:ok = IsabelleClient.Shared.close(pid)