Stopping 'leanls' lsp doesn't stop downloading lean toolchain

[JadAbouHawili]

As the title suggests , if you enter a lean project but don't have the required lean toolchain then lean.nvim starts downloading a new one. Using the recommended way of stopping the lsp server vim.lsp.enable('leanls',false) kills the lean server but does not stop that download

[Julian]

I'm not sure I believe what behavior is the right one here, both seem fine to me and what we have now (which is just an artifact of the fact that invoking lake via elan will autodownload and the parent process does not exit) seems arguably better.

Can you elaborate on whether or why you think this behavior isn't desirable?

[JadAbouHawili]

looking at many projects with different toolchains can be annoying where i would just want to open it in nvim without necessarily doing development and having the lsp and auto download kick in , i thought by stopping the server it wouldn't be downloading the toolchain until i noticed a couple of GBs being filled up in storage.

My expectation was the behavior I described. I don't know how this auto download feature is implemented so perhaps what I'm asking for is unreasonable

I suppose the solution would be to have an alias that refers to a nvim config without lean.nvim installed , something along the lines of

alias nvim-no-lean='NVIM_APPNAME="nvim-no-lean" nvim'

[JadAbouHawili]

the behavior i want is if i have the toolchain installed then the server should kick in , if not then nothing should happen and I'm just in nvim looking at text.