Backend that invokes a locally installed, TPTP-compliant prover via Port.open/2 and reads its stdout through AtpClient.Verdict.

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

Two ways in

query/2 takes an AtpClient.Problem, writes its bytes to a temporary file and passes that to the prover. query_file/2 takes a path and passes it to the prover as it is: nothing is read or copied, and the prover resolves the file's include directives itself, against the file's directory and $TPTP.

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 :timeout. The prover printed no status line on that path, so the backend appends one of its own, % SZS status Timeout : wall-clock kill by AtpClient.LocalExec, which the result's output and comment carry.

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