Closed RaitoBezarius closed 11 months ago
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?
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!
(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.
(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.
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
?
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?
I feel like it's related to things with filetype.lua / filetype.nvim etc.
My system does not have any
lean
in thePATH
of my NeoVim instance (I do this for any language to avoid pollution/confusion), generally, in Lean, we useelan
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.