# `mix tptp.corpus`
[🔗](https://github.com/jcschuster/tptp/blob/v0.1.3/lib/mix/tasks/tptp.corpus.ex#L1)

Reads every problem and axiom file of a local TPTP library and writes a report.

    mix tptp.corpus
    mix tptp.corpus --every 5
    mix tptp.corpus --check

This is a measurement rather than a test. A parser for a standardised language is
characterised by what it reads, and the report is committed so that a change
reducing coverage appears as a diff.

## Scope

Each file is read with `Tptp.from_string/2` alone. No `include` is resolved, no
lint rule is applied and no unit is constructed. Include resolution would read
further files and count one axiom set once per problem including it, and lint
findings do not bear on whether the input was parsed. The question is whether a
file parses, and at what cost.

A file counts as parsed when the result carries no error-severity diagnostic.
Warnings do not count against it: an empty quoted atom is TPTP this library reads
and reports.

## Time budget

Each file is allowed `--timeout` milliseconds of wall clock; one exceeding it is
terminated and recorded as a timeout rather than allowed to block the sweep. The
budget is wall time under `--concurrency` workers and is therefore a property of
the machine as much as of the file. The report records both.

## Memory budget

A file's size does not predict the cost of parsing it. Across the library the
source ranges from 2.5 to 111 bytes per tree node, a 44-fold spread, since
`p(a,b)` and a paragraph of prose occupy comparable numbers of bytes and
different numbers of nodes. Peak heap tracks nodes, at a more uniform 400–950
bytes each. Budgeting by file size therefore bounds the wrong quantity:
`SWV535-1.010.p` is 8.1 MB and peaks at 3.2 GB, while `SWW778_1.p` is twice its
size and peaks at a ninth of that.

Since the cost is not known in advance, it is bounded during the parse. Each file
is parsed in its own process under a `max_heap_size` flag, so the ceiling is
enforced by the VM. The flag counts shared binaries, without which it would
exclude the source itself: a single reference-counted binary into which every
leaf's `text` points, and the larger part of what a parse retains. `--heap` is the
total, divided equally among the workers of a tier, so peak heap across the sweep
is that total by construction.

Size determines concurrency, since it predicts wall time adequately: paths are
grouped into tiers at 1 MB and 4 MB, and each tier runs at its own worker count,
the largest files at the fewest workers. This is scheduling rather than a bound.

A file whose parse would exceed its worker's share is terminated and retried alone
against the whole of `--heap`, so tiering costs no coverage. A file exceeding the
budget when run alone is reported as `:heap` in the failure table.

## Options

  * `--every N` — sweep one file in N. The full sweep is the default; thinning is
    for a local check and its counts are not comparable.
  * `--timeout MS` — per-file budget, default 60000.
  * `--max-bytes N` — skip files larger than this, default 20 MB. In a complete
    TPTP this excludes seventy files, five axiom sets and sixty-five problems,
    which the streaming benchmark reads instead.
  * `--concurrency N` — workers in the smallest tier, default one per scheduler.
    Larger tiers scale down from it.
  * `--heap BYTES` — peak heap across all workers, default 6 GB. Lowering it on a
    smaller machine makes the sweep slower rather than incorrect.
  * `--out PATH` — output path, default `reports/CORPUS.md`.
  * `--check` — write nothing and fail if the committed report's results differ
    from this run. Timings are excluded from the comparison, so only a change in
    what parses can fail it.

# `files`

```elixir
@spec files(keyword()) :: [Path.t()]
```

Problem and axiom files under `root/0`, thinned and size-capped.

`:every` takes one file in n and `:max_bytes` skips the enormous axiom sets. The
sweep and the corpus tests both come through here so that the report and the
tests are describing the same set of files.

# `known_failures`

```elixir
@spec known_failures() :: %{required(binary()) =&gt; binary()}
```

Returns the library files this parser rejects, with the reason for each.

Keyed by base name. An entry is added only once the failure has been resolved to
a property of the sources. Every entry is a discrepancy between the vendored BNF
release and the library distributed alongside it, which a parser generated from
that BNF is expected to report.

The report renders each reason beside the failure it explains. The corpus tests
exclude these files and then assert that each still fails, so an entry that has
become unnecessary is reported rather than retained.

# `root`

```elixir
@spec root() :: Path.t() | nil
```

Returns the library root: `$TPTP_ROOT`, `$TPTP` or `/opt/TPTP`, whichever names a
directory.

Returns `nil` where none does, which allows the corpus tests to be skipped rather
than fail on a machine without a copy of the library.

# `stream`

```elixir
@spec stream([Path.t()], (Path.t() -&gt; term()), keyword()) :: [{Path.t(), term()}]
```

Run `fun` over `paths`, tier by tier, under a heap ceiling the VM enforces.

Each file is parsed in its own monitored process carrying a `max_heap_size` flag,
so a parse that would blow the budget is killed rather than the sweep. A killed
file is retried alone against the whole `:heap` before being reported as
`{:exit, :heap}`, so the tiering costs coverage only for a file that cannot be
read at all.

Returns `{path, {:ok, value}}` or `{path, {:exit, reason}}` in the order given.

# `tiers`

```elixir
@spec tiers(
  [Path.t()],
  keyword()
) :: [{pos_integer(), pos_integer(), [Path.t()]}]
```

Group paths into size tiers, each with the workers and heap share it runs under.

Sizes are grouped at `[1048576, 4194304]` bytes, ascending, empty tiers
dropped. The smallest tier gets `:concurrency` workers and each larger one half
of the tier below, down to one, because a file eight times the size is worth
proportionally fewer simultaneous parses. Every tier divides the same `:heap`
between its workers, so peak heap is the same number whichever tier is running.

Returns `{workers, heap_per_worker, paths}` per tier.

---

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