search

lean-dojo / LeanDojo

Tool for data extraction and interacting with Lean programmatically.
https://leandojo.org
MIT License
478 stars 72 forks source link

ReProver Warning #169

Closed IanWangg closed 2 weeks ago

IanWangg commented 4 weeks ago

Description I followed the instruction from the ReProver repo, and trying to run the training script. And I get warning like this:

image

Should I worry about this? It seems that some lean files are expected from the path "Mathlib/..." and ".lake/...", which I do not have. If this is problematic, how should I fix this?

Platform Information

yangky11 commented 3 weeks ago

How many warnings did you get? One or two thousands is normal, but a number beyond that may indicate problems.

IanWangg commented 3 weeks ago

A bunch. Thank you for your reply, I think everything's normal. I just want to make sure that my data setup is correct. As I can't find any folders starting from "Mathlib/..." or ".lake/...", and when I ran the trace_repos.py, it returned an empty set.

yangky11 commented 2 weeks ago

Around one thousand should be pretty normal.

By default, the traced repos are stored in ~/.cache/lean_dojo