Noob question.The command was not found or executable: lake

[1854039]

I train the retrieval model according to readme step, and I save the deepspeed checkpoint ,
Then I provide the checkpoint as retrieval when training the generate model. But I get this:

It would be so nice if you could share some kindly idea on why I meet this. Maybe I have to download elan?

[1854039]

the error starts here:

when searching for proof .
but I can't see the relationship between these 2 parts of error info.

[yangky11]

Did you install elan following the README?

https://github.com/lean-dojo/ReProver?tab=readme-ov-file#requirements

5. Satisfy the requirements of LeanDojo.

[1854039]

Yes that's the reason. Thank you so much!