Lake Repair Skill (Direct Execution)

Direct execution skill for automated Lean build repair. Runs lake build, parses errors, and automatically fixes common mechanical errors in an iterative loop.

This skill executes inline without spawning a subagent.

Execution

Step 1: Parse Arguments

Extract flags from command input:

• --clean: Run lake clean before building
• --max-retries N: Maximum fix iterations (default: 3)
• --dry-run: Preview fixes without applying
• --module NAME: Build specific module only

clean=false
max_retries=3
dry_run=false
module=""

for arg in "$@"; do
  case "$arg" in
    --clean) clean=true ;;
    --dry-run) dry_run=true ;;
    --max-retries=*) max_retries="${arg#*=}" ;;
    --module=*) module="${arg#*=}" ;;
  esac
done

Step 2: Initial Clean (Optional)

If --clean flag is set:

if [ "$clean" = true ]; then
  echo "Running lake clean..."
  lake clean
fi

Step 3: Build Loop

Initialize tracking variables:

• retry_count=0
• previous_errors="" (for cycle detection)
• total_fixes=0

Step 4: Run Build

Attempt to build the project:

if [ -n "$module" ]; then
  build_output=$(lake build "$module" 2>&1)
else
  build_output=$(lake build 2>&1)
fi
build_exit_code=$?

Step 5: Parse Build Errors

Extract errors and warnings from build output using regex pattern:

Pattern: ^(.+\.lean):(\d+):(\d+): (error|warning): (.+)$

Step 6: Classify Errors

Step 7: Apply Fixes

Missing Cases Fix

Add match cases with sorry placeholders.

Unused Variable Fix

Rename by adding underscore prefix: {name} -> _{name}

Unused Import Fix

Remove the import line (only clean single-import lines).

Step 8: Final Report

After loop exits:

Lake Build Complete
===================

Build succeeded after {retry_count} iterations.

Fixes applied:
- {file}:{line} - {description}

All modules built successfully.

Error Handling

MCP Tool Failure

Fall back to lake build via Bash.

File Read/Write Failure

Skip that particular fix, continue with others.

Parse Failure

Treat as unfixable error.

Safety Measures

Conservative Fixes

• All missing case fixes use sorry placeholders
• Unused variable fixes only add underscore prefix
• Unused import removal is cautious (single-import lines only)

Cycle Prevention

• Track error signatures between iterations
• Stop if same errors recur
• Hard limit via max_retries (default 3)