merge¶
Combine multiple Lean files into a single file.
Python API¶
result = await axle.merge(
documents=[code1, code2, code3],
environment="lean-4.26.0",
use_def_eq=True, # Optional
include_alts_as_comments=False, # Optional
timeout_seconds=120, # Optional
)
print(result.content)
CLI¶
Usage: axle merge FILE1 FILE2 ... [OPTIONS]
# Merge multiple files to stdout
axle merge theorem1.lean theorem2.lean theorem3.lean --environment lean-4.26.0
# Merge all .lean files in directory
axle merge *.lean -o combined.lean --environment lean-4.26.0
# Merge and check
axle merge *.lean --environment lean-4.26.0 | axle check - --environment lean-4.26.0
HTTP API¶
curl -s -X POST http://10.1.10.100:8989/v1/axle/merge \
-d '{"documents": ["import Mathlib\ntheorem foo : 1 = 1 := rfl", "import Mathlib\ntheorem bar : 2 = 2 := rfl"], "environment": "lean-4.26.0"}' | jq
Input Parameters¶
| Name | Type | Required | Description |
|---|---|---|---|
documents |
list[str] |
Yes | A list of Lean code strings to merge |
environment |
str |
Yes | Environment to use (e.g., "lean-4.26.0", "lean-4.25.1") |
use_def_eq |
bool |
No | If true (default), uses definitional equality to de-duplicate declarations |
include_alts_as_comments |
bool |
No | When deduplicating, preserves all versions of a merged declaration as comments (default: false) |
ignore_imports |
bool |
No | If true, ignore import statement mismatches and use the environment's default imports. If false, raise an error on mismatch. Default: false |
timeout_seconds |
float |
No | Maximum execution time (default: 120) |
Output Fields¶
| Name | Type | Description |
|---|---|---|
lean_messages |
dict |
Messages from Lean compiler with errors, warnings, infos lists |
tool_messages |
dict |
Messages from merge tool with errors, warnings, infos lists |
content |
str |
The merged Lean code combined into a single file |
timings |
dict |
Timing info: total_ms, parse_ms (cumulative for all inputs) |
Example Response¶
{
"lean_messages": {
"errors": [],
"warnings": [],
"infos": []
},
"tool_messages": {
"errors": [],
"warnings": [],
"infos": []
},
"content": "import Mathlib\n\ntheorem foo : 1 = 1 := rfl\n\ntheorem bar : 2 = 2 := rfl",
"timings": {
"total_ms": 105,
"parse_ms": 95
}
}
Demo¶
This merge function is intended to be a consolidation of multiple Lean files that performs best-effort deduplication and conflict resolution. As a demonstration, we'll merge the following two files, with descriptions of features along the way.
File 1¶
import Mathlib
open Lean
theorem D : (1 = 1 ∧ 2 = 2) ∧ True := rfl
theorem A : 2 = 2 := rfl
variable (x : Nat)
theorem E : x = 5 := trivial
theorem B : 1 = 1 := rfl
theorem C2 : 1 = 1 ∧ 2 = 2 := ⟨B, A⟩
set_option maxHeartbeats 0
File 2¶
import Mathlib
open Lean.Elab
set_option maxHeartbeats 200000
theorem A : 4 = 4 := rfl
theorem B : 1 = 1 := rfl
theorem C1 : 1 = 1 ∧ 2 = 2 := ⟨B, A⟩
theorem D : (1 = 1 ∧ 2 = 2) ∧ True := ⟨C1, trivial⟩
variable (x : Nat)
theorem E : x = 5 := sorry
Non-declaration commands are extracted first¶
Any non-declaration commands (variables, open scopes, options, notations, etc.) will be extracted first from all files. These commands will be placed under a comment label like ----------------------
Note that this may break files, since many of these commands have global side effects that change how a proof is run, so it is a good idea to normalize your code first, whether manually or by calling normalize.
This gives us:
----------------------
open Lean
variable (x : Nat)
set_option maxHeartbeats 0
----------------------
open Lean.Elab
set_option maxHeartbeats 200000
variable (x : Nat)
Pay attention to how we have conflicting commands here: at first, we set maxHeartbeats to 0, and then immediately reset it to 200000. Until we figure out a better way to handle this scenario, it is good to keep in mind.
Declarations are merged respecting dependencies¶
All remaining commands will be declarations, and will be merged in topological order.
Conflict resolution via renaming¶
Notice that both files have a theorem A, which assert different things. The merge function will automatically rename one of them to a globally unique identifier. Note that our renaming function is fairly robust as seen in the rename endpoint.
Deduplication of identical theorems¶
Theorem B exists in both files here, so we merge them into a single theorem.
Note that we also merge non-theorems (e.g., definitions and structures), but these must have the same value in addition to having the same type, because they are implementation-specific.
Deduplication merges theorems with different names¶
Theorem C exists in both files, but with different names (C1 vs. C2). Our merge function will automatically detect this equivalence and generate a unique name to use in the merged file.
Preference for error-free and sorry-free declarations¶
Theorem D exists in both files, but in the first file, the proof rfl completely fails, so we'll prefer the implementation in the second file.
Notice something interesting here: in the first file, D was declared before A, B, C existed, so there couldn't possibly be a proof of D that uses A, B, C. However, our dependency tracking figures out that since we should use the implementation in the second file, we need the dependencies from that file, where A, B, C are defined.
Unsuccessful attempts are preserved as comments¶
If no successful proofs exist, we select one arbitrarily, but keep the others as reference. We retain the remaining unsuccessful proofs as comments following the chosen proof, with the signposting unsuccessful attempt.
Final File¶
import Mathlib
----------------------
open Lean
variable (x : Nat)
set_option maxHeartbeats 0
----------------------
open Lean.Elab
set_option maxHeartbeats 200000
variable (x : Nat)
theorem A : 2 = 2 := rfl
theorem B : 1 = 1 := rfl
theorem C2_1 : 1 = 1 ∧ 2 = 2 := ⟨B, A⟩
theorem A_1 : 4 = 4 := rfl
theorem D : (1 = 1 ∧ 2 = 2) ∧ True := ⟨C2_1, trivial⟩
theorem E : x = 5 := trivial
/-
-- unsuccessful attempt
theorem E : x = 5 := sorry
-/