atp_client

defmodule AtpClient do
  @moduledoc """
  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 [
    AtpClient.SystemOnTptp,
    AtpClient.StarExec,
    AtpClient.Isabelle,
    AtpClient.LocalExec
  ]

  @doc """
  Returns the modules implementing `AtpClient.Backend`. Iterate this in a
  configuration UI to discover what's wireable without hard-coding the list.
  """
  @spec backends() :: [module()]
  def backends, do: @backends
end