CLI Reference¶
The open-atp command-line interface is a thin shell over the Python API.
usage: open-atp [-h]
{prove,benchmark,download,auth-status,build-docker-image,build-modal-image}
...
Positional Arguments¶
- command
Possible choices:
prove,benchmark,download,auth-status,build-docker-image,build-modal-image
Sub-commands¶
prove¶
Run a standard prover on a lake project or Lean file.
open-atp prove [-h] [-c {docker,modal}] [--json]
[--log-level {debug,error,info,warning}] [-v] [-q]
path output
{claude,codex,deepseek,grok,spark,leanstral,axproverbase,kimi,numina,aristotle}
Positional Arguments¶
- path
A lake project directory or a single .lean file.
- output
Where to write the run’s logs and agent working directory.
- prover
Possible choices:
claude,codex,deepseek,grok,spark,leanstral,axproverbase,kimi,numina,aristotleName of standard prover to run.
Named Arguments¶
- -c, --compute
Possible choices:
docker,modalCompute backend to run generation and verification on.
Default:
'docker'- --json
Emit the result as JSON.
Default:
False- --log-level
Possible choices:
debug,error,info,warningConsole log verbosity (default: info).
Default:
'info'- -v, --verbose, -d, --debug
Shortcut for –log-level debug.
Default:
False- -q, --quiet
Shortcut for –log-level warning.
Default:
False
benchmark¶
Run multiple provers over a dataset of proof tasks.
open-atp benchmark [-h] [--config CONFIG] [-p PROVERS] [-t TASKS]
[-c {docker,modal}] [-w WORKERS] [--timeout TIMEOUT]
[--json] [--log-level {debug,error,info,warning}] [-v] [-q]
dataset output
Positional Arguments¶
- dataset
Directory of tasks to benchmark.
- output
Where to write each run’s logs and agent working directory.
Named Arguments¶
- --config
Path to YAML configuration for provers, tasks, compute, and workers; CLI flags override config values.
- -p, --provers
Comma-separated prover names (standard provers, or names from
--config); run every config prover, else all standard provers, by default.- -t, --tasks
Comma-separated task names to run; every task run by default.
- -c, --compute
Possible choices:
docker,modalCompute backend to run the sweep on (default: docker).
- -w, --workers
Number of workers; each worker runs a single prover on a task.
- --timeout
Per-task wall-clock timeout in minutes; defaults to the prover’s own.
- --json
Emit the result as JSON.
Default:
False- --log-level
Possible choices:
debug,error,info,warningConsole log verbosity (default: info).
Default:
'info'- -v, --verbose, -d, --debug
Shortcut for –log-level debug.
Default:
False- -q, --quiet
Shortcut for –log-level warning.
Default:
False
download¶
Download a benchmark dataset’s task directory.
open-atp download [-h] {examples,putnam,fate-h,fate-m,fate-x} output
Positional Arguments¶
- dataset
Possible choices:
examples,putnam,fate-h,fate-m,fate-xWhich dataset to download.
- output
Parent directory; the dataset lands at <output>/<dataset>.
auth-status¶
Show each standard prover’s credential and how long it stays valid.
open-atp auth-status [-h] [--json]
[{claude,codex,deepseek,grok,spark,leanstral,axproverbase,kimi,numina,aristotle}]
Positional Arguments¶
- prover
Possible choices:
claude,codex,deepseek,grok,spark,leanstral,axproverbase,kimi,numina,aristotleReport only this prover; every standard prover by default.
Named Arguments¶
- --json
Emit the statuses as JSON.
Default:
False
build-docker-image¶
Build the sandbox Docker image from images/Dockerfile.
open-atp build-docker-image [-h] [-t TAG] [-C]
Named Arguments¶
- -t, --tag
Image tag.
Default:
'open-atp:latest'- -C, --no-cache
Pass –no-cache to docker build.
Default:
False
build-modal-image¶
Build the sandbox image on Modal (from images/Dockerfile) and publish.
open-atp build-modal-image [-h] [-n NAME] [-a APP] [-f]
Named Arguments¶
- -n, --name
Name to publish the Modal image under. ModalBackend’s image (sans :tag) must match this.
Default:
'open-atp'- -a, --app
Modal app to associate the image build with.
Default:
'open-atp'- -f, --force
Force a rebuild even if Modal has cached layers.
Default:
False