AtpClient.LocalExec (AtpClient v0.3.0)

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 both to {:ok, :timeout} / {:ok, :out_of_resources}.
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

Summary

Types

result()

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

Functions

query(problem, opts \\ [])

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

resolve_binary(opts \\ [])

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

Types

result()

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

Same as 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.

Functions

query(problem, opts \\ [])

@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(opts \\ [])

@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.