# normalize

Standardize Lean file formatting to prepare for other operations, especially `merge` operations. Use this tool to detect when a file is unusually structured, in which case other Axle operations may behave unexpectedly.

## Input Parameters

`content` · str · required · Lean source code  
The Lean source code to be processed by this tool.

`normalizations` · list[str] · List of normalizations to apply  
Options: remove_sections, expand_decl_names, expand_scoped_notations, remove_duplicates, split_open_in_commands, normalize_module_comments, normalize_doc_comments. Default: remove_sections, remove_duplicates, split_open_in_commands.

`failsafe` · bool · default: `True` · Return original if normalization fails  
If true, returns the original content unchanged if normalization introduces errors. Defaults to true.

`ignore_imports` · bool · default: `True` · Ignore import mismatches  
Controls import statement handling:

- `true` (default): Ignore the imports in `content` and substitute the environment's default header. This uses the pre-built cached environment, so it is fast. The substituted code is returned in the `content` field.  
- `false`: Process the imports in `content` exactly as written. This is significantly slower (the cached environment cannot be reused) and may produce inconsistent or incorrect results if a required dependency such as `Mathlib.Tactic` is missing. A warning is returned in these cases. See the troubleshooting page for more details.

`environment` · str · required · Lean environment or version  
The Lean environment to use for evaluation. Each environment includes a specific  
Lean version and pre-built dependencies (typically Mathlib).

Available environments: `lean-4.28.0`, `lean-4.27.0`, `lean-4.26.0`, etc.

`timeout_seconds` · float · default: `120` · Max execution time in seconds  
Maximum execution time in seconds. Requests exceeding this limit return a timeout error. Note that end-to-end request latency may exceed this timeout due to queue time and other overhead. Additionally, all non-admin requests are subject to an absolute maximum timeout of 900 seconds (15 minutes).

## Output Fields

`lean_messages` · dict · Messages from Lean compiler  
Messages from the Lean compiler with `errors`, `warnings`, and `infos` lists.  
Errors here indicate invalid Lean code (syntax errors, type errors, etc.); an empty `errors` list means the code compiles.

If the tool allows declaration selection and a `names`/`indices` selection is given, elaboration is skipped for the proofs of unselected declarations, so this field reflects only the selected declarations and is otherwise incomplete.

`tool_messages` · dict · Messages from normalize tool  
Messages from the normalize tool with `errors`, `warnings`, and `infos` lists.  
Errors here indicate tool-specific issues (not Lean compilation errors).

`content` · string · The normalized Lean code  
The standardized code. May be identical to input if `failsafe` triggered.

`timings` · dict · Execution timing breakdown  
Timing information in milliseconds for various stages of processing.

`normalize_stats` · dict · Count of each normalization applied  
Maps normalization names to counts (e.g., `{"remove_sections": 2}`).

## Available Normalizations

`remove_sections`  
Removes `section`, `namespace`, and `end` commands. Declaration names are fully qualified to preserve semantics. If a `noncomputable section` is removed, `noncomputable section` is re-inserted at the top of the file to preserve semantics.

**Before:**  
```
namespace MyNamespace
noncomputable section MySection

theorem foo : 1 = 1 := rfl

end MySection
end MyNamespace
```

**After:**  
```
noncomputable section
theorem MyNamespace.foo : 1 = 1 := rfl
```

`expand_decl_names`  
Fully qualifies declaration names by prepending all enclosing namespaces. Useful for making declarations unambiguous without relying on namespace context.

**Before:**  
```
open Option
example (α : Type) (x : α) :
    Option.getD (some x) x = x := by
  simp [getD]
```

**After:**  
```
open Option
example (α : Type) (x : α) :
    Option.getD (Option.some x) x = x := by
  simp [Option.getD]
```

`expand_scoped_notations`  
Expands scoped notations (those brought in by `open`) into their underlying applications. This runs Lean's delaborator with notations disabled, so the expanded form uses function application. Combined with `expand_decl_names`, constant names in the output are fully qualified.

Note: inside an expanded notation, all nested notations are stripped — including globals like +. This expander can be over-aggressive for notations whose body contains other, non-scoped notations.

Note: the delaborator isn't guaranteed to round-trip cleanly — coercions, universe annotations, and a few other constructs are known trouble spots and may produce output that doesn't re-elaborate. Uncommon in practice, but keep `failsafe` on if correctness matters.

**Before:**  
```
namespace MyNS
scoped infix:65 " ⊹ " => HAdd.hAdd
end MyNS

open MyNS

def x : Nat := (1 ⊹ 2) + 3
```

**After:**  
```
namespace MyNS
scoped infix:65 " ⊹ " => HAdd.hAdd
end MyNS

open MyNS

def x : Nat := ( HAdd.hAdd  1  2 ) + 3
```

`remove_duplicates`  
Removes duplicate commands, such as repeated `open` statements for the same module.

**Before:**  
```
open Nat
open Nat
open List
```

**After:**  
```
open Nat
open List
```

`split_open_in_commands`  
Splits `open [modules] in [decl]` syntax into separate `open` and declaration commands. This makes the structure more explicit and easier to process.

**Before:**  
```
open Nat in
theorem foo : succ 0 = 1 := rfl
```

**After:**  
```
open Nat
theorem foo : succ 0 = 1 := rfl
```

`normalize_module_comments`  
Converts module documentation comments (`/-! ... -/`) into regular block comments (`/- ... -/`). Module comments are typically used for file-level documentation.

`normalize_doc_comments`  
Converts documentation comments (`/-- ... -/`) into regular block comments (`/- ... -/`). Doc comments are typically attached to declarations to provide API documentation.

## Python API  
```
result = await axle.normalize(
    content=lean_code,
    environment="lean-4.28.0",
    normalizations=["remove_sections", "expand_decl_names"],  # Optional: specify which normalizations
    failsafe=True,  # Optional: return original if normalization fails
)
print(result.content)
print(result.normalize_stats)
```

## CLI  
**Usage:**`axle normalize CONTENT [OPTIONS]`  
```
# Normalize a file
axle normalize theorem.lean --environment lean-4.31.0
# Normalize and save to file
axle normalize theorem.lean -o normalized.lean --environment lean-4.31.0
# Apply only specific normalizations
axle normalize theorem.lean --normalizations remove_sections,expand_decl_names --environment lean-4.31.0
# Pipeline usage
cat theorem.lean | axle normalize - --environment lean-4.31.0 | axle merge - other.lean --environment lean-4.31.0
# Disable failsafe to always return normalized output
axle normalize theorem.lean --no-failsafe --environment lean-4.31.0
```

## HTTP API  
```
curl -s -X POST https://axle.axiommath.ai/api/v1/normalize \
    -d '{"content": "import Mathlib\nsection\ntheorem foo : 1 = 1 := rfl\nend", "environment": "lean-4.28.0"}' | jq
```

## Example Response  
```
{
  "lean_messages": {
    "errors": [],
    "warnings": [],
    "infos": []
  },
  "tool_messages": {
    "errors": [],
    "warnings": [],
    "infos": []
  },
  "content": "import Mathlib\n\ntheorem foo : 1 = 1 := rfl\n",
  "timings": {
    "total_ms": 92,
    "parse_ms": 87
  },
  "normalize_stats": {
    "remove_sections": 2
  }
}
```