IsabelleClient

IsabelleClient is the ordinary user-facing client. It keeps the socket and the current session_id in a struct, awaits Isabelle tasks for you, and adds helpers for checking text or files.

This notebook shows the ergonomic workflow: start a local HOL session, check theory text and a .thy file, use messages/2 line filters, and clean 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 A Local Session

start/1 starts a resident Isabelle server, connects to it, and starts a session. with_session/2 is the same lifecycle wrapped around a function.

{:ok, client, start_task} =
  IsabelleClient.start(
    session: "HOL",
    server_name: "livebook_client_#{System.unique_integer([:positive])}",
    timeout: 120_000
  )

{is_binary(client.session_id), start_task.status}

{:ok, "stateful"} = IsabelleClient.echo(client, "stateful")

Check Text

When the text is not a complete theory, check_text/5 wraps it as a theory importing Main.

text_body = """
lemma "x = x"
  sledgehammer
  by simp

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

{:ok, text_task} =
  IsabelleClient.check_text(client, "LiveTextExample", text_body, [], 120_000)

true = text_task.result["ok"]

Diagnostic maps include source positions. messages/2, diagnostics/2, errors/2, and warnings/2 accept line: n, line: first..last, line: [n, ...], and offset: n. The offset is matched against pos.offset..pos.end_offset.

proof_offsets =
  for line <- [6, 10],
      diagnostic <- IsabelleClient.diagnostics(text_task, line: line),
      offset = get_in(diagnostic, ["pos", "offset"]),
      is_integer(offset) do
    {line, offset}
  end

%{
  all_messages: IsabelleClient.messages(text_task),
  first_sledgehammer_command: IsabelleClient.messages(text_task, line: 5),
  first_proof_command: IsabelleClient.messages(text_task, line: 6),
  both_sledgehammer_commands: IsabelleClient.messages(text_task, line: [5, 9]),
  raw_diagnostics_on_proofs: IsabelleClient.diagnostics(text_task, line: 6..10),
  proof_offsets: proof_offsets,
  proof_messages_by_line_and_offset:
    for {line, offset} <- proof_offsets do
      {line, offset, IsabelleClient.messages(text_task, line: line, offset: offset)}
    end
}

true =
  text_task
  |> IsabelleClient.messages(line: [5, 9])
  |> Enum.any?(&String.contains?(&1, "Sledgehammer"))

true =
  text_task
  |> IsabelleClient.messages(line: [6, 10])
  |> Enum.any?(&String.contains?(&1, "theorem"))

Check A File

check_file/4 derives master_dir and theory name from the file path.

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

File.mkdir_p!(theory_dir)

theory_path = Path.join(theory_dir, "LiveFileExample.thy")

File.write!(theory_path, """
theory LiveFileExample imports Main
begin

lemma "x = x"
  sledgehammer
  by simp

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

end
""")

{:ok, file_task} = IsabelleClient.check_file(client, theory_path, [], 120_000)

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

Scoped Sessions

{:ok, scoped_messages} =
  IsabelleClient.with_session([timeout: 120_000], fn scoped ->
    {:ok, task} =
      IsabelleClient.check_text(scoped, "ScopedExample", "lemma \"x = x\"\n  by simp", [], 120_000)

    {:ok, IsabelleClient.messages(task)}
  end)

scoped_messages

Stop And Shutdown

{:ok, client, stop_task} = IsabelleClient.stop_session(client, 120_000)
{client.session_id, stop_task.status}

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