TPTP4X as a Tptp.Analyzer: syntax and type findings from the TPTP World's own checker, run on the configured SystemOnTPTP deployment.

Tptp.Lint reads a file against the published BNF and the :== conditions, which is everything the grammar states. What it does not state is the typing of a formula against its declarations; TPTP4X checks that, so this analyzer runs it remotely and brings its messages back as Tptp.Diagnostics with byte spans on the analysed source.

analysis = Tptp.analyze(source)

Tptp.Analyzer.run_all(analysis, [Tptp.Lint, AtpClient.Analyzer.Tptp4x])
# [{:tptp_lint, [...]}, {:tptp4x, [...]}]

An editor runs the remote pass only when the local one found no error, since the user will fix the local error first and TPTP4X's view of a file that does not parse adds noise:

if Tptp.Diagnostic.any_errors?(analysis.diagnostics),
  do: [],
  else: AtpClient.Analyzer.Tptp4x.analyze(analysis, [])

The remote call

TPTP4X is exposed on the SystemOnTPTP form as a pseudo-system, so this module reuses the configured :url under config :atp_client, :sotptp rather than introducing a second endpoint. The identifier is TPTP4X---0.0; it is configurable because it has shifted between deployments.

A clean file comes back as TPTP4X's normalised echo of it and yields no diagnostics. Otherwise TPTP4X prints ERROR: Line N Char M … and WARNING: … lines, which become diagnostics with the code TPTP4X, positioned by Tptp.Span.offset/3. A message TPTP4X positions outside the source is reported at offset 0 rather than dropped.

Failure

analyze/2 returns [] when the deployment cannot be reached, since a network failure is not a finding about the file. check/2 returns the failure as {:error, reason} for callers who want to show it.