benchmark

Run a set of provers across a set of named ProofTasks and tabulate the results. run_benchmark() runs every (task, prover) pair and lays the artifacts out under output_dir as output_dir/<task>/<prover>/{wd,logs,results.json}, returning a BenchmarkResult with a terminal-table view. A prover that raises is recorded as a failed ProofResult so one bad run never aborts the sweep.

Runner

open_atp.benchmark.run_benchmark(tasks: Mapping[str, ProofTask], provers: Mapping[str, AutomatedProver], output_dir: Path | str, *, only: Sequence[str] | None = None, max_workers: int | None = None, max_per_prover: int = 5, progress: bool = True) → BenchmarkResult

Run every prover over every task, writing artifacts under output_dir.

Each (task, prover) pair runs in its own output_dir/<task>/<prover>/ directory, which receives the prover’s wd/logs and a results.json dump of the ProofResult. A prover that raises is recorded as a failed result (its error captured) and the sweep continues.

Pairs run concurrently on a thread pool (prove is I/O-bound on the sandbox and the prover’s API). Two independent limits bound the concurrency: max_workers caps the total in-flight pairs, and max_per_prover caps how many of those may belong to any one prover – so a rate-limited prover (e.g. a hosted model) never has more than max_per_prover calls in flight even when other provers fill the pool. The returned runs keep task-major, prover-minor order regardless of completion order.

Parameters:

tasksMapping[str, ProofTask]

Tasks keyed by name; the name becomes the task’s output subdirectory.

proversMapping[str, AutomatedProver]

Provers keyed by name; the name becomes the per-task output subdirectory. A mapping (not a list) so the caller labels each entry – the same prover can appear under several keys (e.g. different models) and stay distinct on disk and in the table.

output_dirpathlib.Path or str

Output root for the sweep, laid out as output_dir/<task>/<prover>/.

onlySequence[str], optional

Restrict the sweep to these task names (a subset of tasks), in the given order. None (default) runs every task. An unknown name raises ValueError.

max_workersint, optional

Total prove calls in flight at once. None (default) lets the thread pool pick a default; 1 runs the sweep serially.

max_per_proverint, default 5

Most concurrent prove calls for any single prover. Bounded to stay under rate limits.

progressbool, default True

Show a tqdm progress bar over the (task, prover) pairs. Each completed pair is logged (task, prover, status, duration, cost) on the open_atp logger regardless.

Returns:

BenchmarkResult

Every (task, prover) cell (see to_dict()).

exception open_atp.benchmark.RunCeilingExceeded

The run exceeded the maximum allowed duration and is in an unhealthy state.

Distinct from a prover spending its own generation budget: the ceiling only fires once a run has blown past every timeout meant to bound it, so the run is wedged rather than merely out of time.

Building tasks from a directory

tasks_from_dir() builds the tasks mapping from a directory laid out like the public Lean benchmarks (PutnamBench, FATE) — a flat directory of standalone .lean files, optionally with subdirectories grouping several files into one task.

open_atp.benchmark.tasks_from_dir(directory: Path | str, *, skeleton: Path = PosixPath('/home/docs/checkouts/readthedocs.org/user_builds/open-atp/envs/latest/lib/python3.12/images/lean')) → dict[str, ProofTask]

Build a benchmark’s tasks mapping from a directory of Lean files.

Mirrors the layout the public Lean benchmarks ship (PutnamBench, FATE):

• Each .lean file directly under directory becomes one task named by its filename stem, staged into skeleton (a bare file carries no lake project).

• Each subdirectory becomes one task named by the subdirectory name. A subdirectory that is already a complete lake project (carries its own lean-toolchain and lakefile) is used as-is; otherwise its .lean files are staged into skeleton.

In both staged cases create_project() supplies the skeleton. Subdirectories with no .lean files (and entries whose name starts with .) are skipped. The result is ready to hand to run_benchmark().

Parameters:

directorypathlib.Path or str

The benchmark directory: .lean files and/or per-task subdirectories.

skeletonpathlib.Path, default SKELETON_DIR

Project skeleton staged around bare files (see create_project()). The default is the baked image’s pinned Mathlib skeleton, only present in a source checkout. Pass a checkout of a benchmark’s own toolchain to stage against a non-default Lean/Mathlib pin.

Returns:

dict[str, ProofTask]

Tasks keyed by file stem (loose files) or subdirectory name.

Downloading a dataset

download_dataset() fetches one of the public benchmarks (a DATASET member) straight to a task directory — a sparse clone of just the dataset’s .lean subdirectory — ready for tasks_from_dir().

open_atp.benchmark.download_dataset(dataset: DATASET, dest: Path | str, *, ref: str | None = None) → Path

Download a benchmark dataset’s task directory to dest/<dataset>.

Sparse-clones only the dataset’s task subdirectory (shallow + blobless), then lifts its .lean files to dest/<dataset> – a flat directory ready for tasks_from_dir(), with no surrounding git repo. An already-present download is reused as-is (the clone is skipped), so repeated calls are cheap. DATASET.EXAMPLES instead copies the package’s bundled example assets into dest/examples (no clone, ref ignored).

Parameters:

datasetDATASET

Which benchmark to fetch.

destpathlib.Path or str

Parent directory; the dataset lands at dest/<dataset>. Created if missing.

refstr, optional

Branch or tag to check out. None uses the repo’s default branch. Ignored for DATASET.EXAMPLES.

Returns:

pathlib.Path

The dataset’s task directory (dest/<dataset>).

class open_atp.benchmark.DATASET(*values)

The benchmark datasets accepted by download_dataset().

Each member’s value is the directory name the dataset lands in. The FATE datasets and the bundled examples are on the default v4.28.0; PutnamBench pins an older Lean (v4.27.0), so stage it with a matching skeleton (see tasks_from_dir()). EXAMPLES is the package’s bundled EXAMPLE set, copied from the wheel rather than cloned.

Results

class open_atp.benchmark.BenchmarkResult(output_dir: Path, runs: list[BenchmarkRun])

The collected cells of a benchmark sweep.

Parameters:

output_dirpathlib.Path

The benchmark’s output root, laid out as output_dir/<task>/<prover>/.

runslist[BenchmarkRun]

One BenchmarkRun per (task, prover) pair, in run order.

to_dict() → dict[str, object]

JSON-ready view: the output root plus each cell’s task, prover, result.

class open_atp.benchmark.BenchmarkRun(task: str, prover: str, result: ProofResult)

One (task, prover) cell of a benchmark sweep.

Parameters:

taskstr

The task’s key in the benchmark’s tasks mapping.

proverstr

The prover’s key in the benchmark’s provers mapping. Caller-chosen, so it may differ from the prover’s own prover (e.g. two entries running the same prover under different labels).

resultProofResult

The run’s result. On an exception its error is set and verification is None.