Fix deprecated use of lspconfig

[StamesJames]

I saw that leanls.lua is not yet in the new lsp/ directory in the lspconfig plugin. I wrote the PR 4084 to the lspconfig repo adding it. Once some default configs for leanls are in lsp/ this small change should work without the message that the deprecated framework is used.
This is related to Issue #427

[StamesJames]

The PR 4084 nvim-lspconfig seems to be merged, so it should be possible to migrate to the the vim.lsp.config now. I testet it localy and it seemed to work.

[Julian]

Thanks. Please either rebase or push an empty commit so we can see if CI agrees.

[Julian]

I hadn't seen your push but it seems CI here says this still isn't quite right, there's lots of failures. If you pull main you'll at least have the 0.10 failures go away as like I mentioned we'd have to drop 0.10 to do this (which I've now done), but the 0.11 ones still seem "real".

[StamesJames]

I will look into it. Maybe I forgot something in the lspconfig PR and the configuration.

[StamesJames]

I tested some of the failing test by hand and there they seem to work. Is it possible, that the automated tests do not use the nvim-lspconfig version where the leanls configs are already there?

[EDIT] I have just seen, that in packpath there is the right lspconfig

[Julian]

The test runs will use an isolated config, yes (one that generally pulls the latest versions of plugins when you run it).

The issues here will be more subtle, from what I saw they have to do with the fact that the change here is not a drop in replacement -- clients are attached at different times via the new interface than via the old one, either because of different autocmd events or sequencing.

[StamesJames]

Yes, I also think it is something like this, because when I use the new version outside the tests, it works just fine. I will look into the tests and how they are implemented and try to figure out if the new systems attaches LSPs differently, so that the tests do not recognize it.

[StamesJames]

Ok I am currently very confused by the tests.
I use the new version with my PR in my daily programming with lean, and it seems to work just fine. When I reproduce the tests by hand outside the test suit, it also works. Also there are these first tests that do not find an attached LSP at all but then in later tests there is LSP output in the diagnostics window so for those tests the LSP is attached even tough it also simply calls vim.cmd.edit or helpers.clean_buffer.

[yd278]

Hi, I tried to modify these lua scripts myself and find a possible workaround:

In leanls.lua of the nvim-lspconfig, the cmd is set as a function. However, I received notifications saying that the config parameter is nil, and the ls processes is not started at all.

Therefore, I simply change it into cmd = { 'lake', 'serve' }, and use the new api

vim.lsp.config('leanls', opts)
vim.lsp.enable 'leanls'

I also swapped these two line to make sure the configs are set before it get enabled. Now the ls process can get started as normal.

Hope that would be helpful!

[StamesJames]

Thank you, @yd278, that is very helpful. That your config parameter is nil is strange, when I run it, it is not.
According to the nvim help page, returning a function for cmd is supported

      • {cmd}                  (`string[]|fun(dispatchers: vim.lsp.rpc.Dispatchers, config: vim.lsp.ClientConfig): vim.lsp.rpc.PublicClient`)

When I wrote the config in lspconfig I wrote cmd as a function because otherwise the root_dir was not getting passed to the lsp properly.
Does your LSP register the Project you opened correctly?
Maybe the call to vim.lsp.rpc.start behaves slightly different from what is done when cmd is returned as {"lake", "serve"}

[yd278]

Hi, @StamesJames , frankly speaking ,it doesn't. I thought it work because I open the file directly under the root directory. However, I tried a minimal setup with only:

lazy.nvim
lean.nvim
nvim-lspconfig
plenary.nvim

and I can confirm that no lean/lake processes were started, a debug message attempted to index local 'config' (a nil value) appeared as well

Maybe some other plugins did something on your machine?

[StamesJames]

I tried some things in the same settings the tests run with just nvim I found that the root dir still is not right, but that can be fixed by changing the cmd to

  cmd = function(dispatchers, config)
    local local_cmd = { 'lake', 'serve', '--' }
    return vim.lsp.rpc.start(local_cmd, dispatchers, { cwd = config.root_dir })
  end,

This also lets more tests succeed, but still some fail.

One thing I noticed is, that when I open the project folder with just nvim ./spec/fixtures/projects/Example/ and then open the Example.lean file everything works but when I directly open just nvim ./spec/fixtures/projects/Example/Example.lean no LSP is attached.

[StamesJames]

I noticed, that when I manually perform
:lua vim.lsp.enable('leanls', false)
:lua vim.lsp.enable('leanls', true)
after opening Example.lean with
just nvim ./spec/fixtures/projects/Example/Example.lean
the lsp is getting attached right.
Because of this, I think there are some timing differences between the new vim.lsp.enable and the old lspconfig require. The just file uses -c to load the lean plugin and I think the command provided to -c is executed after the file is opened so I think it may be, that the new vim.lsp.enable does not start a lsp on an already opened buffer and therefore.
Does that make sense?