Lean Proof Repair

lean_automator.lean.proof_repair

Attempts heuristic automated repairs for common Lean compilation errors.

This module provides functionality to analyze Lean compilation error logs and attempt simple, pattern-based repairs on the corresponding Lean code. The goal is to automatically fix common, easily identifiable issues that might arise from LLM code generation, potentially reducing the number of LLM retry cycles needed.

Note: Currently, specific repair handlers (like for 'no goals to be solved') are disabled, and the main function attempt_proof_repair will always return indicating no fix was applied. Future handlers for other error patterns can be added here.

Functions

attempt_proof_repair(lean_code: str, error_log: str) -> Tuple[bool, str]

Attempts to automatically repair simple, known Lean compilation errors.

Analyzes the error_log for specific, fixable error patterns. If a known pattern is detected by an enabled handler, this function modifies the lean_code to attempt a fix.

Currently, all specific repair handlers are disabled. Therefore, this function will always return (False, original_lean_code).

Parameters:

Name	Type	Description	Default
lean_code	str	The Lean code string that failed compilation.	required
error_log	str	The stderr/stdout captured from the failed lake build or lean command.	required

Returns:

Type

Description

Tuple[bool, str]

Tuple[bool, str]: A tuple containing: bool: True if a fix was attempted and resulted in modified code, False otherwise (including if no matching error pattern was found, if the relevant handler is disabled, or if an error occurred during the fix attempt). Currently always False. str: The potentially modified Lean code string if a fix was applied, otherwise the original lean_code. Currently always the original lean_code.

Source code in lean_automator/lean/proof_repair.py

def attempt_proof_repair(lean_code: str, error_log: str) -> Tuple[bool, str]:
    """Attempts to automatically repair simple, known Lean compilation errors.

    Analyzes the `error_log` for specific, fixable error patterns. If a known
    pattern is detected by an *enabled* handler, this function modifies the
    `lean_code` to attempt a fix.

    Currently, all specific repair handlers are disabled. Therefore, this function
    will always return `(False, original_lean_code)`.

    Args:
        lean_code (str): The Lean code string that failed compilation.
        error_log (str): The stderr/stdout captured from the failed `lake build`
            or `lean` command.

    Returns:
        Tuple[bool, str]: A tuple containing:

            - bool: `True` if a fix was attempted and resulted in modified code,
              `False` otherwise (including if no matching error pattern was found,
              if the relevant handler is disabled, or if an error occurred during
              the fix attempt). Currently always `False`.

            - str: The potentially modified Lean code string if a fix was applied,
              otherwise the original `lean_code`. Currently always the original
              `lean_code`.
    """
    logger.debug(
        "Attempting automated proof repair (Note: Specific handlers "
        "currently disabled)..."
    )
    original_code = lean_code  # Store original code for return if no fix applied

    # Basic validation
    if not lean_code or not error_log:
        logger.debug("Skipping repair: No code or error log provided.")
        return False, original_code  # Cannot repair without input

    # --- Handler 1: Only "no goals to be solved" errors (CURRENTLY DISABLED) ---
    # This handler remains disabled as the simple fix proved insufficient.
    # The logic is kept for reference or future reactivation.
    # ```python
    # if _is_only_no_goals_error(error_log):
    #     logger.info("Detected 'no goals to be solved' pattern (Handler Disabled).")
    #     # FIX DISABLED: return False, original_code
    #     # Attempt fix if handler were enabled:
    #     # try:
    #     #     modified_code = _fix_no_goals_error(lean_code, error_log)
    #     #     if modified_code != original_code and modified_code.strip():
    #     #         logger.info("Applied hypothetical fix for 'no goals'.")
    #     #         return True, modified_code
    #     #     else:
    #     #          logger.warning(
    #     #              "Hypothetical 'no goals' fix resulted in no change "
    #     #              "or empty code."
    #     #          )
    #     #          return False, original_code
    #     # except Exception as e:
    #     #      logger.exception(
    #     #          f"Error during disabled 'no goals' fix execution: {e}"
    #     #      )
    #     #      return False, original_code
    # ```
    # --- End Disabled Handler ---

    # --- Placeholder for Future Handlers ---
    # Add `elif` blocks here to check for other error patterns and call
    # corresponding `_fix_...` functions when handlers are developed and enabled.
    # Example:
    # elif _is_some_other_fixable_pattern(error_log):
    #     logger.info("Detected other fixable pattern...")
    #     # ... call fixer function ...
    #     # return True, modified_code

    # --- Default Case: No Enabled Handler Matched ---
    # If execution reaches here, it means no enabled handler recognized the
    # error pattern.
    logger.debug("No enabled/matching fixable error pattern detected in error log.")
    return False, original_code  # Return False and the original code