LSP handling for code actions is broken and deprecated

[SephVelut]

The LSP handler injected by lean.setup() appears to strip the data field from codeAction/resolve requests. When executing a :lua vim.lsp.buf.code_action() the following panic occurs

[ERROR] .../lean/stderr.lua:92    "rpc"    "lake"    "stderr"    "PANIC at Lean.Server.CodeAction.getFileSource! Lean.Server.CodeActions.Basic:47:22: no data param on code action Change to IO.println\nbacktrace:\n" 

Disabling this plugin's LSP management and using the native Neovim client fixes the issue:

require('lean').setup{ lsp = { enable = false } }

vim.lsp.config('leanls', {
    cmd = { 'lean', '--server' },
    init_options = {
        editDelay = 10,
        hasWidgets = true,
    },
    on_attach = function(client, bufnr)
        local opts = { buffer = bufnr, noremap = true, silent = true }
        vim.keymap.set('n', '<C-CR>', vim.lsp.buf.code_action, opts)
    end,
})
vim.lsp.enable('leanls')

neovim v0.11.5

[Julian]

Can you share a full reproducer here for the behavior you're observing? I don't believe I've noticed any recent issues with code actions but keen to hear if there's something specific which is broken.

[SephVelut]

local lazypath = vim.fn.stdpath("data") .. "/lazy/lazy.nvim"
if not (vim.uv or vim.loop).fs_stat(lazypath) then
  local lazyrepo = "https://github.com/folke/lazy.nvim.git"
  local out = vim.fn.system({ "git", "clone", "--filter=blob:none", "--branch=stable", lazyrepo, lazypath })
  if vim.v.shell_error ~= 0 then
    vim.api.nvim_echo({
      { "Failed to clone lazy.nvim:\n", "ErrorMsg" },
      { out, "WarningMsg" },
      { "\nPress any key to exit..." },
    }, true, {})
    vim.fn.getchar()
    os.exit(1)
  end
end
vim.opt.rtp:prepend(lazypath)

return require('lazy').setup({
    {
        'nvim-lua/plenary.nvim',
    },
    {
        'Julian/lean.nvim',
        event = { 'BufReadPre *.lean', 'BufNewFile *.lean' },

        dependencies = {
            'nvim-lua/plenary.nvim',
        },
        opts = {
            mappings = true,
            lsp = { enable = true },
        },
    },
    {
        'neovim/nvim-lspconfig',
    },
})

~/.config/nvim/after is not in the path for repro test.

[Julian]

What Lean code and what interaction with it?

[SephVelut]

The crash is not specific to any particular Lean code. The trigger is selecting a code action. Lean 4.26

[Julian]

So with any lean code you have, you cannot invoke a code action?

I can't reproduce neither locally nor here in CI, nor have I seen other users have that general of an issue, please work on sharing a full reproducer of the behavior.

[SephVelut]

This is a repro with nvim -u repro.lua Main.lean and neovim's after dir moved out. If you have any suggestions on further isolating this then feel free to reopen.