backends

A ComputeBackend runs a command over a working directory inside a Lean+Mathlib sandbox. It is the single load-bearing primitive of the platform, used both to run a coding agent and to run lake env lean ... for verification. A ComputeSession keeps that sandbox alive across several commands – generation then verification against the same hot filesystem – without paying a second spin-up.

Base

class open_atp.backends.base.ComputeBackend(*, image: Image | Mapping[str, object] = Image(name='open-atp:latest', lean_toolchain='leanprover/lean4:v4.28.0', mathlib_rev='v4.28.0'), env: Mapping[str, str] | None = None)[source]

Runs commands over a workdir in a sandbox carrying Lean + Mathlib.

Parameters:
imageImage, default DEFAULT_IMAGE

The sandbox image carrying Lean + Mathlib – its tag plus the toolchain and Mathlib revision the verifier checks projects against. A mapping is coerced to an Image (so a parsed config’s nested image: block works).

envMapping[str, str], optional

Environment variables baked into every command run in the sandbox. Defaults to no extra variables.

abstract property name: str

Short identifier for the backend, such as docker or modal.

Used to label log records and benchmark rows.

abstract property wallclock_overhead_s: int

Wall-clock time budget required beyond a command’s timeout, in seconds.

The timeout_s passed to run()/session() is the command’s wall-clock budget. The backend may need extra time for spin-up, teardown, file transfer, etc. The time allotted for this overhead is captured here, so a caller can bound the total wall-clock for a run.

abstractmethod session(workdir: Path, *, timeout_s: int, env: Mapping[str, str] | None = None, mounts: Sequence[tuple[str, str]] | None = None) → ComputeSession[source]

Open a persistent sandbox over workdir for multiple exec() calls.

Unlike run() (one command, then teardown), the returned ComputeSession stays alive until ComputeSession.close(), so the same hot sandbox can run generation and verification back to back.

env/mounts here pin the long-lived sandbox at creation (Docker bind mounts can only be set at docker run); per-command credentials go to ComputeSession.exec()’s own env.

Parameters:
workdirpathlib.Path

Host directory mounted/synced into the sandbox for the session’s life.

timeout_sint

Wall-clock cap for the sandbox, in seconds.

envMapping[str, str], optional

Environment variables pinned on the sandbox at creation, merged over the backend’s env.

mountsSequence[tuple[str, str]], optional

Extra (host_path, container_path) mounts pinned at creation.

Returns:
ComputeSession

A live session over the workdir; close it via ComputeSession.close() (use as a context manager).

run(workdir: Path, command: str, *, timeout_s: int, env: Mapping[str, str] | None = None, mounts: Sequence[tuple[str, str]] | None = None) → CommandResult[source]

Run a single command in a fresh sandbox over workdir, then tear down.

A one-shot session(): the workdir (and any mounts) is synced in, the command runs to completion, and the sandbox is torn down – pulling file mutations (completed proofs) back to the host on the way out.

Parameters:
workdirpathlib.Path

Host directory mounted/synced into the sandbox; mutations sync back out.

commandstr

The shell command to run inside the sandbox.

timeout_sint

Wall-clock cap for the command, in seconds.

envMapping[str, str], optional

Per-call environment variables, merged over the backend’s env.

mountsSequence[tuple[str, str]], optional

Extra (host_path, container_path) bind mounts beyond the workdir.

Returns:
CommandResult

Exit code, captured stdout/stderr, and wall-clock duration.

test() → bool[source]

Smoke-test the backend by verifying a trivial proof end to end.

Returns:
bool

Whether the trivial proof verified in this backend.

class open_atp.backends.base.CommandHandle[source]

A live command running in a session’s sandbox. Backends fill the hooks.

Streaming matters for agents (we want incremental stdout for cost/progress parsing) but is equally usable for a blocking lake invocation via wait(). The handle owns no teardown: the sandbox is the session’s, torn down by ComputeSession.close().

stream() → Iterator[str][source]

Yield stdout lines as they arrive.

Yields:
str

Each line of the command’s standard output, newline-stripped, as produced.

wait() → CommandResult[source]

Drain to completion and return the final result.

Returns:
CommandResult

Exit code, captured stdout/stderr, and wall-clock duration.

class open_atp.backends.base.CommandResult(exit_code: int, stdout: str, stderr: str, duration_s: float)[source]

Outcome of a finished command run inside a backend.

Parameters:
exit_codeint

The command’s process exit code (0 on success).

stdoutstr

The full captured standard output.

stderrstr

The full captured standard error.

duration_sfloat

Wall-clock time the command took, in seconds.

class open_atp.backends.base.ComputeSession[source]

A persistent sandbox over a workdir, exec’d many times, torn down once.

The one-shot ComputeBackend.run() creates a sandbox, runs a single command, and tears it down. A session keeps the sandbox alive so several commands can run against the same hot filesystem – the agent’s generation then the verifier’s compile – without paying a second spin-up.

Lifecycle invariant: teardown lives in close() (not in the handle’s wait), so a session MUST be used as a context manager and close() MUST be idempotent – otherwise an error between exec and close leaks the sandbox.

Examples

Open a session over a workdir and run several commands against the same hot sandbox – here generation followed by the compile, with one spin-up (needs a live backend, so this is illustrative rather than a doctest):

from open_atp.backends.docker import DockerBackend
from open_atp.images import DEFAULT_IMAGE

backend = DockerBackend(image=DEFAULT_IMAGE)
with backend.session(workdir, timeout_s=1800) as session:
    result = session.exec("lake env lean Demo.lean", timeout_s=300).wait()
    session.sync_out()   # pull the agent's edits back to the host
# the sandbox is torn down on exit, even if exec raised
exec(command: str, *, timeout_s: int, env: Mapping[str, str] | None = None) → CommandHandle[source]

Run command in the live sandbox; the handle does NOT tear it down.

Parameters:
commandstr

The shell command to run in the live sandbox.

timeout_sint

Wall-clock cap for the command, in seconds. When the command exceeds this budget it is killed, surfaced as CommandTimeout from wait().

envMapping[str, str], optional

Per-command environment variables, merged over the backend’s env.

Returns:
CommandHandle

A live handle to stream or wait() on. Its teardown hook does NOT close the session.

sync_out() → None[source]

Pull the sandbox workdir back to the host (no-op when bind-mounted).

sync_in() → None[source]

Push the host workdir into the sandbox (no-op when bind-mounted).

close() → None[source]

Tear the sandbox down (pull artifacts first where needed). Idempotent.

Docker

class open_atp.backends.docker.DockerBackend(*, image: Image | Mapping[str, object] = Image(name='open-atp:latest', lean_toolchain='leanprover/lean4:v4.28.0', mathlib_rev='v4.28.0'), env: Mapping[str, str] | None = None, volumes: tuple[tuple[str, str], ...] = ())[source]

Bases: ComputeBackend

Run sandboxes as local docker containers over a bind-mounted workdir.

The workdir is bind-mounted (not copied), so a command’s file edits land directly on the host. Construction is offline – it just records its knobs; the daemon is only contacted when a command runs.

Parameters:
imageImage, default DEFAULT_IMAGE

The sandbox image carrying Lean + Mathlib – its tag plus the toolchain and Mathlib revision the verifier checks projects against. A mapping is coerced to an Image (so a parsed config’s nested image: block works).

envMapping[str, str], optional

Environment variables baked into every command run in the sandbox. Defaults to no extra variables.

volumestuple[tuple[str, str], …], default ()

Extra -v host:container mounts (e.g. agent credential dirs).

Examples

Constructing the backend records its config without contacting the daemon:

>>> from open_atp.backends.docker import DockerBackend
>>> from open_atp.images import DEFAULT_IMAGE
>>> backend = DockerBackend(image=DEFAULT_IMAGE)
>>> backend.name
'docker'
property name: str

Short identifier for the backend: "docker".

property wallclock_overhead_s: int

Docker container start/teardown have near-zero overhead; use small buffer.

session(workdir: Path, *, timeout_s: int, env: Mapping[str, str] | None = None, mounts: Sequence[tuple[str, str]] | None = None) → ComputeSession[source]

Start a detached keep-alive container for repeated docker exec commands.

All mounts are wired at docker run time (Docker can’t add them per-exec); the container lives until DockerSession.close().

Parameters:
workdirpathlib.Path

Host directory bind-mounted at WORKDIR_MOUNT for the session’s life.

timeout_sint

Unused by Docker (the container has no built-in cap).

envMapping[str, str], optional

Environment variables pinned on the container at creation, merged over the backend’s env.

mountsSequence[tuple[str, str]], optional

Extra (host_path, container_path) bind mounts wired at creation (Docker can’t add them per-exec).

Returns:
ComputeSession

A live DockerSession over the workdir.

class open_atp.backends.docker.DockerSession(backend: DockerBackend, container: str)[source]

Bases: ComputeSession

A live docker run -d container; exec many commands, docker kill once.

The workdir is bind-mounted, so sync_out()/sync_in() are no-ops – edits already live on the host.

Parameters:
backendDockerBackend

The backend that provisioned the container.

containerstr

Name of the running container commands are docker exec’d into.

exec(command: str, *, timeout_s: int, env: Mapping[str, str] | None = None) → CommandHandle[source]

docker exec command into the container; close() owns teardown.

The command is wrapped in coreutils timeout so it is killed (only the exec, not the container) once timeout_s elapses, leaving the session up for the next command.

sync_out() → None[source]

No-op: the bind mount means edits are already on the host.

sync_in() → None[source]

No-op: the bind mount means host edits are already visible in-container.

close() → None[source]

docker kill the keep-alive container. Idempotent.