Client for Isabelle servers, built on top of IsabelleClient from the :isabelle_elixir package.

The Isabelle server cannot accept theory text over the wire — theories have to live as .thy files on a filesystem that both the BEAM node running AtpClient and the Isabelle server can see. This module handles the file bookkeeping for you: you pass the theory body as a string, and it is written into a configured shared directory before use_theories is invoked.

Configuration

config :atp_client, :isabelle,
  host: "isabelle.example.org",
  port: 9999,
  password: System.get_env("ISABELLE_PASSWORD"),
  session: "HOL"

When the BEAM and the Isabelle server run on the same host (the usual dev setup) no further configuration is required — :local_dir defaults to a subdirectory of System.tmp_dir!/0 and the library writes .thy files there before asking Isabelle to load them. Pass theory text in, get results back; the file bookkeeping is hidden.

Zero-config: isabelle on $PATH

If the isabelle executable is discoverable (either on $PATH or via the ISABELLE_TOOL environment variable), the bundled :isabelle_elixir package can spin up a local resident server on demand. This removes any need to configure host/port/password by hand:

# Start a throwaway server (uses `isabelle` from $PATH).
{:ok, server} = IsabelleClient.start_server()

opts = [host: server.host, port: server.port, password: server.password]

{:ok, session} = AtpClient.Isabelle.open_session(opts)
{:ok, %AtpClient.Result{status: :theorem}} =
  AtpClient.Isabelle.prove_theory(session, ~S"""
  lemma "P \<or> \<not> P" by auto
  """, "Example")
:ok = AtpClient.Isabelle.close_session(session)

# When you're done, stop the server:
IsabelleClient.Server.kill(server.name)

A minimal config/config.exs reduces the per-call opts to nothing — after the one-time start_server/0 call, put the returned coordinates into the application env once and forget about them.

Paths: local_dir vs. isabelle_dir

Only relevant when the BEAM node and the Isabelle server see the shared directory under different paths. In that case set both explicitly:

config :atp_client, :isabelle,
  local_dir: "/shared/problems",
  isabelle_dir: "/data/problems"

The two common cases:

• Containers: BEAM writes to /shared/problems inside its container; the Isabelle server container has the same volume mounted at /data/problems.
• Windows + Cygwin: BEAM on Windows sees C:/Users/you/thy; Isabelle started from a Cygwin shell sees the same directory as /cygdrive/c/Users/you/thy.

Paths given via isabelle_dir are passed through verbatim — the library does not try to translate Windows paths to POSIX or vice-versa. When unset, :isabelle_dir defaults to :local_dir.

Results

Every proving call returns {:ok, %AtpClient.Result{}} or {:error, reason}. Isabelle prints no SZS lines; the status is read from the server's messages by AtpClient.Isabelle.Verdict, and the result's evidence is {:backend, AtpClient.Isabelle}. output is the text of those messages, and details carries what the call knows beyond the status:

• prove_theory/4 — %{payload: map()}, the use_theories payload as the server returned it.
• prove_lemmas/4, query_lemmas/3, prove_tptp/3 and query/2 — %{lemmas: [lemma_result], payload: map()}, one entry per lemma in the order of the lemma declarations, each %{name: name, status: status}. The result's own status is the weakest link: :theorem only when every lemma was discharged, otherwise the first other status in lemma order. A body with no lemmas is :gave_up.

Example

Pass a full theory or just the body — bare text is automatically wrapped in theory <name> imports Main begin ... end:

# Full theory
theory = ~S"""
theory Example imports Main begin
lemma "P \<or> \<not> P" by auto
end
"""

# Or just the body (equivalent)
body = ~S"""
lemma "P \<or> \<not> P" by auto
"""

{:ok, session} = AtpClient.Isabelle.open_session()
{:ok, %{status: :theorem}} = AtpClient.Isabelle.prove_theory(session, theory, "Example")
{:ok, %{status: :theorem}} = AtpClient.Isabelle.prove_theory(session, body, "Example")
:ok = AtpClient.Isabelle.close_session(session)

Submitting TPTP/THF problems

query/2 and prove_tptp/3 take an AtpClient.Problem and route it through IsabelleClient.TPTP.isabellize_theory/1 before handing it to the per-lemma path. The bundled TPTP.thy support theory is copied into :local_dir on first use, and the generated theory imports it with unbundle from_TPTP active:

problem = ~S"""
thf(p_type, type, p: $i > $o).
thf(g, conjecture, ! [X: $i]: (p @ X | ~ (p @ X))).
"""

{:ok, result} = AtpClient.Isabelle.query(problem)
result.status           # :theorem
result.details.lemmas   # [%{name: "g", status: :theorem}]

Lemma names propagate from TPTP formula names. Line numbers are not exposed — they would refer to the generated theory, not the input TPTP source. Match on :name for UI attribution.

Cancellation

Death of the process calling query/2 or any of the session helpers is the abort signal. The session is owned by an internal GenServer that monitors the caller; on caller :DOWN it stops the underlying IsabelleClient.Shared, which closes the TCP socket to the Isabelle server. Closing the socket while a use_theories task is in flight aborts that task on the server side — per the Isabelle protocol, the running check is dropped along with the session.

IsabelleClient does not currently expose a way to cancel a single in-flight task while keeping the session open, so cancelled calls pay the session-start cost again on the next request (typically a few seconds for HOL, longer for larger sessions). Callers that need to cancel cheaply should keep the volume of cancelled work small or open multiple sessions in parallel.