# `AtpClient.LocalExec`
[🔗](https://github.com/jcschuster/AtpClient/blob/v0.5.0/lib/atp_client/local_exec.ex#L1)

Backend that invokes a locally installed, TPTP-compliant prover via
`Port.open/2` and normalizes its stdout through
`AtpClient.ResultNormalization.interpret_result/1`.

No authentication, no polling: the prover runs to completion (or until one of
the two timeouts fires) and the captured stdout is classified by the same
SZS-aware classifier used for the SystemOnTPTP and StarExec backends.

## Cancellation

The prover is run through a port owned by the calling process. If that
process dies (`Process.exit/2`, `Task.shutdown/2`, or any other linked
termination), the BEAM closes the port and the OS child receives SIGKILL —
no orphaned prover lingers after a cancelled `query/2`. The wall-clock
timeout below uses the same mechanism.

Process-group cleanup is **not** performed: SIGKILL reaches only the direct
child, so a prover that forks helper subprocesses may leak them. This is
rare in the TPTP ecosystem and is left for a follow-up.

## Two-layered timeout

Two timeouts protect the caller from a wedged prover, and both fold into the
same `{:ok, :timeout}` result so callers do not have to branch on the
failure mode:

  * The **prover-side CPU limit** (`:cpu_timeout_s`) is passed to the prover
    via the configured `:args`. A prover that honors it (E's `--cpu-limit`,
    Vampire's `-t`, …) will exit cleanly and emit a real
    `SZS status Timeout` or `SZS status ResourceOut` — the classifier maps
    these to `{:ok, :timeout}` / `{:ok, :resource_out}`.
  * The **wall-clock timeout** (`:wall_timeout_ms`) is enforced on the BEAM
    side: when it fires, the port is closed and the OS child is killed,
    and the kill is mapped to the same `{:ok, :timeout}`.

By default `:wall_timeout_ms` is `(cpu_timeout_s + 10) * 1000`, leaving the
prover ten extra seconds to flush its `SZS status` line before the kill.

## Configuration

    config :atp_client, :local_exec,
      binary: "eprover",       # required; resolved with System.find_executable/1
      args: ["--auto", "--tstp-format"],
      cpu_timeout_s: 30,
      wall_timeout_ms: 45_000  # optional; computed from cpu_timeout_s if unset

Any setting may be overridden per call:

    AtpClient.LocalExec.query(problem, binary: "vampire", args: ["--mode", "casc"])

Absolute paths are accepted verbatim; otherwise the binary is looked up on
`PATH` via `System.find_executable/1` and `{:error, {:prover_not_found, name}}`
is returned when missing.

## Building the args

`LocalExec` appends the problem file path as the **last** positional argument
to the configured `:args`. Provers that take the file path elsewhere should
embed the literal `"{{problem}}"` placeholder in `:args`; it is substituted
with the temp file path before invocation and suppresses the default append.

    args: ["--input-file={{problem}}", "--cpu-limit=60"]

"runSolver" and "benchExec" could help

# `result`

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

Same as `t:AtpClient.ResultNormalization.atp_result/0`, with one extra
failure shape specific to `LocalExec`:

  * `{:error, {:prover_not_found, name}}` — `System.find_executable/1`
    returned `nil` for the configured `:binary`.

Both the prover-side CPU limit and the BEAM-side wall-clock kill surface
as `{:ok, :timeout}`; see "Two-layered timeout" in the module doc.

# `query`

```elixir
@spec query(
  String.t(),
  keyword()
) :: result()
```

Runs the configured prover against `problem` (a TPTP problem in a string)
and returns the normalized result.

See the module doc for the option list. All keys may also be set per-call:

  * `:binary` (required) — the prover executable name or an absolute path;
  * `:args` — extra arguments to pass before the problem file path
    (default `[]`). Embed `"{{problem}}"` to control where the file path is
    inserted; otherwise it is appended last;
  * `:cpu_timeout_s` — CPU limit hint reported to callers and used to derive
    the default wall-clock timeout (default `60`). `LocalExec` does **not**
    inject a `--cpu-limit` flag for you — encode that in `:args` so each
    prover gets the flag spelling it understands;
  * `:wall_timeout_ms` — BEAM-side wall-clock kill (default
    `(cpu_timeout_s + 10) * 1000`).

# `resolve_binary`

```elixir
@spec resolve_binary(keyword()) :: {:ok, String.t()} | {:error, term()}
```

Returns the absolute path of the configured prover binary, or
`{:error, {:prover_not_found, name}}` if it can't be located.

Useful in startup checks and for surfacing a clear error before the first
`query/2` call.

---

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