Minimizing Lean Errors

Workflow

1. •Set up the guard (#guard_msgs or #guard_panic)
2. •Run lake exe minimize
3. •Review and polish the output

Repository Setup

For Mathlib-related bugs:

cd /tmp
git clone https://github.com/kim-em/mathlib-minimizer.git
cd mathlib-minimizer
lake exe cache get

For pure Lean 4 bugs:

cd /tmp
git clone https://github.com/kim-em/lean-minimizer.git
cd lean-minimizer

Step 1: Create the Test File

For Regular Errors

Use #guard_msgs to capture the exact error:

import Mathlib.SomeModule

/--
error: the exact error message
goes here verbatim
-/
#guard_msgs in
example : ... := by some_tactic

For Panics

import Mathlib.SomeModule

#guard_msgs in
#guard_panic in
some_command_that_panics

Step 2: Verify the Guard Works

lake env lean YourFile.lean

No output = success (guard passed). Error output = guard failed, and you need to redesign the test case.

Step 3: Run the Minimizer

lake exe minimize YourFile.lean

Output is written to YourFile.out.lean.

Useful Options

• •--resume: Continue from the output file if interrupted
• •--quiet: Suppress progress output
• •--only-delete: Only run the deletion pass
• •--only-import-inlining: Only inline imports

Never use --no-import-inlining. The entire point is to produce a self-contained file.

For Long-Running Minimizations

Use --resume to continue from where you left off:

# Initial run (Ctrl-C if needed)
lake exe minimize YourFile.lean

# Resume later
lake exe minimize YourFile.lean --resume

After manually editing the .out.lean file, always use --resume to continue from the edited state.

Step 4: Review the Output

lake env lean YourFile.out.lean

Checklist Before Filing

• • The .out.lean file compiles with the expected error/panic
• • No Mathlib imports remain (ideal) or minimal imports remain
• • The error message in #guard_msgs matches exactly