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

Elixir client for external automated theorem provers.

Three 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`.

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"),
      # Directory shared between this node and the Isabelle server. If the two
      # see the same files under different paths (e.g. because one runs inside
      # a container), set `isabelle_dir` separately:
      local_dir: "/shared/problems",
      isabelle_dir: "/shared/problems",
      session: "HOL"

Any setting may be overridden for a single call:

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

---

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