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
convtactic uses a different prefix (|) for showing goals in the infoview? I didn't. But nowlean.nvimproperly shows that prefix instead. - Version numbers, clearly. Going forward,
lean.nvimwill have "releases". This really doesn't affect you as a user, it's at the minute simply an excuse to write up release notes whenlean.nvimgets something new + notable. lean.nvimis now onLuarocks. 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