@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 lemma_specs(String.t()) :: [AtpClient.ResultNormalization.lemma_spec()]

Extracts the lemma specs (name + body-line range) from a theory body.

Walks the body line-by-line, picking out lemma <name>: or lemma <name>[…]: declarations and computing each lemma's range as [its line .. (line before the next lemma)]. Used by prove_lemmas/4 and prove_tptp/3 to feed ResultNormalization.per_lemma_results/3 without having to re-parse the body inside the classifier.

@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 session.client. 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 interpreted by AtpClient.ResultNormalization.interpret_isabelle_result/1. Pass raw: true to get back the full use_theories payload (a map with "nodes", "ok", "errors", …) returned by the Isabelle server.

Options

• :raw — return the raw payload map (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).

@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.
• :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()) :: result()

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

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).