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.