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
andgrpcio
when runningpip 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.