# `KinoAtpClient.IsabelleRuntime`
[🔗](https://github.com/jcschuster/KinoAtpClient/blob/v0.6.0/lib/kino_atp_client/isabelle_runtime.ex#L1)

Lazy singleton that auto-manages a local Isabelle server + `HOL` session for
the Smart Cell's Isabelle backend, mirroring the workflow demonstrated in
the `isabelle_elixir` livebooks: spawn a local server, open one session,
load the bundled `TPTP.thy`, and re-use both across calls.

Compared with `AtpClient.Isabelle.query_tptp/2`, this:

  * **needs zero configuration** when the `isabelle` executable is on
    `PATH` (or `ISABELLE_TOOL` is set) — no `:password`, no `:local_dir`,
    no `:isabelle_dir`;
  * **persists** the server + session for the lifetime of the BEAM node,
    so the ~30 s `HOL` start-up only happens on the first solve click;
  * writes theory files into the **session's own `tmp_dir`** rather than
    a configured shared directory, so the BEAM and the Isabelle server
    always agree on where the theory lives.

The runtime is started as a permanent child of the package's application
supervision tree but stays *idle* until the first `query_tptp/2` call — no
Isabelle process is spawned just by loading the package.

# `available?`

```elixir
@spec available?() :: :ok | {:error, term()}
```

Returns `:ok` if a local Isabelle executable is reachable on this machine.

Probes `ISABELLE_TOOL` and then `PATH`; does not spawn anything.

# `child_spec`

Returns a specification to start this module under a supervisor.

See `Supervisor`.

# `query_tptp`

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

Checks a TPTP/THF `problem` against the auto-managed local Isabelle session
and returns the per-lemma classification.

`opts`:

  * `:proof_method` — Isabelle tactic appended after each generated `lemma`
    (default `"by auto"`).

Returns `{:ok, [%{name:, result:}]}` on success or `{:error, reason}` if
Isabelle is unavailable, the TPTP fragment failed to parse, or the
server reported a task failure.

# `reset`

Stops the running session (if any) and tears down the local server.

Useful for tests; not strictly necessary in production since the runtime
is terminated when the application shuts down.

# `start_link`

Starts the runtime supervisor child. Does not spawn Isabelle yet.

---

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