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