Modal¶
open-atp can run commands in Modal Sandboxes instead of
local Docker containers. Each run gets its own cloud Sandbox, which avoids duplicate
Lean environments and lets many runs proceed in parallel
without consuming local resources.
Install Modal¶
Modal ships as a dependency of open-atp. Authenticate the modal CLI against your
Modal workspace (this writes a token to ~/.modal.toml):
modal setup
Verify the credentials are working with:
modal app list
Build the Modal image¶
Unlike Docker, Modal Sandboxes have an isolated filesystem and ignore a container
USER, so the sandbox image is built and published programmatically (rather than
from images/Dockerfile). It installs the Lean toolchain and agent CLIs globally as
root and bakes the same warm Mathlib olean cache. Build and publish it with:
open-atp build-modal-image
This publishes a named Modal image (open-atp by default) that the backend looks
up at run time. The name must match ModalConfig.image (sans :tag); pass --name
to publish under a different name and --force to rebuild even when Modal has cached
layers. As with Docker, the first build pre-builds Mathlib and is expected to take a
while.
Using the Modal backend¶
A ModalBackend is constructed from a
ModalConfig and is a drop-in
ComputeBackend — substitute it for the
DockerBackend anywhere a verification or generation backend is expected:
from open_atp.backends.modal import ModalBackend, ModalConfig
from open_atp.images import DEFAULT_IMAGE
backend = ModalBackend(ModalConfig(image=DEFAULT_IMAGE, cpu=4.0, memory_mib=4096))
cpu is a guaranteed floor of cores (the Sandbox may burst higher) and memory_mib
is in MiB. See the backends reference for the full set of options.
For the common case of verifying against the published image, the
modal_verifier() helper wires up a
Verifier for you — the Modal counterpart of
docker_verifier():
from open_atp.verify import modal_verifier
verifier = modal_verifier()
Note
Running on Modal incurs cloud compute charges billed by your Modal workspace. See Modal’s pricing for details.