v2024.12.2

Oh hello there. Another new release of lean.nvim is out, sneaking in just before 2025 🎊 📆.
It contains some additional autoindent fixes and better widget behavior for try this widgets.

Clickable Suggestions

Patrick Massot pointed out that in VSCode, when you see suggestions via e.g. the apply?, exact?, rw? tactics, that clicking in the infoview will perform the replacement.
Now this happens in nvim as well -- if you click on a suggestion, you should see the contents of your Lean source change.
Here's a quick demo if you haven't seen this feature before:

output.mp4

Note that "click" here has the same keybinding as other "clicking" operations in the infoview -- namely <CR> or K.

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:

telescope.mp4

This isn't a good replacement for \-based abbreviation entering -- not least of which because telescope has a bug that means that after inserting an abbreviation you end up in normal mode. But it's something we'd discussed previously as being cute if only to be able to dynamically see the list of abbreviations (and preview what they'll expand to), and can be improved upon slightly.

Other Changes

• Better dedenting autoindent behavior after some sorrys 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.

I'd still love to hear any feedback on how well (or not well) autoindent is working for anyone, but I hope that the silence there is either everything working well or better everyone enjoying their holidays.

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.12.1...v2024.12.2

v2024.12.1

Oh hello there. Another new release of lean.nvim is out! 🕎 🎄
By popular request, this one brings initial support for... autoindenting.

Autoindent

This hopefully should be self explanatory.
When you hit enter in places, or use other normal mode commands for creating lines like o, you should see the cursor automatically be indented in places which are stylistically expected.
Similarly, using the = operator should indent code (e.g. gg=G indents all lines in the buffer, which I've used to test that many but not all files in Mathlib will no-op when run through lean.nvim's autoindent support).
Note of course that given that Lean is whitespace sensitive that this = indentation is by nature "impossible" to do unambiguously for all cases, but it should do some right things some of the time.

I'm calling this alpha level, as there certainly are (even known) cases which can be improved and it's very possible that there are still some significant issues to work out, but it's at a state where I'd like more feedback and I've been using it a bit the past few weeks.
Please report any things you wish were indented, or things you wish weren't, as I've done a bit more than was originally requested here which can be both good or bad; in particular what good autoindentation feels like I find to often be slightly subjective and slightly hard to make precise -- so feedback as usual is welcome.

(n.b. you'll find that I've implemented at least one case of autodedenting, specifically when you type sorry you'll find yourself automatically dedented. There's more we could do there, e.g. we could make use of goal states to decide whether to dedent automatically, but I chose for now to get a first version out even though I've played a bit with fancier logic for dedenting, especially given that if you don't like any of this behavior I'd be happy to make it configurable to turn off.)

Turning it off

If for whatever reason you notice undesirable indent behavior, let me know, but you also can completely disable the behavior by creating the file ~/.config/nvim/indent/lean.lua and having it contain:

vim.b.did_ident = true

which tells Neovim that this (empty) file is the indent rules for Lean.

Other Changes

• Return correct has_satellite by @adlerd in #361
• fix(keymap): not shadow keymap desc so make blink.cmp happy by @tim3nd in #367

New Contributors

• @adlerd made their first contribution in #361
• @tim3nd made their first contribution in #367

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.10.1...v2024.12.1

v2024.10.1

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

v2024.9.2

Oh hello there.

A new release of lean.nvim is out. You should be able to update to it in whatever plugin manager you're using, e.g. via :Lazy update.

There's one 'big' feature and some small tweaks.
The bigger one is...

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, but here's the tl;dr:

A new <LocalLeader>v mapping is now enabled within Lean files. It opens a window where you can hit <Tab> on each line to toggle the setting you're on top of. Hit <Enter> when you're done to confirm your choices, or hit K if you want a hover showing you more information about the setting.

Please provide any feedback!

Also... I'd love to hear if anyone has ideas for further filtering beyond these options!
Now's a good time for me to implement any such ideas, and I know the VSCode functionality hasn't really changed since it was introduced, so perhaps if you deal with proofs with lots of hypotheses often, you have suggestions for other things we could configurably filter!
Feel free to post them!

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. Unless you plan on interfacing with Lean via Lua, you probably don't care about this either.

Full Changelog: v2024.9.1...v2024.9.2