Server crash when trying to use suggestions

[RenanFlorencio]

Hello!

I was able to run every command in the instruction before applying LeanCopilot tactics. However, when I try to use suggest_tactics or search_proof I get the error:
Server process for file:///home/renanflorencio/teste/Teste/Basic.lean crashed, likely due to a stack overflow or a bug.

I tried restarting the file and the server, but it did not work.
After applying a tactic and running lake build I get:

 ...
⣷ [686/688] Running Teste.Basic (+
⣷ [686/688] Running Teste.Basic (+
⣷ [686/688] Running Teste.Basic (+
⣯ [686/688] Running Teste.Basic (+
...

This goes on and on for some seconds until I finally get the error:

error: Lean exited with code 132
Some required targets logged failures:
- Teste.Basic
error: build failed

I'm using version 4.28.0:

lakefile.toml:

name = "teste"
version = "0.1.0"
keywords = ["math"]
defaultTargets = ["Teste"]

[leanOptions]
pp.unicode.fun = true # pretty-prints `fun a ↦ b`
relaxedAutoImplicit = false
weak.linter.mathlibStandardSet = true
maxSynthPendingDepth = 3

[[require]]
name = "mathlib"
scope = "leanprover-community"
rev = "v4.28.0"

[[lean_lib]]
name = "Teste"

moreLinkArgs = ["-L./.lake/packages/LeanCopilot/.lake/build/lib", "-lctranslate2"]

[[require]]
name = "LeanCopilot"
git = "https://github.com/lean-dojo/LeanCopilot.git"
rev = "v4.28.0"

lean toolchain: leanprover/lean4:v4.28.0

Feel free to ask me if you need any more details.

I do not have a dedicated GPU and I'm running it on Ubuntu WSL.
Processor: Intel(R) Core(TM) Ultra 7 165U, 1700 Mhz, 12 Core(s), 14 Logical Processor(s)
OS Name : Microsoft Windows 11 Education

WSL Information:
WSL version: 2.6.3.0
Kernel version: 6.6.87.2-1
WSLg version: 1.0.71
MSRDC version: 1.2.6353
Direct3D version: 1.611.1-81528511
DXCore version: 10.0.26100.1-240331-1435.ge-release
Windows version: 10.0.26100.7840

WSL OS:
Distributor ID: Ubuntu
Description: Ubuntu 24.04.4 LTS
Release: 24.04
Codename: noble