Oh hello there. Another new release of lean.nvim is out! There are a few nice features included, as well as a nice announcement you should stick around until the end for :)
Here's what we have coming out of the oven:
Goal State Diffing
When the goal state changes in your proof, or as you introduce new hypotheses, Lean sends little hints saying which parts of your goal have changed.
These can be subtle (I didn't even notice them myself until they were pointed out) but they're very helpful for watching your proof state change.
lean.nvim now supports showing them as well:
goaldiff.mp4
The precise colors you see will depend on your color scheme, but the defaults should be good enough, as they're tied to the colors you should already see in other "diff" contexts.
If that isn't the case, please feel free to share your setup.
Diagnostic Widgets
lean.nvim previously supported interacting with hypotheses in the infoview (e.g. allowing you to click on a term you see and to see its type).
But now it properly renders some widgets within diagnostics, which are sometimes used by commands you may already be familiar with.
As a concrete example, here's what you should now see with the #find_home command:
diagnosticwidgets.mp4
(Note that in the screencast I'm hitting gd to jump to definition -- this is because the widget coming from #find_home is specifically one meant for jumping to a corresponding Lean module being shown).
Mapping Documentation
Neovim key mappings can be "self-documenting", in that when you run e.g. :map <LocalLeader>\\ they can tell you not only that this is mapped to some command or Lua function, but also some documentation about what the mapping does.
lean.nvim now sets this property for all mappings it creates.
In this particular case then, you'll now see:
n <Space><Space>\ *<Cmd>LeanAbbreviationsReverseLookup<CR>
Show how to type the unicode character under the cursor.
where the second line is new.
Similar short descriptions are present for all of what lean.nvim binds both in Lean files as well as the infoview.
Those of you who use which-key.nvim (which actually doesn't include me :) should now see something other than a blank spot in your popovers, as it's this same property which is used to generate the text there.
FRO Sponsorship 🎉 🎉 🎉
I am really happy to be able to share that the Lean FRO has decided to sponsor me working on lean.nvim part-time for a short period.
Sincere thanks are definitely owed (to Leo, Sebastian and many others in the FRO!)
And of course some of the existing work these last 2 weeks already is a direct outcome.
While I feel like I have some decent sense of missing functionality that could be worked on in the coming weeks, please do take this as an official solicitation to share pain points and gaps.
I'll shortly share the list I have which I'm using to prioritize what to do next, but this list is malleable and definitely could use you (yes you!) throwing ideas in the hat to help me reorder priorities.
I'd like to sincerely thank all of you who use it for showing how much interest there is!
Undoubtedly it was instrumental in making this specific sponsorship happen, and bodes well for Neovim and Lean being long term friends.
Other 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 :)
Until next time Neovim friends.
You should be able to update using whatever plugin manager you're using, e.g. via :Lazy update.
Full Changelog: v2024.9.2...v2024.10.1
