IsabelleClientFull

IsabelleClientFull 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.

The Full 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

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_note callbacks lightweight; sending a message to another process is a good pattern.

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 A Shared Client

Without a :password, start_link/1 starts a local Isabelle server and session. The returned pid is the shared client handle.

{:ok, pid} =
  IsabelleClientFull.start_link(
    session: "HOL",
    server_name: "livebook_full_#{System.unique_integer([:positive])}",
    timeout: 120_000
  )

Process.alive?(pid)

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: "full", n: n, framed: String.duplicate("#{n}", 120)}
          {:ok, echoed} = IsabelleClientFull.echo(pid, payload)
          {:echo, echoed["n"]}

        {:help, n} ->
          {:ok, commands} = IsabelleClientFull.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)

Concurrent Theory Tasks

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

parent = self()
note_ref = make_ref()
done_ref = make_ref()

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

File.mkdir_p!(theory_dir)

theories = [
  {"FullExample1", "lemma \"x = x\"\n  by simp", "theorem ?x = ?x"},
  {"FullExample2", "lemma \"xs @ [] = xs\"\n  by simp", "theorem ?xs @ [] = ?xs"},
  {"FullExample3", "lemma \"(A \\ A) \\ True\"\n  by simp",
   "theorem (?A \\ ?A) \\ True"}
]

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.shuffle()
  |> Enum.map(fn {theory, _body, expected_message} ->
    Task.async(fn ->
      on_note = fn note ->
        send(parent, {:full_note, note_ref, theory, note["task"], note["message"]})
      end

      {:ok, task} =
        IsabelleClientFull.use_theories(
          pid,
          [theories: [theory], master_dir: theory_dir],
          120_000,
          on_note: on_note
        )

      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, {:full_done, done_ref, result})
      result
    end)
  end)

completion_order =
  for _ <- theory_tasks do
    receive do
      {:full_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)

notes =
  Stream.repeatedly(fn ->
    receive do
      {:full_note, ^note_ref, theory, task_id, message} -> {theory, task_id, message}
    after
      100 -> :done
    end
  end)
  |> Enum.take_while(&amp;(&amp;1 != :done))

notes_by_theory = Enum.group_by(notes, fn {theory, _task_id, _message} -> theory end)
results_by_theory = Map.new(theory_results, &amp;{&amp;1.theory, &amp;1})

true = Map.keys(results_by_theory) |> Enum.sort() == ~w(FullExample1 FullExample2 FullExample3)
true = Map.keys(notes_by_theory) |> Enum.sort() == ~w(FullExample1 FullExample2 FullExample3)

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

%{
  completion_order: completion_order,
  checked_theories: Map.keys(results_by_theory) |> Enum.sort(),
  note_count: length(notes),
  notes_routed_to_callers?: true
}

Check Text Helper

check_text/5 is available on Full too. Use it when you do not need a custom on_note callback.

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

IsabelleClient.messages(inline_task)

{:ok, purge_result} =
  IsabelleClientFull.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, stop_task} = IsabelleClientFull.stop_session(pid, 120_000)
stop_task.status

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