-
Notifications
You must be signed in to change notification settings - Fork 97
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Errors tracing older repos #177
Comments
An alternative would be upgrading these repos to the latest version of Lean. Is that feasible? |
That would be possible in most cases but not ideal because it would not be a direct apples-to-apples comparison. For example in the miniF2F repo I linked, |
You could edit the installed *.py directly to remove |
I removed |
The error trace you showed was in |
Closing due to inactivity. Feel free to re-open. |
I know that LeanDojo has dropped support for older versions of Lean, but I used to be able to trace older Lean repos with older LeanDojo versions, now I'm getting errors when I do so.
Here are two examples with the following miniF2F repo: https://github.com/rah4927/lean-dojo-mew/
LeanDojo 1.3.0 logs (I removed the 1k+ lines of the repo's building):
LeanDojo 1.5.1 logs (again with build lines removed):
I understand support for older Lean versions has been dropped. Still if possible I would appreciate some insight in case the problem is simple, because many of the machine learning benchmarks such as miniF2F are on older versions of Lean, and if I cannot trace the repos I cannot evaluate on these benchmarks. Thanks!
Platform Information
The text was updated successfully, but these errors were encountered: