search

lean-dojo / ReProver

Retrieval-Augmented Theorem Provers for Lean
https://leandojo.org
MIT License
208 stars 44 forks source link

url, hashcode in scripts/download_data.py #33

Closed irene622 closed 9 months ago

irene622 commented 9 months ago

Hi, I found an error when running scripts/download_data.py.

Since the benchmark version was updated from v3 to v5, the url and the hashcode are changed, but the code has not changed. So, I change the latest urls and hashcodes in both Lean version 3 and 4.

After making the changes, I run scripts/download_data.py and there are no errors.

Please check them! Thanks! :)

yangky11 commented 9 months ago

looks good to me. thanks