Tptp.Resolver.Fs (Tptp v0.1.0)

Copy Markdown View Source

Resolves an include against the local filesystem.

Search order

  1. the directory of the including file, when there is one;
  2. :root, or $TPTP_ROOT if the option is absent;
  3. $TPTP, the older variable the TPTP tools have always used;
  4. :cwd, or the current working directory.

$TPTP_ROOT is the documented environment variable and :root is the local override, so that a caller directing resolution at a vendored copy, a fixture directory or a second library need not set an environment variable for the whole VM.

Tptp.Unit.from_file("PUZ001+1.p", resolver: Tptp.Resolver.Fs)
Tptp.Unit.from_file("PUZ001+1.p", resolver: {Tptp.Resolver.Fs, root: "/opt/TPTP"})

:root takes a list too, tried in order, for a caller layering a local override over a shared library:

{Tptp.Resolver.Fs, root: ["priv/my_axioms", "/opt/TPTP"]}

:root does not suppress $TPTP or the working directory; it is inserted ahead of them. To search only the named directories, pass cwd: false and leave the environment variables unset, or use Tptp.Resolver.Map.

$TPTP is honoured after :root because a machine with the TPTP distribution installed usually already has it set, and failing to find Axioms/SET007+0.ax on such a machine would be a silly way to lose.

Confinement

An include name originates in a file that may not be trusted, so it must be a relative path that does not ascend; see Tptp.Resolver.safe?/1. The name is checked rather than the joined result, which makes the condition independent of the candidate directory: no absolute paths and no .., in any position.

Canonicalisation

The returned path is expanded, so two routes to one file — Axioms/a.ax from the root and a.ax from the Axioms directory — memoise to the same entry and a diamond in the include graph is read once.

Summary

Functions

roots(from, options \\ [])

The directories this resolver would look in, in order.

Functions

roots(from, options \\ [])

@spec roots(
  Path.t() | nil,
  keyword()
) :: [Path.t()]

The directories this resolver would look in, in order.

Exposed because "it could not find the file" is a much less useful thing to be told than "it looked here, here and here".