Fail to use "suggest_tactics"

[HanksonYe]

Thank you very much for your help with my problem!
I have partially succeeded in using LeanCopilot in WSL Ubuntu. I can successfully import Mathlib.Data.Set.Basic and LeanCopilot. Moreover, I can successfully use "search_proof." Please refer to the following figure for instance:

However, when I try to use "suggest_tactics," It raises an error that it can not find the model ct2-leandojo-lean4-tacgen-byt5-small:

But I have already downloaded all models successfully using "lake exe LeanCopilot/download":

It is really weird, and I can not fix this problem. I have tried to follow the suggestions using "lake exe LeanCopilot/download" to redownload it, but it still can't work.
Thanks a lot if you can give me any help about this problem.

[HanksonYe]

And I also can't use "select_premises" for the similar reasons: