split-file

/split-file - Split Large Lean Files

Split a large Lean file (>1500 lines) into smaller, focused modules.

Usage

/split-file [file_path]

Splitting Strategy

Step 1: Analyze the File

1. Get the file outline using lean_file_outline
2. List all declarations with their line numbers
3. Group declarations by naming prefix (e.g., cauchyPrincipalValue*, residue*)

Step 2: Identify Natural Groupings

Group declarations by the object they work on, identified by naming patterns:

Prefix Pattern	Suggested File
cauchyPrincipalValue*	CauchyPrincipalValue.lean
residue*, Residue*	Residue.lean
pv_*, PV*	PrincipalValue.lean
winding*, Winding*	WindingNumber.lean
integral_*	Integration.lean
Core definitions	Basic.lean or Defs.lean

Step 3: Determine Split Structure

Option A: Two-file split (for 1500-3000 lines)

Module/
├── Basic.lean      -- Core definitions + simple lemmas
└── Theorems.lean   -- Main results (imports Basic)

Option B: Multi-file split (for >3000 lines)

Module/
├── Defs.lean       -- Core definitions only
├── Basic.lean      -- API lemmas (imports Defs)
├── Topic1.lean     -- Grouped lemmas (imports Basic)
├── Topic2.lean     -- Grouped lemmas (imports Basic)
└── Main.lean       -- Main theorems (imports all above)

Step 4: Execute the Split

For each new file:

1. Create the file with proper header:

/-
Copyright (c) 2024 [Author]. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: [Author]
-/
import [necessary imports]

/-!
# [Module Title]

[Brief description]

## Main definitions/results

* `foo`: Description
-/

1. Move declarations preserving order (dependencies must come before dependents)

2. Update imports in all affected files

3. Verify each file compiles before proceeding to next

Step 5: Verify

1. Run lake build on each new file
2. Ensure no circular imports
3. Check that downstream files still compile