Isabelle Elixir

Elixir clients for the Isabelle server.

The library speaks Isabelle's server protocol directly. See Chapter 4 in the Isabelle system manual for the specification.

Clients

IsabelleClientMini is the low-level building block. It is stateless, exposes the TCP socket, and gives you explicit command/3, async_command/3, and await_task/3 helpers.

IsabelleClient is the default client for scripts and notebooks. It keeps the socket and current session_id in a struct, and awaits asynchronous Isabelle tasks for the common session workflow.

IsabelleClientFull is a GenServer wrapper. It owns the socket, so callers may safely share it across processes. Calls are serialized by design.

Tutorial Livebooks

The notebooks in livebook_examples/ are intended to be read and run in this order:

  1. IsabelleClientMini.livemd introduces the wire-level building blocks and explicit task handling.
  2. IsabelleClient.livemd shows the default stateful client for ordinary use.
  3. IsabelleClientFull.livemd shows the process-owning client and why it is the right choice when multiple Elixir processes share one Isabelle connection.

Together they serve as the tutorial for the library. They start local Isabelle servers, run smoke tests, build and start a HOL session, check theories, purge, stop, and clean up. The "Full" notebook additionally demonstrates concurrency-safe access.

Example

Make sure Isabelle is available on PATH:

export PATH=/path/to/Isabelle2025-2/bin:$PATH

Then:

{:ok, [server]} = IsabelleClientMini.new_server("elixir", 0)

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

{:ok, client, _task} = IsabelleClient.start_session(client, %{"session" => "HOL"})

File.write!("/tmp/Example.thy", """
theory Example imports Main
begin

theorem "x = x"
  sledgehammer by simp

proposition "x = y"
  nitpick oops

end
""")

{:ok, task} =
  IsabelleClient.use_theories(client, %{
    "theories" => ["Example"],
    "master_dir" => "/tmp"
  })

IO.puts(IsabelleClientMini.extract_results(task))

{:ok, _client, _task} = IsabelleClient.stop_session(client)