@spec close_session(AtpClient.Isabelle.Session.t()) :: :ok

Stops the active Isabelle session and shuts down the underlying IsabelleClient.Shared GenServer, closing its TCP socket.

@spec open_session(keyword()) ::
  {:ok, AtpClient.Isabelle.Session.t()} | {:error, term()}

Connects to the Isabelle server, starts a session (typically HOL or Main), and returns a Session handle.

The handle is backed by a private owner process that holds the link to IsabelleClient.Shared for you, so callers do not need to trap exits: a failed connection surfaces as {:error, reason} and a later crash of the Shared process surfaces as a :DOWN if the caller monitors AtpClient.Isabelle.Session.client/1. The owner is also caller-monitored, so if the caller dies the session is shut down cleanly instead of orphaning a remote Isabelle session.

The caller is still responsible for eventually passing the handle to close_session/1 under normal control flow.

Options

• :host, :port, :password — override config;
• :session — name of the Isabelle session to start (default from config, typically "HOL");
• :session_start_timeout_ms — how long to wait for the initial session_start to complete (default 120_000).

@spec prove_lemmas(AtpClient.Isabelle.Session.t(), String.t(), String.t(), keyword()) ::
  {:ok, [AtpClient.ResultNormalization.lemma_result()]} | {:error, term()}

Like prove_theory/4, but returns one result per lemma instead of a single consolidated result.

Calls prove_theory/4 internally with raw: true and parses the payload via AtpClient.ResultNormalization.per_lemma_results/3. Returns {:ok, [lemma_result]} for a finished task, where entries follow the order of the lemma <name>: declarations in the input body:

%{
  name:   String.t(),                # lemma name from the body
  result: {:ok, :theorem} | {:ok, :counter_satisfiable} | {:ok, :satisfiable}
        | {:ok, :gave_up} | {:ok, :timeout} | {:ok, :memory_out}
}

Unnamed lemma "…" by … declarations are not represented in the result — the classifier buckets messages by lemma name extracted from the body.

Returns {:error, term()} for connection failures and for tasks that fail before producing any messages (e.g. unreadable theory files).

Options

Same as prove_theory/4 except :raw, which is always overridden.

@spec prove_theory(AtpClient.Isabelle.Session.t(), String.t(), String.t(), keyword()) ::
  result()

Writes theory_text to <local_dir>/<theory_name>.thy, asks the Isabelle server to process it in the given session, and blocks until the task finishes or fails.

If theory_text does not begin with theory, it is automatically wrapped:

theory <theory_name> imports <imports> begin
<theory_text>
end

By default the result is classified by AtpClient.ResultNormalization.interpret_isabelle_result/1 and returned as {:ok, szs_status} — the same shape every other backend produces from its query/2 entry point. Pass raw: true to get back the full use_theories payload (a map with "nodes", "ok", "errors", …) as {:ok, map()}.

Options

• :raw — return {:ok, payload_map} instead of {:ok, szs_status} (default false);
• :imports — session/theory to import when auto-wrapping (default "Main");
• :use_theories_timeout_ms — overall deadline for the task (default from config, 120_000).

Examples

# Non-raw: single-wrap SZS verdict.
{:ok, :theorem} =
  AtpClient.Isabelle.prove_theory(session, "lemma p: True by auto\n", "P")

# Raw: full server payload.
{:ok, %{"nodes" => _, "ok" => true}} =
  AtpClient.Isabelle.prove_theory(session, "lemma p: True by auto\n",
    "P", raw: true)

@spec prove_tptp(AtpClient.Isabelle.Session.t(), String.t(), keyword()) ::
  {:ok, [AtpClient.ResultNormalization.lemma_result()]} | {:error, term()}

Like prove_lemmas/4, but takes a TPTP/THF problem string instead of an Isabelle theory.

The problem is converted to an Isabelle theory body via IsabelleClient.TPTP.isabellize_theory/1, which maps thf(name, axiom, …) to axiomatization, thf(name, type, …) to consts/typedecl/ type_synonym, and thf(name, theorem|conjecture, …) to lemma. The generated body is preceded by unbundle from_TPTP so that the TPTP/THF notation parses inside Isabelle, then handed to prove_lemmas/4 with imports: "TPTP".

The bundled TPTP.thy support theory is copied into the configured :local_dir on first use so Isabelle's loader can resolve imports "TPTP" from the generated theory file. Existing files are not overwritten.

Result attribution

Entries in the returned lemma_result() list follow the order of the thf(…, conjecture, …) declarations in the input problem and carry the TPTP formula name as :name. Line numbers are intentionally not exposed: they would refer to the generated theory body rather than the caller's TPTP source.

Options

Same as prove_lemmas/4, plus:

• :theory_name — name to use for the generated Isabelle theory (default: a content-derived AtpClient_<hash> string). Useful for stable filenames across runs.
• :raw — accepted for opts compatibility with prove_theory/4, but ignored: the return of prove_tptp/3 is inherently a per-lemma list, so the raw use_theories payload would be attached to the generated Isabelle theory (with axiomatization, unbundle from_TPTP, and the support theory in scope) rather than to the caller's TPTP source, and would carry no useful line/anchor mapping back. If you need the raw payload for a TPTP problem, call IsabelleClient.TPTP.isabellize_theory/1 yourself and pass the result to prove_theory/4 with raw: true.
• :proof_method — Isabelle tactic appended to each generated lemma (default "by auto"). The isabellizer emits lemma declarations without proofs, which Isabelle treats as unfinished goals; a tactic must be supplied for the goal to close (or be withdrawn). Pass "by metis" for first-order portfolio reasoning, or "sledgehammer nitpick oops" to probe both proof and countersatisfiability; the latter relies on the per-lemma classifier recognising sledgehammer's "found a proof" and nitpick's verdicts directly, so oops is fine — {:ok, :theorem} / {:ok, :counter_satisfiable} / {:ok, :satisfiable} come from the tool messages, not from a theorem name: completion.

Errors

• {:error, {:tptp_thy_copy_failed, reason}} — could not place TPTP.thy next to the generated theory in :local_dir;
• {:error, {:tptp_parse, message}} — isabellize_theory/1 raised (the parser is tolerant by design, so this should be rare);
• everything prove_lemmas/4 can return.

@spec query(
  String.t(),
  keyword()
) :: AtpClient.ResultNormalization.atp_result() | {:error, term()}

Behaviour entry point: proves problem (a TPTP-format string) and collapses the per-lemma results from query_tptp/2 into a single AtpClient.ResultNormalization.atp_result/0.

Aggregation is weakest-link: any non-{:ok, :theorem} entry wins, so the unified result only reads {:ok, :theorem} when every isabellized lemma was discharged. Callers that need per-lemma detail should use query_tptp/2 directly.

@spec query(String.t(), String.t(), keyword()) :: legacy_result()

Deprecated. Opens a session, calls prove_theory/4, closes the session, and returns the historical double-wrapped shape ({:ok, atp_result()} in non-raw mode — success reads {:ok, {:ok, :theorem}}).

Preserved verbatim so callers that predate the 0.6.0 unwrap keep working (in particular, the code samples in the AtpClient paper). New code should call one of:

• prove_theory/4 with a session you own — returns {:ok, szs_status()} (single-wrap), matching every other backend;
• query_lemmas/3 for a one-shot theory with per-lemma results;
• query_tptp/2 for a TPTP/THF problem;
• query/2 (AtpClient.Backend entry point) for a TPTP/THF problem collapsed to a single verdict.

opts must be passed explicitly (use [] for none) — a default value would shadow query/2 from AtpClient.Backend.

@spec query_lemmas(String.t(), String.t(), keyword()) ::
  {:ok, [AtpClient.ResultNormalization.lemma_result()]} | {:error, term()}

Convenience wrapper: opens a session, calls prove_lemmas/4, and unconditionally closes the session afterwards (even on error).

@spec query_tptp(
  String.t(),
  keyword()
) :: {:ok, [AtpClient.ResultNormalization.lemma_result()]} | {:error, term()}

Convenience wrapper: opens a session, calls prove_tptp/3, and unconditionally closes the session afterwards (even on error).