Add option to use plugins.lean.leanPackage only as a fallback

[MrQubo]

lean4 package doesn't work with lake projects configured with elan. So to work with these one has to set plugins.lean.leanPackage = null. But with this setting LSP will break on stand-alone files. I think that the ideal solution to have best of the two worlds is to use lean4 binaries found on PATH when available, and use binaries packaged with nixvim only if it's not. I believe, this behaviour should even be the default.

As for implementation, I think that appending packages bin PATH to neovim PATH should work. I'm guessing current implementation prepends extraPackages to PATH.

Additionally, I think that, the same issue applies to not only lean but probably many other LSPs. As such, it would be nice to have nixvim option like extraPackagesAppend or extraPackagesFallback, that will append the packages bin path to neovim PATH.

[MrQubo]

Alternative solution for the problem is that, whenever a lean project development environment is being set-up (via e.g. flakes), than nixvim should also be configured for the development environment, in which case one can set leanPackage to the same one as used by the project.

[GaetanLepage]

This is an interesting proposition.
Regarding extraPackages, this is forwarded to nixpkgs's neovim wrapper and I am not sure we have enough control to decide whether the PATH gets appended or prepended...
Also, nixvim can only take decisions at build time and cannot change at runtime.
The solution would be to set the "binary name" option (from the plugin or nvim-lspconfig) to a lua function that handles the suggested logic.

[MrQubo]

I think we just need this, but with --suffix instead of --prefix.

nixvim/modules/top-level/output.nix

Line 344 in c7a600c

) ''--prefix PATH : "${lib.makeBinPath config.extraPackages}"'')

Iirc nixvim uses unwrapped neovim, and extraPackages is implemented in nixvim's wrapper.

[MattSturgeon]

Hm, maybe we should have two extraPackages options, one for --prefix and another for --suffix?