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 = truewhich 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
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
