Lean 4 lsp server not found

[KihongHeo]

Hi. I got the following error: "Lean 4 lsp server not found" when any of the command is invoked such as "LeanGoal".

Here is the output of :check health lean

lean.nvim (d799fb2) ~
- ✅ OK Neovim is new enough.
- `vim.version()`:  0.12.0-dev
- ✅ OK Lake is runnable.
- `lake --version`:  Lake version 5.0.0-src+ad1a017 (Lean version 4.23.0-rc2)
- ⚠️ WARNING You have active timers, which can degrade infoview (CursorMoved) performance.
  - ADVICE:
    - See https://github.com/Julian/lean.nvim/issues/92

Is there any way I can fix the issue?

[Julian]

Is there anything else notable about your Lean setup perhaps? If you clone Mathlib,say, and run lake exe cache get then lake build does it appear to work?

[KihongHeo]

I think this is because of a conflict with other plugins (e.g., vim-polyglot). Fixed by removing conflicing plugins. Thanks.