Stateful Agent that caches the system identifiers currently advertised by
a SystemOnTPTP deployment.
The initial refresh is triggered in the background once the agent starts.
get_systems_list/0 and systems/0 block on the first call until the
initial refresh completes or refresh_timeout_ms elapses. Subsequent calls
return the cached list immediately. Callers can force a re-fetch via
refresh_systems_list/0.
Names and identifiers
SystemOnTPTP identifies a system as <name>---<version>, Vampire---5.0.1,
and keeps only the current version of each. resolve/1 accepts either form:
an identifier is checked against the advertised list, and a bare name is
resolved to the latest version advertised under it, so a caller writes
"Vampire" and is not tied to a version string that changes under them.
The agent is started with the application under
config :atp_client, :sotptp, auto_refresh: true (the default). Without it,
nothing is cached and resolve/1 passes identifiers through unchanged, since
it has nothing to check them against.
Summary
Functions
Returns a specification to start this module under a supervisor.
Returns the list of available provers (e.g. "cvc5---1.3.0"): every
advertised system except the format converters, checkers and statistics
tools SystemOnTPTP lists alongside them.
The name of a system identifier: "Vampire" for "Vampire---5.0.1". A bare
name is returned as it is.
Refreshes the cached system list via a synchronous query to SystemOnTPTP.
Resolves a system name or identifier against the advertised systems.
Links the module as an Agent process with the caller process and
schedules a background refresh of the system list.
Every system the deployment advertises, tools included.
Functions
Returns a specification to start this module under a supervisor.
See Supervisor.
@spec get_systems_list() :: [String.t()]
Returns the list of available provers (e.g. "cvc5---1.3.0"): every
advertised system except the format converters, checkers and statistics
tools SystemOnTPTP lists alongside them.
Blocks on the first call until the background refresh triggered at startup
completes or refresh_timeout_ms elapses; subsequent calls return the
cached list immediately.
The name of a system identifier: "Vampire" for "Vampire---5.0.1". A bare
name is returned as it is.
iex> AtpClient.SystemOnTptp.Provers.name("Vampire---5.0.1")
"Vampire"Refreshes the cached system list via a synchronous query to SystemOnTPTP.
Accepts the same options as the rest of the SoTPTP API:
:url— SystemOnTPTP endpoint (defaults to the configured URL);:refresh_timeout_ms— request timeout in ms.
@spec resolve(String.t(), [String.t()]) :: {:ok, String.t()} | {:error, {:unknown_system, String.t()}}
Resolves a system name or identifier against the advertised systems.
An identifier ("E---3.5.1") must be advertised as written. A bare name
("E") resolves to the latest version advertised under it, versions being
compared component-wise as numbers. When no list is available — the agent is
not running, or the deployment could not be reached — an identifier is passed
through unchanged and a bare name cannot be resolved.
iex> systems = ["E---3.5.1", "Vampire---5.0.1", "Vampire---4.8", "TPTP4X---0.0"]
iex> AtpClient.SystemOnTptp.Provers.resolve("Vampire", systems)
{:ok, "Vampire---5.0.1"}
iex> AtpClient.SystemOnTptp.Provers.resolve("Vampire---4.8", systems)
{:ok, "Vampire---4.8"}
iex> AtpClient.SystemOnTptp.Provers.resolve("Vampire---4.7", systems)
{:error, {:unknown_system, "Vampire---4.7"}}
iex> AtpClient.SystemOnTptp.Provers.resolve("Nope", systems)
{:error, {:unknown_system, "Nope"}}
iex> AtpClient.SystemOnTptp.Provers.resolve("Nope---1", [])
{:ok, "Nope---1"}Links the module as an Agent process with the caller process and
schedules a background refresh of the system list.
@spec systems() :: [String.t()]
Every system the deployment advertises, tools included.
Blocks like get_systems_list/0. Returns [] when the agent is not running.