Open sagehane opened 2 years ago
Also, this plugin seems to slow down Neovim's startup time for all files I open; not just Idris files.
The annoying error message should be dealt with and I will investigate the issue with the startup times. In the mean time I suggest using some sort of lazy loading. Since you are using Packer, you cannot use the ft
option to lazy load, because the idris2 filetype is created by the plugin itself, therefore you must use autocmds or the custom function lazy loading of Packer.
@sagehane can you share your Packer config? I don't get any errors in my Packer script when the executable is missing, I only see it in the output of :LspInfo
.
@gwerbin, you should be correct because I can no-longer reproduce the error message for non-Idris2 files. Assuming I wasn't delusional, it probably was fixed since then.
The LSP still causes slow-downs for Neovim if the plugin is loaded and idris2
is in PATH
(help appreciated if you can reproduce it). Although that probably could be tracked by a different issue, and this can be closed. Thoughts?
Issue description
Running Neovim will always cause it to start with the following error message:
This error message occurs even if the filetype opened isn't Idris2.
How to reproduce:
Start neovim with
idris2-nvim
setup, withoutidris2
in$PATH
. This issue doesn't occur withidris2-lsp
missing, unless opening an Idris2 file (which seems reasonable to me).I use Packer as my plugin manager and could reproduce the issue with the startup command only being
require('idris2').setup({})
, as per the README.Expected behaviour/Proposed solution:
I think this error message should only pop up when opening Idris2 files. I hate having to comment/uncomment this plugin on my system depending on whether or not I have access to
idris2
on my system.Also, there are certain use-cases like Nix/Guix where people might only install certain packages as a dependency of project through
nix-shell
and Idris2 might be one of them.Maybe this issue can also be circumvented by setting the plugin as optional on Packer or whatever, but I don't really know how to do that and I don't think all plugin managers would support that.