# `AtpClient.Isabelle`
[🔗](https://github.com/jcschuster/AtpClient/blob/v0.5.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.

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

    {:ok, :theorem} = AtpClient.Isabelle.query(theory, "Example", [])
    {:ok, :theorem} = AtpClient.Isabelle.query(body, "Example", [])

For fine-grained workflows, open a session once and reuse it:

    {:ok, session} = AtpClient.Isabelle.open_session()
    {:ok, result1} = AtpClient.Isabelle.prove_theory(session, theory1, "T1")
    {:ok, result2} = AtpClient.Isabelle.prove_theory(session, theory2, "T2")
    :ok = AtpClient.Isabelle.close_session(session)

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

# `result`

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

The result of a call to `prove_theory/4` or `query/3`:

  * `{:ok, result}` where `result` is either the normalized ATP result or the
    raw `use_theories` payload (a map with `"nodes"`, `"errors"`, `"ok"`, …),
    depending on the `:raw` option;
  * `{: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.

# `lemma_specs`

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

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

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

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

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

# `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*