LeanDojo tracing and caching

Stream: Machine Learning for Theorem Proving

[Gerben Koopman]

Hi all,

I'm not entirely sure how Zulip works, this being my first time posting something, but hopefully someone can point me in the right direction.

I've been trying to use LeanDojo as a gym-like environment for reinforcement learning. For those unfamiliar, the idea is to apply the ideas from models such as AlphaGo to the Lean tactics system for theorem proving. This is probably a well explored avenue on this subzullip (if that is the word?), but I can't find any topics myself.

My question is, given a traced version of Mathlib4 that is compatible with LeanDojo and the installed Lean4 version, I keep trying to access the theorems using the cache. I can verify that the cache is there, and that it is not corrupted, but regardless after loading the repo into memory, the code still begins retracing.

Has anyone run into similar issues before? Or do people have some familiarity with LeanDojo? Before dumping a bunch of code snippets with potential mistakes, which would make this post even longer (apologies), I thought I'd ask if anyone would be able to help.

Many thanks!
Gerben

[Gerben Koopman]

The repo in question is github.com/GerbenKoopman/LeanReinforcement, but it is quickly growing very messy and chaotic due to much falling standing up and more falling.

[Kaiyu Yang]

Feel free to post an issue in LeanDojo's GitHub repo. You may also want to explore whether other alternatives work for your use case, e.g., https://github.com/leanprover-community/repl, https://github.com/leanprover/Pantograph, https://github.com/project-numina/kimina-lean-server

[Nicholas Jiang]

Hi there, I'm new to Zulip as well. I tried to trace the miniF2F-lean4 repo with LeanDojo and got an error. I thought I'd bring some more attention to the issue since it's been a few days without any activity on my issue. Not sure if it's better to move it directly to the LeanDojo's GitHub repo. https://github.com/yangky11/miniF2F-lean4/issues/31

[Gerben Koopman]

Hi Nicholas, I've since solved my issue, but maybe I can still help you with the error you're running into. I thought it might be related to https://github.com/lean-dojo/LeanDojo/issues/211, but it looks like you're using Lean version 4.10? Regardless, the latest MiniF2F repo uses mathlib v.4.24 so that might still be it. Maybe worth trying to downgrade MiniF2F to something pre 4.12 and see if that works?

[Nicholas Jiang]

Related: I'm not sure if leandojo automatically uses the lean version from the repo's lean-toolchain file when tracing. For the repo I was tracing it's using 4.24 now but I think it was 4.21 when I tried tracing (https://github.com/yangky11/miniF2F-lean4/blob/main/lean-toolchain)

[Gerben Koopman]

Yeah exactly, but both are post-v4.12, which the issue is about. The only thing that makes me unsure is because it states to only be in tactic mode and I'm still getting my bearing in the whole TacticM stuff that Lean uses (not by statements but rather the metaprogramming used). Perhaps others can confirm if this issue is related to tracing in the first place.