# `AtpClient.LocalExec`
[🔗](https://github.com/jcschuster/AtpClient/blob/v0.6.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. On port
close, the BEAM closes stdio pipes but does **not** signal the OS child.
A guardian process monitors the caller and issues SIGKILL to the OS child
if the caller dies (`Process.exit/2`, `Task.shutdown/2`, or any other
linked termination) before the prover returns. The wall-clock timeout 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 independent timeouts protect the caller from a wedged prover:

  * 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 line
    — the classifier maps e.g. `SZS status Timeout` to `{:ok, :timeout}`
    and `SZS status MemoryOut` to `{:ok, :memory_out}`. The status atom
    reflects what the prover reported, not a generic timeout.
  * The **wall-clock timeout** (`:wall_timeout_ms`) is enforced on the BEAM
    side: when it fires, the guardian sends SIGKILL to the OS child and the
    result is normalised to `{:ok, :timeout}` — the wall-clock kill does not
    produce a prover SZS line, so only `:timeout` can be returned on that
    path.

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

# `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`);
  * `:raw` — when `true`, skip `interpret_result/1` and return
    `{:ok, captured_stdout}` so the caller can inspect the prover's raw
    output. The `AtpClient.Backend` behaviour's `query/2` entry point always
    passes `raw: false` so the unified contract always returns an
    `atp_result()`.

---

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