# 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.
<!-- livebook:{"break_markdown":true} -->
When using the published package, replace the dependency with `{:isabelle_elixir, "~> 0.3"}`.
```elixir
Mix.install([
{:isabelle_elixir, path: Path.expand("..", __DIR__)}
])
```
```elixir
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.
```elixir
{: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`:
```elixir
# {: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.
```elixir
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.
```elixir
{: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.
```elixir
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 \\<longrightarrow> A) \\<and> True\"\n by simp",
"theorem (?A \\<longrightarrow> ?A) \\<and> 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
```
```elixir
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(&(&1 != :done))
results_by_theory = Map.new(theory_results, &{&1.theory, &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:
```isabelle
theory SharedInlineExample imports Main begin
<your text starts on line 2>
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.
```elixir
{: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.
```elixir
{: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.
```elixir
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)
}
```
```elixir
{: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
```elixir
{: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
}
```
```elixir
{:ok, nil} = IsabelleClient.Shared.shutdown_server(pid)
:ok = IsabelleClient.Shared.close(pid)
```