# Configuration

AXLE can be configured via environment variables or constructor arguments.

## Authentication

AXLE uses API key authentication for active request rate limiting. Requests without an API key are limited to 10 concurrent active requests.

To obtain an API key, visit [axle.axiommath.ai/app/console](https://axle.axiommath.ai/app/console). If you need higher rate limits, you can [request more capacity](https://forms.gle/CdLKu45tEsRXtFQ29).

### Setting Your API Key

The recommended way to configure your API key is via the `AXLE_API_KEY` environment variable:

```
export AXLE_API_KEY=your-api-key
```

You can also pass it directly when creating the client (see [Python Configuration](https://axle.axiommath.ai/v1/docs/configuration/#python-configuration) below).

## Environment Variables

| Variable                   | Default                        | Description                                               |
|----------------------------|--------------------------------|-----------------------------------------------------------|
| `AXLE_API_KEY`            | —                              | API key for authentication                                 |
| `AXLE_API_URL`            | `https://axle.axiommath.ai`   | API server URL                                           |
| `AXLE_TIMEOUT_SECONDS`     | `1_800`                       | Base timeout in seconds for retry window if service is temporarily unavailable |
| `AXLE_MAX_CONCURRENCY`     | `20`                          | Max concurrent requests                                   |

### Example

```
export AXLE_API_KEY=your-api-key
export AXLE_API_URL=https://axle.axiommath.ai
export AXLE_TIMEOUT_SECONDS=600
export AXLE_MAX_CONCURRENCY=50
```

## Python Configuration

### Constructor Arguments

```
from axle import AxleClient

# API key from environment variable (recommended)
client = AxleClient()

# Explicit API key
client = AxleClient(api_key="your-api-key")

# Custom URL, timeout, and concurrency
client = AxleClient(
    api_key="your-api-key",
    url=AxleClient.DEFAULT_URL,
    base_timeout_seconds=600,
    max_concurrency=50,
)
```

All constructor arguments fall back to environment variables if not provided.

## CLI Configuration

The CLI reads the `AXLE_API_KEY` environment variable automatically. Set it before running CLI commands:

```
export AXLE_API_KEY=your-api-key
```

### Global Options

```
# Custom API URL
axle --url https://axle.axiommath.ai check file.lean --environment lean-4.28.0

# JSON output
axle --json check file.lean --environment lean-4.28.0

# Output to file
axle theorem2sorry input.lean --environment lean-4.28.0 -o output.lean
```

## Lean Environments

AXLE supports multiple Lean environments, each containing a specific Lean version and set of dependencies (e.g., Mathlib). Every API request requires an `environment` parameter specifying which environment to use. To get started, we recommend using the latest Lean + Mathlib version, which at the time of writing is packaged in `lean-4.28.0`.

### Discovering Available Environments

You can query the available environments using any access method:

#### Python

```
import asyncio
from axle import AxleClient

async def main():
    async with AxleClient() as client:
        environments = await client.environments()
        for env in environments:
            print(f"{env.name}: {env.description}")

asyncio.run(main())
```

#### CLI

```
axle environments
```

#### HTTP API

```
curl -s -H "Authorization: Bearer $AXLE_API_KEY" https://axle.axiommath.ai/v1/environments | jq
```

The `Authorization` header is required for all requests.

### Environment Response Format

Each environment includes the following fields:

| Field               | Type | Description                                          |
|---------------------|------|------------------------------------------------------|
| `name`              | `str`| Environment identifier to use in requests (e.g., "lean-4.28.0") |
| `lean_toolchain`    | `str`| Lean toolchain version (e.g., "leanprover/lean4:v4.26.0") |
| `repo_url`          | `str | null` | Git repository URL for custom environments            |
| `revision`          | `str | null` | Git revision/commit hash for custom environments      |
| `subdir`           | `str | null` | Subdirectory within the repository                     |
| `imports`           | `str`| Default imports available (e.g., "import Mathlib") |
| `description`       | `str`| Human-readable description                           |

### Example Environments

```
[\
  {\
    "name": "lean-4.21.0",\
    "lean_toolchain": "leanprover/lean4:v4.21.0",\
    "imports": "import Mathlib",\
    "description": "Lean 4.21.0 with Mathlib"\
  }]
```

See [Import Mismatches](https://axle.axiommath.ai/v1/docs/troubleshooting/#import-mismatches) for important notes on how AXLE handles import statements.