Find executable via elan which

[RaitoBezarius]

My system does not have any lean in the PATH of my NeoVim instance (I do this for any language to avoid pollution/confusion), generally, in Lean, we use elan as a switcher for the version we use, otherwise we can fallback to Lean.

I guess all that needs to do is to build a function inside of the _util.lua and replace all hardcoding of lean command to a lookup.

[Julian]

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?

[RaitoBezarius]

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!

[Julian]

(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.

[RaitoBezarius]

(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.

[Julian]

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?

[RaitoBezarius]

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?

[RaitoBezarius]

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