Isabelle Elixir

Elixir clients for the Isabelle server.

The library talks to Isabelle's TCP server protocol directly. For protocol details, see chapter 4 of the Isabelle system manual.

Installation

{:isabelle_elixir, "~> 0.3"}

Local server helpers need the Isabelle executable. Set ISABELLE_TOOL when isabelle is not already on PATH:

export ISABELLE_TOOL=/path/to/Isabelle2025-2/bin/isabelle

Which Client?

Start with IsabelleClient (see corresponding livebook tutorial). It owns one socket and keeps a local LIFO stack of sessions, with the most recently started session treated as active.

Use IsabelleClient.Shared when several Elixir processes should share one connection. It owns the socket in a GenServer and routes async task replies by Isabelle task id.

Use IsabelleClient.Raw when you want protocol-level control: explicit socket ownership, explicit session ids, and explicit task waiting.

Quick Start

{:ok, server} = IsabelleClient.start_server()

{:ok, client} = IsabelleClient.connect(server)

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



{:ok, task} =

  IsabelleClient.check_text(client, "Example", """

  theorem "x = x"

    by simp

  """)



IsabelleClient.messages(task)

check_text/5 is a convenience for snippets. It writes a temporary theory of this shape:

theory Example imports Main begin

<your text starts on line 2>

end

So Isabelle diagnostics report line 1 as the generated header; snippet line n appears as Isabelle line n + 1. Offsets are absolute Isabelle symbol offsets from the start of the generated file.

More Examples

The main tutorial is in the Livebooks:

  1. livebook_examples/IsabelleClient.livemd: default client, diagnostics, line/offset filtering, sessions, checking files/text, building sessions.
  2. livebook_examples/IsabelleClientShared.livemd: shared process-owned client for concurrent callers.
  3. livebook_examples/IsabelleClientRaw.livemd: raw socket usage, server management, protocol commands, explicit async tasks.

Existing Servers

You do not have to start a local server from Elixir. If an Isabelle server is already reachable, connect with its password, host, and port:

{:ok, client} =

  IsabelleClient.connect("server-password",

    host: "isabelle.example.org",

    port: 9999

  )

The same applies to IsabelleClient.Shared and IsabelleClient.Raw.

Sessions

Isabelle sessions live in the server and are addressed by session id. IsabelleClient keeps local session bookkeeping for ergonomics:

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



IsabelleClient.sessions(client)

IsabelleClient.active_session(client)

Starting a session pushes it onto client.sessions. Stopping a session removes it; if it was active, the previous session becomes active again. Pass session_id: when you want to address a non-active session explicitly.

Sessions may outlive a client connection, and a client may use a session started elsewhere if given its id. client.sessions is local state, not a server-side session query.

Results

messages/1 returns user-facing Isabelle messages. diagnostics/1 returns the raw diagnostic maps, including positions when Isabelle provides them.

IsabelleClient.messages(task)

IsabelleClient.errors(task)

IsabelleClient.warnings(task, line: 5)

IsabelleClient.diagnostics(task, file: "Example.thy", line: 5, offset: 42)

Position filters support file:, line:, and offset:. Offsets are Isabelle symbol offsets, not columns.

Common results can also be decoded:

IsabelleClient.session_build_result(task)

IsabelleClient.use_theories_result(task)

IsabelleClient.nodes(task)

IsabelleClient.exports(task)