Find executable via `elan which` about lean.nvim HOT 7 CLOSED

The default installation of elan though makes "fake" lean and lake binaries (which are aliases to elan). Are you saying you don't have those either?

from lean.nvim.

Ah right, I can inject those actually. Though, it still does not work "LSP is not connected" (I am using lspconfig) for some unknown reason, yet. Thank you!

from lean.nvim.

(I am using lspconfig) for some unknown reason, yet.

Are you saying you're using lspconfig directly? You don't need to, lean.nvim will call setup for you -- you just need to pass the lsp object.

from lean.nvim.

(I am using lspconfig) for some unknown reason, yet.

Are you saying you're using lspconfig directly? You don't need to, lean.nvim will call setup for you -- you just need to pass the lsp object.

Even if I do so, the big issue I am having is that even if I am in the folder of the Lean project, filetype=lean is never autodetected properly even though I have a lakefile and a lean-toolchain and it's a file called .lean and I didn't touch the ft field.

from lean.nvim.

Being in the folder of a Lean project isn't necessary for lean.nvim, it will detect the project root correctly -- if you don't have filetype detection working that sounds more like an install problem, how did you install lean.nvim?

from lean.nvim.

I installed lean.nvim via Nix / Home-Manager, CheckHealth is all green, my packdir which is loaded contains:
https://clbin.com/nNtT2

Maybe, the build process change some months/years ago I guess?

from lean.nvim.

I feel like it's related to things with filetype.lua / filetype.nvim etc.

from lean.nvim.