search

lean-dojo / ReProver

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

Unknown package "Mathlib" #58

Closed hongjin-su closed 2 months ago

hongjin-su commented 2 months ago

In reproducing numbers in the paper, I encounter the error unknown package 'Mathlib'. Do you know what is the potential issue? Thanks!

yangky11 commented 2 months ago

It would be more helpful if you can post the exact steps to reproduce the error.

hongjin-su commented 2 months ago

Thanks a lot for your response! The problem is the incorrect permission of the .elan folder, which results in the installation failure of Mathlib. Thanks a lot for the great work!