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 <, 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. < 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.