Skip to content

python-api.md

Latest commit

 

History

History
90 lines (70 loc) · 3.89 KB

python-api.md

File metadata and controls

90 lines (70 loc) · 3.89 KB
Raw

Python API Reference

Axle Client

The main client for interacting with the AXLE API.

Basic Usage

import asyncio
from axle import AxleClient

async def main():
    async with AxleClient() as client:
        result = await client.check(content="import Mathlib\ndef x := 1", environment="lean-4.28.0")
        # okay means it compiled; failed_declarations catches sorry, disallowed axioms, etc. that leave okay true.
        print(f"Compiles: {result.okay}")
        print(f"Valid proof: {result.okay and not result.failed_declarations}")

asyncio.run(main())

Constructor

AxleClient(
    api_key: str | None = None,          # default: AXLE_API_KEY env var
    url: str | None = None,              # default: AXLE_API_URL env var
    max_concurrency: int | None = None,  # default: AXLE_MAX_CONCURRENCY env var
    base_timeout_seconds: float | None = None,  # default: AXLE_TIMEOUT_SECONDS env var
)

All arguments fall back to their corresponding environment variables if not provided. See Configuration for details.

Error Handling

All errors raise exceptions. Use try/except to handle them:

from axle.exceptions import (
    AxleIsUnavailable,
    AxleRuntimeError,
    AxleInternalError,
    AxleInvalidArgument,
    AxleRateLimitedError,
    AxleForbiddenError,
    AxleNotFoundError,
    AxleConflictError,
    AxleBrowserLoginRequiredError,
)

try:
    result = await axle.check(content=code, environment="lean-4.28.0")
except AxleIsUnavailable as e:
    print(f"API unavailable at {e.url}: {e.details}")
except AxleInvalidArgument as e:
    print(f"Invalid request: {e}")
except AxleInternalError as e:
    print(f"Server error: {e}")
except AxleRuntimeError as e:
    print(f"Operation failed: {e}")
Exception HTTP Status Cause Action
AxleIsUnavailable 503 Cannot reach API server (connection refused, DNS failure, service unavailable, service upgrade) Automatically retried; check network if persistent
AxleRateLimitedError 429 Too many requests Automatically retried with backoff
AxleInvalidArgument 400 Malformed request (missing parameters, invalid arguments) Fix the request
AxleForbiddenError 403 Access denied Check credentials/permissions
AxleNotFoundError 404 Resource not found Check the endpoint or resource ID
AxleConflictError 409 Request conflicts with current state Resolve the conflict
AxleInternalError 500 Server bug Report it
AxleBrowserLoginRequiredError 302 Endpoint is gated behind interactive browser sign-in Access via browser, or use an endpoint intended for CLI access
AxleRuntimeError — Operation reached the executors but failed Usually not worth retrying — AXLE already retried across executors internally
LeanResourceExceeded — Lean worker hit a resource cap (e.g. memory) for this input Reduce the problem's memory allocation
LeanTimeout — Lean worker exceeded its time budget for this input Simplify the input or raise the timeout

Automatic Retries

The client automatically retries transient errors with exponential backoff:

  • AxleIsUnavailable (503, connection errors)
  • AxleRateLimitedError (429)

Non-retryable errors like AxleInternalError (500) and client errors (4xx) are raised immediately.

Beyond the client's own retries, the AXLE gateway retries transient executor failures (worker crashes) across multiple executors before giving up — so an AxleRuntimeError usually means those internal retries are already exhausted and re-retrying rarely helps. LeanResourceExceeded and LeanTimeout are deterministic for a given input and are never retried: the same input yields the same outcome.

To catch all API errors at once, use the base class AxleApiError.