# `AtpClient.Lint.Tptp4x`
[🔗](https://github.com/jcschuster/AtpClient/blob/v0.1.3/lib/atp_client/lint/tptp4x.ex#L1)

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 `Diagnostic`s. 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.

# `check`

```elixir
@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`).

---

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