can not lake build on windows wsl- a problem with the modelmodel

[zhiang0226]

I try to use Lean4Example, to learn leancopilot https://github.com/yangky11/lean4-example/tree/LeanCopilot-demo?tab=readme-ov-file
But I could not run lake exe LeanCopilot/downloadI，so I manually downloaded the contents of four web pages to ~/.cache/lean_copilot/，when I run lake build, the following error occurred：

ℹ [14/552] Replayed ModelCheckpointManager.Url
info: ././././ModelCheckpointManager/Url.lean:68:0: { protocol := "https", hostname := "huggingface.co", path := FilePath.mk "kaiyuy/ct2-leandojo-lean4-tacgen-byt5-small" }
info: ././././ModelCheckpointManager/Url.lean:69:0: { protocol := "https", hostname := "huggingface.co", path := FilePath.mk "bert-base-uncased" }
info: ././././ModelCheckpointManager/Url.lean:71:0: "ct2-leandojo-lean4-tacgen-byt5-small"
info: ././././ModelCheckpointManager/Url.lean:72:0: "bert-base-uncased"

and suggest_tactics, search_proof, select_premises are not available in Lean4Example https://github.com/yangky11/lean4-example/tree/LeanCopilot-demo?tab=readme-ov-file
could your help me? @Peiyang-Song @yangky11

[zhiang0226]

Looks like I have the same problem as https://github.com/lean-dojo/LeanCopilot/issues/103