Infoview crash on hover for terms without docstrings (Neovim 0.12)

[justus-springer]

Description

Pressing <CR> on a term with no doctoring in the infoview crashes with: attempt to get length of local 'text' (a userdata value)

Example

To reproduce, run Neovim 0.12 with lean.nvim v2026.4.1 and open a file with contents:

/-- A docstring. -/
def a : Nat := 0

def b : Nat := 0

example : a = b := by
  sorry

Put the cursor on the sorry and open the infoview. In the infoview, putting the cursor on a and pressing <CR> opens the expected popup. But putting the cursor on b and pressing <CR> produces an error:

vim.schedule callback: /Users/justus/lean/lean.nvim/lua/std/async.lua:26: /Users/justus/lean/lean.nvim/lua/lean/tui.lua:362: attempt to get length of local
 'text' (a userdata value)                                                                                                                                 
stack traceback:                                                                                                                                           
        /Users/justus/lean/lean.nvim/lua/lean/tui.lua: in function 'go'                                                                                    
        /Users/justus/lean/lean.nvim/lua/lean/tui.lua:382: in function 'go'                                                                                
        /Users/justus/lean/lean.nvim/lua/lean/tui.lua:399: in function 'render_lines'                                                                      
        /Users/justus/lean/lean.nvim/lua/lean/tui.lua:848: in function 'render'                                                                            
        /Users/justus/lean/lean.nvim/lua/lean/tui.lua:1020: in function 'hover'                                                                            
        /Users/justus/lean/lean.nvim/lua/lean/tui.lua:1087: in function 'rehover'                                                                          
        ...stus/lean/lean.nvim/lua/lean/widget/interactive_code.lua:98: in function <...stus/lean/lean.nvim/lua/lean/widget/interactive_code.lua:86>       
stack traceback:                                                                                                                                           
        [C]: in function 'error'                                                                                                                           
        /Users/justus/lean/lean.nvim/lua/std/async.lua:26: in function </Users/justus/lean/lean.nvim/lua/std/async.lua:25>                               

Possible fix

The root cause might have to do with changing behavior in Neovim's LSP JSON decoding of null values. A possible fix is to strengthen the guard in L67 of lua/lean/widget/interactive_code.lua from

lean.nvim/lua/lean/widget/interactive_code.lua

Line 67 in b7b330a

if info_popup.doc ~= nil then

to

if type(info_popup.doc) == 'string' then

Versions

• Neovim: 0.12.1
• lean.nvim: v2026.4.1
• Lean toolchain: Lean (version 4.30.0-rc2, arm64-apple-darwin24.6.0, commit 3dc1a088b6d2d8eafe25a7cd7ec7b58d731bd7cc, Release)