search

Julian / lean.nvim

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

Error executing vim.schedule lua callback #283

Closed mattrobball closed 1 year ago

mattrobball commented 1 year ago

OS : MacOS Ventura Nvim version: NVIM v0.8.0 Build type: Release LuaJIT 2.1.0-beta3 Compiled by brew@HMBRW-A-001-M1-004.local

It looks like the infoview widget is calling outside the bounds of a list. 

Error executing vim.schedule lua callback: ...ck/packer/start/plenary.nvim/lua/plenary/async/async.lua:18: The coroutine failed with this message: ...im/site/pack/packer/start/lean.nvim/lua/lean/widgets.lua:440: Vim:E322: line number out of range: 1 past the end
stack traceback:
    [C]: in function 'error'
    ...ck/packer/start/plenary.nvim/lua/plenary/async/async.lua:18: in function 'callback_or_next'
    ...ck/packer/start/plenary.nvim/lua/plenary/async/async.lua:45: in function 'step'
    ...ck/packer/start/plenary.nvim/lua/plenary/async/async.lua:48: in function 'execute'
    ...ck/packer/start/plenary.nvim/lua/plenary/async/async.lua:118: in function 'update'
    ...m/site/pack/packer/start/lean.nvim/lua/lean/infoview.lua:1031: in function '__update_pin_by_uri'
    ...e/nvim/site/pack/packer/start/lean.nvim/lua/lean/lsp.lua:85: in function 'fn'
    ...nvim/site/pack/packer/start/lean.nvim/lua/lean/_util.lua:129: in function <...nvim/site/pack/packer/start/lean.nvim/lua/lean/_util.lua:125>
    ...e/nvim/site/pack/packer/start/lean.nvim/lua/lean/lsp.lua:8: in function 'handler'
    ...w/Cellar/neovim/0.8

If I have more time, I will investigate further but dropping it here now.

Julian commented 1 year ago

I think I've seen this before too (though I haven't done a ton of Lean the past few weeks) -- the thing is when I looked I don't really understand what the issue is, it's supposed to be out of bounds, that's the "neovim API" way to replace the whole contents. But yeah let's leave this open and I'll try to reproduce.

Julian commented 1 year ago

I think ^^ that commit fixes this (at least it does for me). I don't really understand why this happens (if you look at the change it shouldn't really make sense for it to happen given we're replacing from 0 to -1, so I suspect there's some minor upstream issue here, but I don't care to track it down :/)

Let me know if you see this again.