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:

[byrong7]

Hi @HanksonYe,

I hope this message finds you well. I noticed your involvement with LeanCopilot and Mathlib and wanted to ask if you could guide me on how you managed to run LeanCopilot with Mathlib.

I'm working on a similar project and would greatly appreciate learning about your process, any challenges you faced, and how you resolved them.

Thank you very much for your time and assistance!

[HanksonYe]

@byrong7
Sorry to reply late. I'm happy to help you with using LeanCopilot with Mathlib. When I installed the LeanCopilot, I followed the Readme of LeanCopilot guidelines. The only thing I have changed is that I have checked the version/commit of the Mathlib in Step 1 in the Readme. I paste the context of my lakefile.lean here for convenience:

import Lake
open Lake DSL

package «my_project2» {
-- Settings applied to both builds and interactive editing
leanOptions := #[
⟨pp.unicode.fun, true⟩ -- pretty-prints fun a ↦ b`
]
-- add any additional package configuration options here
moreLinkArgs := #[
"-L./lake/packages/LeanCopilot/.lake/build/lib",
"-lctranslate2"
]
}

require mathlib from git
"https://github.com/leanprover-community/mathlib4.git" @ "20c73142afa995ac9c8fb80a9bb585a55ca38308"

require LeanCopilot from git
"https://github.com/lean-dojo/LeanCopilot.git" @ "880f820ecbc128166a9a07b19497d1b4fa8090ae"

@[default_target]
lean_lib «MyProject2» where
-- add any library configuration options here

Here "my_project2" and "MyProject2" depend on the name of your lean project.

Then, other steps follow the same as those in the Readme. And finally, you can find that LeanCopilot can work partially: only the tactic "search_proof" can work.

Please get in touch with me if you have any difficulty installing LeanCopilot.

[yangky11]

I just updated LeanCopilot to support v4.14.0 and v4.15.0-rc1. Can you try again and see if the issue still persists?