Julian / lean.nvim

Neovim support for the Lean theorem prover
MIT License
278 stars 27 forks source link

Setting `ft` configuration causes an error on startup #353

Closed Ben10164 closed 1 month ago

Ben10164 commented 1 month ago

All commits from 2d76773e1a09769310248bbf2ae6797a9d3370bb and later no longer successfully run. All features stop working.

On a fresh install I get the following error:

[ERROR Sun Sep 22 10:14:18 2024] ...hare/nvim/lazy/neo-tree.nvim/lua/neo-tree/utils/init.lua:761: Error opening file: vim/_editor.lua:0: nvim_exec2()..BufReadPost Autocommands for "*": Vim(append):Error executing lua callback: ...v0.10.0/nvim-macos-arm64/share/nvim/runtime/filetype.lua:35: Error executing lua: ...v0.10.0/nvim-macos-arm64/share/nvim/runtime/filetype.lua:36: nvim_exec2()..BufReadPost Autocommands for "*"..FileType Autocommands for "*"..function <SNR>1_LoadFTPlugin[20]..script /Users/[redacted]/.local/share/nvim/lazy/lean.nvim/ftplugin/lean/lean.lua: Vim(runtime):E5113: Error while calling lua chunk: .../.local/share/nvim/lazy/lean.nvim/ftplugin/lean/lean.lua:40: attempt to call method 'should_modify' (a nil value)
stack traceback:
    .../.local/share/nvim/lazy/lean.nvim/ftplugin/lean/lean.lua:40: in main chunk
    [C]: in function 'nvim_cmd'
    ...v0.10.0/nvim-macos-arm64/share/nvim/runtime/filetype.lua:36: in function <...v0.10.0/nvim-macos-arm64/share/nvim/runtime/filetype.lua:35>
    [C]: in function 'nvim_buf_call'
    ...v0.10.0/nvim-macos-arm64/share/nvim/runtime/filetype.lua:35: in function <...v0.10.0/nvim-macos-arm64/share/nvim/runtime/filetype.lua:10>
    [C]: in function 'nvim_exec2'
    vim/_editor.lua: in function <vim/_editor.lua:0>
    [C]: in function 'pcall'
    ...hare/nvim/lazy/neo-tree.nvim/lua/neo-tree/utils/init.lua:741: in function 'open_file'
    ...y/neo-tree.nvim/lua/neo-tree/sources/common/commands.lua:733: in function 'open'
    ...y/neo-tree.nvim/lua/neo-tree/sources/common/commands.lua:755: in function 'open_with_cmd'
    ...y/neo-tree.nvim/lua/neo-tree/sources/common/commands.lua:764: in function 'open'
    ...o-tree.nvim/lua/neo-tree/sources/filesystem/commands.lua:184: in function <...o-tree.nvim/lua/neo-tree/sources/filesystem/commands.lua:183>
stack traceback:
    [C]: in function 'nvim_cmd'
    ...v0.10.0/nvim-macos-arm64/share/nvim/runtime/filetype.lua:36: in function <...v0.10.0/nvim-macos-arm64/share/nvim/runtime/filetype.lua:35>
    [C]: in function 'nvim_buf_call'
    ...v0.10.0/nvim-macos-arm64/share/nvim/runtime/filetype.lua:35: in function <...v0.10.0/nvim-macos-arm64/share/nvim/runtime/filetype.lua:10>
    [C]: in function 'nvim_exec2'
    vim/_editor.lua: in function <vim/_editor.lua:0>
    [C]: in function 'pcall'
    ...hare/nvim/lazy/neo-tree.nvim/lua/neo-tree/utils/init.lua:741: in function 'open_file'
    ...y/neo-tree.nvim/lua/neo-tree/sources/common/commands.lua:733: in function 'open'
    ...y/neo-tree.nvim/lua/neo-tree/sources/common/commands.lua:755: in function 'open_with_cmd'
    ...y/neo-tree.nvim/lua/neo-tree/sources/common/commands.lua:764: in function 'open'
    ...o-tree.nvim/lua/neo-tree/sources/filesystem/commands.lua:184: in function <...o-tree.nvim/lua/neo-tree/sources/filesystem/commands.lua:183>
stack traceback:
    [C]: in function 'nvim_buf_call'
    ...v0.10.0/nvim-macos-arm64/share/nvim/runtime/filetype.lua:35: in function <...v0.10.0/nvim-macos-arm64/share/nvim/runtime/filetype.lua:10>
    [C]: in function 'nvim_exec2'
    vim/_editor.lua: in function <vim/_editor.lua:0>
    [C]: in function 'pcall'
    ...hare/nvim/lazy/neo-tree.nvim/lua/neo-tree/utils/init.lua:741: in function 'open_file'
    ...y/neo-tree.nvim/lua/neo-tree/sources/common/commands.lua:733: in function 'open'
    ...y/neo-tree.nvim/lua/neo-tree/sources/common/commands.lua:755: in function 'open_with_cmd'
    ...y/neo-tree.nvim/lua/neo-tree/sources/common/commands.lua:764: in function 'open'
    ...o-tree.nvim/lua/neo-tree/sources/filesystem/commands.lua:184: in function <...o-tree.nvim/lua/neo-tree/sources/filesystem/commands.lua:183>
Julian commented 1 month ago

Hi there, can you provide a fuller reproducer? They work fine here, both on a fully fresh install (which is what CI runs) as well as a LazyVim install.

Ben10164 commented 1 month ago

Holy crap, I just realized that its because I have

        ft = {
          -- A list of patterns which will be used to protect any matching
          -- Lean file paths from being accidentally modified (by marking the
          -- buffer as `nomodifiable`).
          nomodifiable = {
            -- by default, this list includes the Lean standard libraries,
            -- as well as files within dependency directories (e.g. `_target`)
            -- Set this to an empty table to disable.
          },
        },

in the config that I use.

Ben10164 commented 1 month ago

Here is a repro, but I believe it's that the nomodifiable option has been changed.

local lazypath = vim.fn.stdpath("data") .. "/lazy/lazy.nvim"

if not (vim.uv or vim.loop).fs_stat(lazypath) then
  -- bootstrap lazy.nvim
  -- stylua: ignore
  vim.fn.system({ "git", "clone", "--filter=blob:none", "https://github.com/folke/lazy.nvim.git", "--branch=stable", lazypath })
end
vim.opt.rtp:prepend(vim.env.LAZY or lazypath)

require("lazy").setup({
  spec = {
    { "LazyVim/LazyVim", import = "lazyvim.plugins" },
    {
      "Julian/lean.nvim",
      opts = {
        ft = {
          nomodifiable = {},
        },
      },
    },
  },
})

Screenshot upon opening a lean file after doing a fresh install with the above config:

Screenshot 2024-09-22 at 11 11 50 AM
dpetka2001 commented 1 month ago

No, it's the ft key that causes the problem. Even if you set ft = {}, it throws an error.

Ben10164 commented 1 month ago

No, it's the ft key that causes the problem. Even if you set ft = {}, it throws an error.

Is that the expected behavior @Julian ? The commit that I was referring to seems to be removing the ft key, but the README.md for the repo still includes it in the example configuration

Julian commented 1 month ago

Fixed in the linked commit, please follow up if you still have trouble.

Ben10164 commented 1 month ago

Thanks!