# `AtpClient.Isabelle`
[🔗](https://github.com/jcschuster/AtpClient/blob/v0.6.0/lib/atp_client/isabelle.ex#L1)

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, :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`.

## 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
    """

    # Recommended: open a session and drive it directly. `prove_theory/4`
    # returns the single-wrapped `atp_result()` shape every other backend
    # already uses.
    {:ok, session} = AtpClient.Isabelle.open_session()
    {:ok, :theorem} = AtpClient.Isabelle.prove_theory(session, theory, "Example")
    {:ok, :theorem} = AtpClient.Isabelle.prove_theory(session, body, "Example")
    :ok = AtpClient.Isabelle.close_session(session)

The single-shot `query/3` (session-less) is deprecated but still around
for callers that predate 0.6.0 — see the "Deprecations" section below.

For a single-shot TPTP/THF problem collapsed to one verdict, use `query/2`
(the `AtpClient.Backend` entry point); for per-lemma results, use
`query_tptp/2`.

## Submitting TPTP/THF problems

`query_tptp/2` and `prove_tptp/3` accept a TPTP/THF problem string 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, lemma_results} = AtpClient.Isabelle.query_tptp(problem)

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`, `query_tptp/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.

# `legacy_result`

```elixir
@type legacy_result() ::
  {:ok, AtpClient.ResultNormalization.atp_result()}
  | {:ok, map()}
  | {:error, term()}
```

Legacy shape returned by the deprecated `query/3` only: the non-raw path
wraps the normalized ATP result in an extra `:ok`, so success reads
`{:ok, {:ok, :theorem}}`. Preserved verbatim for callers that predate the
0.6.0 unwrap (notably code samples in the AtpClient paper). Prefer
`prove_theory/4` / `query_lemmas/3` / `query_tptp/2` in new code.

# `result`

```elixir
@type result() ::
  {:ok, AtpClient.ResultNormalization.szs_status()}
  | {:ok, map()}
  | {:error, term()}
```

The result of a call to `prove_theory/4`:

  * `{:ok, szs_status}` — the classified SZS verdict (default mode). Matches
    the shape every other backend returns from its `query/2` entry point;
  * `{:ok, payload_map}` — when `:raw` is `true`, the full `use_theories`
    payload (a map with `"nodes"`, `"errors"`, `"ok"`, …) returned by the
    Isabelle server;
  * `{:error, {:isabelle_failed, payload, notes}}` when the server reports a
    `FAILED` message for the task (e.g. a theory file that Isabelle could not
    load). `notes` is the list of intermediate `NOTE` payloads accumulated by
    `IsabelleClient.Task` before the failure;
  * `{:error, {:isabelle_failed, payload, hints}}` — same shape, but with
    `hints` carrying diagnostic suggestions and the `local_dir` /
    `isabelle_dir` actually used. Currently emitted when the server reports
    "Cannot load theory file";
  * other `{:error, reason}` for connection, session-start, and I/O issues.

# `close_session`

```elixir
@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.

# `open_session`

```elixir
@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`).

# `prove_lemmas`

```elixir
@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.

# `prove_theory`

```elixir
@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)

# `prove_tptp`

```elixir
@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.

# `query`

```elixir
@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
`t: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.

# `query`

> This function is deprecated. Use prove_theory/4 with an open session, or query_lemmas/3 / query_tptp/2 for one-shot calls. See @typedoc for `legacy_result` for the double-wrap this function preserves..

```elixir
@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`.

# `query_lemmas`

```elixir
@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).

# `query_tptp`

```elixir
@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).

---

*Consult [api-reference.md](api-reference.md) for complete listing*