# `AtpClient`
[🔗](https://github.com/jcschuster/AtpClient/blob/v0.5.0/lib/atp_client.ex#L1)

Elixir client for external automated theorem provers.

Four backends are supported:

  * **SystemOnTPTP** — public tptp.org HTTP form API; see
    `AtpClient.SystemOnTptp`.
  * **StarExec** — self-hosted StarExec instances; see `AtpClient.StarExec`.
  * **Isabelle** — `isabelle server` instances via `isabelle_elixir`; see
    `AtpClient.Isabelle`.
  * **LocalExec** — a locally installed TPTP-compliant prover binary
    (e.g. E, Vampire) invoked via `System.cmd/3`; see `AtpClient.LocalExec`.
    Run `scripts/build_eprover.sh` to install E into `priv/bin/`.

Each backend reads its settings through `AtpClient.Config`, which layers
`config/config.exs` on top of the library defaults and lets per-call options
override everything. See the `AtpClient.Config` module docs for details.

## Configuration

Settings are resolved from three sources, in increasing precedence:

1. Library defaults (declared in `AtpClient`'s `mix.exs`).
2. Application environment (typically `config/config.exs`).
3. Per-call keyword options passed to the relevant function.

Only the settings required by the backends you actually use need to be set.

    # config/config.exs
    import Config

    config :atp_client, :sotptp,
      # The default points at tptp.org; override for a mirror or internal
      # deployment:
      url: "https://tptp.org/cgi-bin/SystemOnTPTPFormReply",
      default_time_limit_sec: 10

    config :atp_client, :starexec,
      base_url: "https://starexec.example.org/starexec",
      username: System.get_env("STAREXEC_USER"),
      password: System.get_env("STAREXEC_PASS")

    config :atp_client, :isabelle,
      host: "isabelle.example.org",
      port: 9999,
      password: System.get_env("ISABELLE_PASSWORD"),
      session: "HOL"

    # Same-host setups need nothing more — `:local_dir` defaults to a
    # subdirectory of `System.tmp_dir!/0`. Only set `:local_dir` and
    # `:isabelle_dir` when the two sides see the directory under different
    # paths (containers, Cygwin).

    config :atp_client, :local_exec,
      binary: "eprover",
      args: ["--auto", "--tstp-format", "--cpu-limit=10"],
      cpu_timeout_s: 10

Any setting may be overridden for a single call:

    AtpClient.Isabelle.query(theory, "Example", session: "Main", raw: true)

# `backends`

```elixir
@spec backends() :: [module()]
```

Returns the modules implementing `AtpClient.Backend`. Iterate this in a
configuration UI to discover what's wireable without hard-coding the list.

---

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