AtpClient.Lint.Tptp4x (AtpClient v0.1.3)

Authoritative TPTP syntax and type checker, delegated to TPTP4x on the SystemOnTPTP deployment.

Shares the same endpoint and form convention as AtpClient.SystemOnTptp — the TPTP4x tool is exposed as a pseudo-prover on the form, so we reuse the configured :url rather than introducing a second endpoint. The system identifier is TPTP4x---0.0 (note the lowercase x and the two-part version).

When the input parses cleanly, TPTP4x echoes a normalised form of the problem and this module returns {:ok, []}. When it doesn't, TPTP4x emits ERROR: / WARNING: lines (usually with a line N, column M suffix), and we translate those into Diagnostics. Unrecognised error formats fall back to a single line-1 diagnostic carrying the raw TPTP4x output so the user can still see what the tool complained about — better than silently dropping information during a live demo.

Summary

Functions

check(problem, opts \\ [])

Runs TPTP4X on problem via the configured SystemOnTPTP endpoint.

Functions

check(problem, opts \\ [])

@spec check(
  String.t(),
  keyword()
) :: {:ok, [AtpClient.Lint.Diagnostic.t()]} | {:error, term()}

Runs TPTP4X on problem via the configured SystemOnTPTP endpoint.

Options

:url — override the endpoint URL. Defaults to the value configured under config :atp_client, :sotptp, :url;
:tptp4x_system — override the TPTP4X system identifier (default "TPTP4X---0.0"). Configurable because the identifier occasionally shifts with TPTP deployments;
:tptp4x_time_limit_sec — server-side time limit (default 10);
:request_timeout_ms — HTTP receive timeout (default (tptp4x_time_limit_sec + 5) * 1000).