-
|
Is there any chance that you are willing to put traced repos used by the zenodo benchmark besides mathlib4 in the remote cache? This is necessary to run reprover's evaluate.py. That will be of great help since tracing turns out to be a major obstacle. Thank you! |
Beta Was this translation helpful? Give feedback.
Replies: 1 comment 1 reply
-
|
@zoryzhang Sorry I didn't see this earlier. Could you list the repos required by the zenodo dataset that are not yet in the remote cache? |
Beta Was this translation helpful? Give feedback.
-
|
I think in the latest (v9) zenodo dataset, there is only one repo now (leanprover-community-mathlib4-fe4454af900584467d21f4fd4fe951d29d9332a7) so this is solved. Thank you. |
Beta Was this translation helpful? Give feedback.
@zoryzhang Sorry I didn't see this earlier. Could you list the repos required by the zenodo dataset that are not yet in the remote cache?