# `Tptp.Resolver.Http`
[🔗](https://github.com/jcschuster/tptp/blob/v0.1.3/lib/tptp/resolver/http.ex#L1)

Fetches from tptp.org over HTTPS, through a local cache.

For use where the TPTP distribution is not installed locally. It is never a
default and is never composed implicitly, network access being a decision for the
caller.

    Tptp.Unit.from_name("Problems/PUZ/PUZ001+1.p", resolver: Tptp.Resolver.Http)

    Tptp.Unit.from_file("problem.p",
      resolver: {Tptp.Resolver.Cascade,
                 resolvers: [Tptp.Resolver.Fs, Tptp.Resolver.Http]}
    )

## The SeeTPTP mapping

tptp.org serves the library through a CGI script taking the components of a name
rather than a path:

    Axioms/SET007+0.ax   ->  ?Category=Axioms&File=SET007+0.ax
    SET007+0.ax          ->  ?Category=Axioms&File=SET007+0.ax
    Problems/PUZ/PUZ001+1.p  ->  ?Category=Problems&Domain=PUZ&File=PUZ001+1.p
    PUZ001+1.p           ->  ?Category=Problems&Domain=PUZ&File=PUZ001+1.p

A bare problem name takes its domain from the leading three letters, following
the TPTP naming convention. `url/2` is public so that the mapping can be read and
tested without network access.

The `+` in `SET007+0.ax` is part of the name, and form encoding converts it to a
space unless the parameter is escaped. Every parameter is escaped.

## SeeTPTP answers with a web page, not a file

Every successful response is an HTML page containing the file within a `<pre>`
block, and the block is not the file: SeeTPTP inserts an `<A NAME="...">` anchor
before each formula. `contents/1` recovers the file and is public so that it can
be read and tested without network access.

Two steps, in this order:

  1. **Remove the markup.** Every `<` belonging to the TPTP source arrives as
     `&lt;`, the page escaping `<` while leaving `>` and `&` unescaped, so a
     literal `<` within the block is inserted markup rather than `<=>`, `<~>` or
     `<<`. This is what renders removing `<[^>]*>` sound in this context.
  2. **Resolve the entities.** `&lt;` becomes `<` only at this point, so it cannot
     be treated as a tag by the first step.

The reverse order would delete every equivalence in the file.

A page containing no `<pre>` block is SeeTPTP's error page and is reported as
such. A body that is not HTML is passed through unmodified, which is what a plain
file server behind `:base_url` returns.

## Caching

Every response is written to `:cache_dir` under a digest of its URL, and a hit is
served from disk without network access, so a corpus run costs one request per
file. The default is `~/.cache/tptp`; set `:cache_dir` to `false` to disable
caching.

## `:inets` and `:ssl` are started here, not by the application

Both are absent from this library's `extra_applications`. Listing them would
start two OTP applications in every consumer, including those whose resolver is
`Tptp.Resolver.None` and which open no socket. `started/0` starts them on the path
about to issue a request; a cache hit does not reach it.

### Why that needs more than `ensure_all_started/1`

Mix prunes the code path to the applications named in the `.app` file, so dropping
`:ssl` from `extra_applications` also removes `ssl`, `public_key` and `asn1` from
the code path. The application controller still reports them as *running* — they
are, in the VM — while their modules are not loadable, and `ensure_all_started/1`
cheerfully answers `{:ok, []}`. The first symptom is an `:undef` from deep inside
`:httpc`, raised while it builds the default HTTPS options.

So `started/0` puts the ebin directories back on the path first, resolving them
under `:code.root_dir/0` rather than `:code.lib_dir/1` — the latter consults the
code path it is trying to repair and answers `:bad_name`. It then checks a
representative module of each application is really loadable, so a genuine absence
is reported as a sentence rather than surfacing later as an `:undef`.

In a release the applications must be included as usual; nothing here can conjure
code that was not shipped, and `started/0` says so plainly if it was not.

## Failure

A non-200, a timeout, a connection error or a body that looks like SeeTPTP's HTML
error page all come back as `{:error, reason}`, and `Tptp.Include` turns that into
a diagnostic. Nothing here raises and nothing retries — a resolver that retries on
its own turns one slow file into a much slower run without telling anyone.

# `contents`

```elixir
@spec contents(binary()) :: {:ok, binary()} | :error
```

The TPTP file inside a SeeTPTP response.

A body that is not HTML is already the file and comes back unchanged. An HTML body
must carry a `<pre>` block, which is unwrapped and unescaped; without one it is
SeeTPTP's error page and the answer is `:error`.

    iex> Tptp.Resolver.Http.contents("fof(a, axiom, p).")
    {:ok, "fof(a, axiom, p)."}

    iex> Tptp.Resolver.Http.contents(~s|<pre><A NAME="a"></A>fof(a, axiom, p &lt;=> q).</pre>|)
    {:ok, "fof(a, axiom, p <=> q)."}

    iex> Tptp.Resolver.Http.contents("<html><body>No such file</body></html>")
    :error

# `started`

```elixir
@spec started() :: :ok | {:error, binary()}
```

Make `:inets` and `:ssl` usable, if they are not already.

Idempotent, and a handful of module lookups once they are up. Public so that a
caller who would rather pay it once up front — a long corpus run, or a release
that wants every application accounted for at boot — can, and so that the lazy
start is testable without a network.

    iex> Tptp.Resolver.Http.started()
    :ok

# `url`

```elixir
@spec url(
  binary(),
  keyword()
) :: binary()
```

The SeeTPTP URL an include name maps to.

    iex> Tptp.Resolver.Http.url("Problems/PUZ/PUZ001+1.p")
    "https://tptp.org/cgi-bin/SeeTPTP?Category=Problems&Domain=PUZ&File=PUZ001%2B1.p"

    iex> Tptp.Resolver.Http.url("Axioms/SET007+0.ax")
    "https://tptp.org/cgi-bin/SeeTPTP?Category=Axioms&File=SET007%2B0.ax"

    iex> Tptp.Resolver.Http.url("SET007+0.ax")
    "https://tptp.org/cgi-bin/SeeTPTP?Category=Axioms&File=SET007%2B0.ax"

---

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