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.26.0")
        print(f"Valid: {result.okay}")

asyncio.run(main())

Constructor

AxleClient(
    api_key: str | None = None,          # API key (default: AXLE_API_KEY env var)
    url: str | None = None,              # API URL (default: AXLE_API_URL env or production)
    max_concurrency: int | None = None,  # Max concurrent requests
    base_timeout_seconds: float | None = None,  # Base timeout
)

If api_key is not provided, the client reads from the AXLE_API_KEY environment variable. 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,
)

try:
    result = await axle.check(content=code, environment="lean-4.26.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
AxleRuntimeError	—	Operation couldn't complete (timeout, resource limits)	Retry or adjust parameters

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.

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

Checking Results

For transformation endpoints (rename, merge, etc.), check lean_messages.errors since output should compile:

result = await axle.rename(content=code, declarations={"old": "new"}, environment="lean-4.26.0")

if result.lean_messages.errors:
    print("Output has compilation errors:")
    for msg in result.lean_messages.errors:
        print(f"  {msg}")
else:
    print(result.content)

For evaluation endpoints (verify_proof, check, comparator), lean_messages.errors being non-empty is normal - it's diagnostic output for invalid code. Check result.okay for pass/fail.