Julian/lean.nvim

📦 Inline Images and SVGs in the Infoview

• `lean.nvim` can now render images and SVGs directly in your terminal.
• This works in Kitty, WezTerm, Ghostty, and other terminals that support the protocol.
• Images scroll and clip correctly within the infoview window, and are cached to avoid redundant decoding or rasterization on re-render.
• SVG support requires installing resvg (`brew install resvg` or `cargo install resvg`).
• Raster images work without any extra dependencies.
• To disable terminal graphics entirely, set `graphics = { enabled = false }`.
• https://github.com/user-attachments/assets/ee02f764-22c5-42cb-b21f-e37c36333567

📦 Semantic Navigation in the Infoview

• The infoview now supports structured navigation between goals, hypotheses, suggestions, links, and trace diagnostics.
• Rather than scrolling or searching visually, you can jump directly to what you care about:
• | Key | What it does |
• |---|---|
• | `<LocalLeader>g` | move cursor to the first goal |
• | `]g` / `[g` | next / previous goal |
• | `]h` / `[h` | next / previous hypothesis |
• | `]s` / `[s` | next / previous suggestion |
• + 5 more

📦 Trace Search

• You can now search through trace messages directly in the infoview (the client side of [leanprover/lean4#10365](https://github.com/leanprover/lean4/pull/10365)).
• Place your cursor on a trace diagnostic and hit `<LocalLeader>/` to search — matching text is highlighted and matching traces are automatically uncollapsed.
• An empty query restores the original.
• After searching, `n` / `N` navigate between matches, and the last query is remembered.
• https://github.com/user-attachments/assets/fcda765e-a985-464e-b340-527a7a2f6b3f

📦 `<Plug>` Mappings for Everything

• All lean.nvim mappings now have `<Plug>` names, making them properly remappable.
• For example, to rebind the infoview toggle:
• ```lua
• vim.keymap.set('n', '<leader>li', '<Plug>(LeanInfoviewToggle)', { buffer = true })
• ```
• The full list of `<Plug>` names is in the README.

📦 Dropped Dependencies: `nvim-lspconfig` and `plenary.nvim`

• `lean.nvim` no longer depends on either `nvim-lspconfig` or `plenary.nvim`.
• LSP attachment is now handled natively using Neovim's built-in `vim.lsp` APIs, and plenary's async has been replaced with a thin coroutine wrapper.
• Your `dependencies` block can remove both.
• If you were passing LSP configuration through `lean.setup`'s config table, this is now deprecated — use `vim.lsp.config('leanls', {})` instead.

📦 Imports-Out-of-Date Detection

• There are two situations where Lean can indicate that a file's dependencies are stale.
• The more critical one occurs when a file is first opened and its imports need rebuilding — in this case the file cannot be checked at all until they are rebuilt.
• This behavior is customizable via the `on_imports_out_of_date` callback.
• For example, to skip the prompt and always restart automatically:
• ```lua
• require('lean').setup {
• on_imports_out_of_date = function(bufnr)
• require('lean.lsp').restart_file(bufnr)
• + 3 more

📦 Goal Diff Highlighting

• When Lean marks a goal as inserted or removed (via `diffInteractiveGoals`), the goal prefix (`⊢`) is now highlighted with `DiffAdd` or `DiffDelete` respectively.
• This matches the existing hypothesis-level diffing.

📦 Diagnostic Signs in the Sign Column

• When a diagnostic spans multiple lines, the sign column now shows guide characters marking the full range of the diagnostic rather than just its first line.
• This makes it easier to see exactly which code a diagnostic covers, especially for errors in multi-line definitions or tactic blocks.
• https://github.com/user-attachments/assets/d599ab77-5a97-4ab5-a973-b487d0c9ae74

📦 Infoview State Highlighting

• The infoview window's background now changes when attention is needed — it uses `leanInfoNCError` when the LSP is dead and `leanInfoNCWarn` when the infoview is paused.
• Both are customizable highlight groups.

📦 Interactive Hover

• Pressing `K` now opens an interactive hover popup where subexpressions are clickable — the same TUI system the infoview uses.
• Click on a type to see its own type, press `gd` to jump to its definition, and so on.
• The popup shows the full expression signature, the type rendered interactively, documentation, and import info.
• When the RPC session is unavailable it falls back to the standard `vim.lsp.buf.hover()`.
• This can be disabled via `lsp.enhanced_handlers.hover = false` if it interferes with another plugin.
• https://github.com/user-attachments/assets/0c62cb86-756e-4745-9ac6-83173415518f

📋 Other Changes

• Additional pins now display in their own split windows rather than being concatenated in the main infoview buffer
• https://github.com/user-attachments/assets/1890f6c4-3878-44ed-b522-36543264c273
• Infoview updates on cursor movement are now throttled — rapid scrolling (e.g. holding `j`/`k`) no longer floods the LSP with requests.
• Further performance improvements are coming
• Progress bar signs are now cleared when LSP clients stop, preventing stale signs from lingering
• Fractional `width`/`height` values are now supported for the infoview (e.g. `width = 1/3`), and are the new default
• Only syntax-highlight interpolation in `s!""` strings, not all strings
• Correct the root directory when editing files in `.lake/packages`
• + 2 more

📦 Contributors

• Thanks to everyone who contributed to this release:
• [@antinomie8](https://github.com/antinomie8) — syntax highlighting for `≠` and `^` as operators
• Benedict Christian Smit — lspconfig deprecation fix
• [@lucianchauvin](https://github.com/lucianchauvin) — fractional infoview dimensions
• [@scott7z](https://github.com/scott7z) — diagnostic and configuration fixes
• [@Vinh-CHUC](https://github.com/Vinh-CHUC) — documentation fix
• The [wiki manual](https://github.com/Julian/lean.nvim/wiki/The-lean.nvim-Manual) has also been updated to cover all of the above.
• Until next time Neovim friends.
• + 5 more

✨ New Contributors

• @Vinh-CHUC made their first contribution in https://github.com/Julian/lean.nvim/pull/448
• @scott7z made their first contribution in https://github.com/Julian/lean.nvim/pull/486
• @antinomie8 made their first contribution in https://github.com/Julian/lean.nvim/pull/495
• Full Changelog: https://github.com/Julian/lean.nvim/compare/v2025.10.1...v2026.4.1

📋 What's Changed

• fix goto_last_window by @funemy in https://github.com/Julian/lean.nvim/pull/373
• Remove some keywords in leanDeclaration by @stephen-huan in https://github.com/Julian/lean.nvim/pull/385
• Add `orientation` opt to force infoview orentation by @lucianchauvin in https://github.com/Julian/lean.nvim/pull/403
• Fix backslashes on multiline comments by @MithicSpirit in https://github.com/Julian/lean.nvim/pull/419

✨ New Contributors

• @funemy made their first contribution in https://github.com/Julian/lean.nvim/pull/373
• @stephen-huan made their first contribution in https://github.com/Julian/lean.nvim/pull/385
• @PatrickMassot made their first contribution in https://github.com/Julian/lean.nvim/pull/386
• @emmanuel-ferdman made their first contribution in https://github.com/Julian/lean.nvim/pull/397
• @lucianchauvin made their first contribution in https://github.com/Julian/lean.nvim/pull/403
• Full Changelog: https://github.com/Julian/lean.nvim/compare/v2024.12.2...v2025.10.1

📦 Telescope Picker for Abbreviations

• I've also added a telescope picker for inserting abbreviations, which you can activate via `:Telescope lean_abbreviations`.
• Here's how that looks:
• https://github.com/user-attachments/assets/fdfe4bc4-936f-4d25-b51f-e06cf74e972d
• Better dedenting autoindent behavior after some `sorry`s and `=>` (though there's still one case I know is wrong)
• The order of diagnostics and suggestions in the infoview has been flipped to match VSCode, with widgets now showing up first before diagnostics in the infoview.
• Until next time Neovim friends.
• ---
• You should be able to update using whatever plugin manager you're using, e.g. via `:Lazy update`.
• + 1 more

📋 Changes

• Return correct has_satellite by @adlerd in https://github.com/Julian/lean.nvim/pull/361
• fix(keymap): not shadow keymap desc so make blink.cmp happy by @tim3nd in https://github.com/Julian/lean.nvim/pull/367
• @adlerd made their first contribution in https://github.com/Julian/lean.nvim/pull/361
• @tim3nd made their first contribution in https://github.com/Julian/lean.nvim/pull/367

📋 Changes

• A default mapping was added for `:LeanRestartFile` (`<LocalLeader>r`). You of course are still free to map it to whatever you'd like if you prefer another mapping. Thanks to @utensil for the contribution!
• Communication with the LSP should be *slightly* more reliable because we now do a few more retrys when we get a failure, though it's here that I actually want to make my next set of improvements.
• The infoview contains less trailing whitespace. This is something you may not have noticed if you're not as bothered by it as I am, but occasionally we would render extra empty trailing lines, and now we don't :)

📦 Infoview View Options

• We now have configurable view options, a la VSCode.
• This means you can dynamically hide hypotheses which are instances, types, or inaccesible names in the infoview.
• You can also reverse the order of the goal state such that the goal is on top.
• Here's a quick GIF:
• 
• Some documentation for this configuration is [in the Manual](https://github.com/Julian/lean.nvim/wiki/The-lean.nvim-Manual#customizing-the-infoview), but here's the tl;dr:
• Please provide any feedback!
• Also... I'd love to hear if anyone has ideas for further filtering beyond these options!
• + 1 more

📋 Other Changes

• Did you know that the `conv` tactic uses a different prefix (`|`) for showing goals in the infoview? I didn't. But now `lean.nvim` properly shows that prefix instead.
• Version numbers, clearly. Going forward, `lean.nvim` will have "releases". This really doesn't affect you as a user, it's at the minute simply an excuse to write up release notes when `lean.nvim` gets something new + notable.
• `lean.nvim` is now [on `Luarocks`](https://luarocks.org/modules/Julian/lean.nvim). Unless you plan on interfacing with Lean via Lua, you probably don't care about this either.
• Full Changelog: https://github.com/Julian/lean.nvim/compare/v2024.9.1...v2024.9.2