Have to set ft=lean3 to hook lean3ls

[fecet]

I'm a lean starter, so please point out if I get anything wrong. I have followed READEME and finish the setup, then I start learning lean with the tutorial project, as the project require mathlib, I still use lean3.

However, open a lean file didn't hook lean3ls successful, I have to set ft=lean3 as @ram02z in https://github.com/Julian/lean.nvim/issues/170#issuecomment-942050777 mentioned, which is being reported as solved.

Here is my config about lean

require("lean").setup({
    abbreviations = { builtin = true },
    lsp = {
        disable = true,
    },
    lsp3 = {
        on_attach = custom_attach,
        capabilities = capabilities,
        -- cmd = { "lean-language-server", "--stdio" },
        cmd = { "lean-language-server", "--stdio", "--", "-M", "16384", "-T", "100000" },
    },
    mappings = true,
    ft = { default = "lean3" },
    progress_bars = {
        -- Enable the progress bars?
        enable = true,
        -- Use a different priority for the signs
        priority = 10,
    },
})

[rish987]

I just tried your config and had no issues, so I'll need a bit more information here. When you open up a lean3 file and do :set ft? do you get filetype=lean, filetype=, or something else? If it's empty, I'd suspect you haven't installed the plugin correctly (it needs to be able to source ftdetect/lean.lua BEFORE you BufRead the lean3 file), but if it's lean then something funky must be going on with the automatic filetype detection.

[fecet]

ource ftdetect/lean.lua BEFORE

I get filetype=lean3 if the extension is "file.lean3", for file "file.lean", I get "filetype=lean"

[rish987]

That's interesting, I can't repro that behavior, for file.lean3 I get an empty filetype. Perhaps your neovim is simply applying the filetype based on the extension somehow -- to make sure that the autocmd is being fired, could you add a print"HERE" to the callback function at the bottom of ftdetect/lean.lua and see if that gets printed when you open a Lean file? If it does, you can further debug by adding print statements to the detect function above.

If it doesn't print, can you try plopping ftdetect/lean.lua in ~/.config/nvim/ftdetect and see if that fixes the issue? If that's the case you might have a broken install.

[fecet]

It doesn't print, I guess that's because of my massive lazyload settings in packer, I have managed to work around it by adding a file types settings.

return function()
    require("lean").setup({
        abbreviations = { builtin = true },
        lsp = { enable = false },
        lsp3 = {
            cmd = { "lean-language-server", "--stdio", "--", "-M", "16384", "-T", "100000" },
            filetypes={"lean","lean3"}
        },
        mappings = true,
        ft = { default = "lean3" },
        progress_bars = {
            -- Enable the progress bars?
            enable = true,
            -- Use a different priority for the signs
            priority = 10,
        },
    })
end

I will keep investigating it in case there is any unexpected behavior. Thanks for your help.