Troubleshooting

When troubleshooting, set the environment variable VERBOSE=1 to get debug logs. Below are some common errors when using LeanDojo:

Installation

  • I run into errors related to lxml and grpcio when running pip install lean-dojo on a Mac with Apple silicon.

This is a known issue with these two packages on Apple silicon. You should install them using whatever way that works for you. See these two posts on Stack Overflow.

Tracing Repos

  • The process is killed when tracing a repo.

The most likely reason is your machine doesn’t have enough memory. The amount of memory required depends on the repo you’re tracing. For large repos, such as mathlib, you need at least 32 GB memory. If getting more memory is not an option, you can try a smaller repo. If your machine has enough memory but the process still gets killed, please check whether your Docker has access to all resources of host machine (see here).

Interacting with Lean

  • docker: Error response from daemon: invalid mount config for type "bind": bind source path does not exist

Make sure Docker has access to the /tmp directory. If you’re using Docker Desktop, go to Settings -> Resources -> File sharing.