Skip to content

Troubleshooting

This guide covers common issues you might encounter when using LeanInteract.

Common Issues

Out of Memory Errors

Symptoms:

  • The application crashes with memory-related errors
  • Python process is killed by the operating system
  • Error messages mentioning "MemoryError" or "Killed"

Solutions:

  • Reduce parallel processing or increase system memory
  • Use AutoLeanServer with conservative memory settings:
from lean_interact import AutoLeanServer
server = AutoLeanServer(config, memory_threshold_mb=1000)  # Limit to 1GB
  • Avoid working with large files or complex proofs in a single session
  • Use environment pickling to save and restore states across sessions

Timeout Errors

Symptoms:

  • Commands take too long to execute
  • Error messages mentioning "TimeoutError"

Solutions:

  • Increase the timeout in the configuration:
config = LeanREPLConfig(timeout=60)  # 60 seconds
  • Use AutoLeanServer for automatic recovery from timeouts:
server = AutoLeanServer(config)
  • Break complex commands into smaller, more manageable pieces

Long Waiting Times During First Run

Symptoms:

  • Initial setup takes a long time
  • Process seems stuck at "Downloading" or "Building"

Solution: This is expected behavior as LeanInteract:

  1. Downloads and sets up the specified Lean version
  2. Downloads and builds Lean REPL
  3. If using Mathlib, downloads it and instantiates a project using it (which is resource-intensive)

Subsequent runs will be much faster due to caching.

Lake Update Errors

Symptoms:

  • Error: Failed during Lean project setup: Command '['lake', 'update']' returned non-zero exit status 1.

Solutions:

  • Update your elan version (should be at least 4.0.0):
elan self update
  • Check your project's lake file for errors
  • Ensure Git is properly installed and can access required repositories

Path Too Long Error (Windows)

Symptoms:

  • On Windows, errors related to path length limitations
  • Git errors about paths exceeding 260 characters

Solutions: Enable long paths in Windows 10/11:

# Run in administrator PowerShell
New-ItemProperty -Path "HKLM:\SYSTEM\CurrentControlSet\Control\FileSystem" -Name LongPathsEnabled -Value 1 -PropertyType DWord -Force
git config --system core.longpaths true

Cache Issues

Symptoms:

  • Unexpected behavior after upgrading LeanInteract
  • Errors about incompatible versions

Solution: Clear the LeanInteract cache:

clear-lean-cache

Unexpected Lean error messages

Symptom: LeanInteract returns error messages while the Lean code runs fine in VSCode.

Solutions:

  • Check you are using the same Lean version in both environments
  • If you are creating a temporary project using LeanInteract, make sure your dependencies are correctly set and compatible with the Lean version you are using

  • A frequent issue is forgetting to include mathlib in the dependencies:

    config = LeanREPLConfig(
    lean_version="v4.19.0", 
    project=TempRequireProject("mathlib")
)

  • Check if a similar issue for the Lean REPL has been reported

"'elan' is not recognized as an internal or external command"

Symptom: Error when running LeanInteract on a new system

Solution: Install Lean's version manager:

install-lean

Getting Additional Help

If you encounter issues not covered in this guide:

  1. Check the GitHub repository for open issues
  2. Open a new issue with:
  3. A minimal reproducible example
  4. Your operating system and Python version
  5. LeanInteract version (pip show lean-interact)
  6. Complete error message/stack trace