15 second Lean 3 startup time

[darabos]

Hi,
Thanks for LeanDojo! I've just switched from lean-gym. As I understand, lean-gym re-used the same Lean process for all theorems if I used env.reset(). I don't see an equivalent in LeanDojo, so it's starting a separate Lean process for each theorem. Which is nice because the Lean process doesn't use up all my RAM anymore. 😅

But starting Lean takes 15 seconds for me. It's not a big deal when you're running a proof search for 10 minutes, but during development I would prefer if this could be avoided.

I thought I'd ask if you have any advice.

• I haven't tried Lean 4. Is it faster to start up?
• Is 15 seconds normal? Or is my Lean messed up?
• What is Lean doing during startup? Maybe there is some configuration to turn off something that's slow?

Thanks!

[yangky11]

Hi,

Thank you for your interest in LeanDojo! I'd say 15 seconds is pretty fast for LeanDojo, since sometimes it can take 1 or 2 minutes. A lot of things happen during startup, e.g., downloading/installing the right version of Lean, copying the traced repo from the cache to a local directory, locating the target proof, and inserting LeanDojo's special tactics into the target proof.

As discussed in #50, Lean 4 + disabling Docker might lead to significant speedup.

LeanDojo wasn't optimized for startup time, but there are community-driven efforts trying to improve it (discussions in #50 and #63)

[yangky11]

I finally get some time to work on this. This is the draft PR. I'll make a few further improvements and merge it into main.