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.4"}

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. If a command or task times out, the shared connection is currently closed conservatively (reusing the socket before the stale reply is handled could return the wrong result to a later caller).

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.

For TPTP/THF examples, IsabelleClient.TPTP.check/5 wraps check_text/5 with Unicode output, routine message filtering, and optional from:, to:, and show_thf_app: notation setup.

More Examples

The main tutorials are in the Livebooks:

livebook_examples/Client.livemd: default client, diagnostics, line/offset filtering, sessions, checking files/text, building sessions.
livebook_examples/ClientShared.livemd: shared process-owned client for concurrent callers.
livebook_examples/ClientRaw.livemd: raw socket usage, server management, protocol commands, explicit async tasks.
livebook_examples/Unification.livemd: Isabelle unification and matching examples from Elixir.
livebook_examples/TPTP.livemd: TPTP/THF-style syntax and pretty-printing.

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)

Next Page → Client