search

Julian / lean.nvim

neovim support for the Lean theorem prover
MIT License
255 stars 25 forks source link

ftdetect script references rest of plugin #272

Closed 4e554c4c closed 2 years ago

4e554c4c commented 2 years ago

Hi! I'd like to only load the lean.nvim plugin if im editing a lean file. I'm currently using the packer package manager, so I did

 use { 'Julian/lean.nvim', ft = { 'lean', 'lean3' }}

In order to do this, packer installs lean.nvim's ftdetect script without the rest of the plugin, so that lean.nvim can do filetype detection in order to determine if the plugin should be loaded. Unfortunately, lean.nvim's ftdetect script calls into the plugin itself. Because the plugin isn't loaded at the time, this causes filetype detection to crash.

Getting around this isn't too hard, since the fix is to just do

 use { 'Julian/lean.nvim', ft = { 'lean', 'lean3' }, module = 'lean'}

but it still doesn't seem optimal since this is loading the entire lean plugin when it's not necessary to do so.

It seems like it would be pretty easy to solve this by moving main/lua/lean/ft.lua to ftdetect/lean3.lua instead of using the vimscript shim.

Julian commented 2 years ago

This is probably a vestige from versions of neovim that predate supporting ftdetect in lua. Any chance you're interested in a PR?

4e554c4c commented 2 years ago

yep, I'll send one :smile: just try to check beforehand that it's desired