VSCode indentation

Stream: lean4

[Patrick Massot]

Since we are discussing VSCode improvements, I would really love to see work on auto-indentation. It would be really nice if VSCode could automatically insert correct indentation after a focusing center dot. I see many students writing

constructor
· intro x
exact...

thinking exact ... is continuing the proof started by intro x, and getting very confused by Lean being very confused. The crucial point is that hitting the Return key at the end of the · intro x line does not put the cursor in the correct position.

[Marc Huisinga]

This should be possible with the right onEnterRules setting in the language configuration.

[Thomas Murrills]

Would it be helpful if I started a PR to the extension with some rules for indentation on enter? This seems pretty straightforward, and I've got this rule working (and, unrelatedly, have wanted a chance to get used to the extension development workflow for other reasons) :)

[Thomas Murrills]

The basic version (focus blocks only) is now at vscode-lean4#328. I'm exploring indentation after certain tokens like by, do etc. in the draft PR vscode-lean4#329.

[Thomas Murrills]

However, I'm not sure when we would want to use onEnterRules, and when we would want to use indentationRules. The documentation seems to describe an overlapping use case with onEnterRules, but says it also applies to "when you type, paste, and move lines". It doesn't detail what exactly the consequences of a line matching an increaseIndentPattern are. Some googling suggests it also needs a decreaseIndentPattern, which often isn't uniformly definable in lean.

[Thomas Murrills]

Also, I was wondering—can indentation-on-enter be performed in a language-aware way instead of using regexes? It seems like it'd be much better to indent in a manner based on full knowledge of the parsed syntax and infotree instead of just relying on hardcoded, fragile regexes! :) I did some googling but couldn't find anything.

[Eric Wieser]

I would guess it has to be regex based for performance

[Thomas Murrills]

Ah, that makes sense—you don't want to hit enter and then have to wait for elaboration to finish before your keystroke has an effect.

[Sebastian Ullrich]

Waiting just for parsing though could be very reasonable! Which however the server architecture does not support yet We already do some parsing-only tasks, this may or may not be a good fit as well

[Sky Wilshaw]

I think the LaTeX workshop extension does something comparable, I think it sometimes tries to format the line I'm on once I press enter, and it takes about a second to process.

[Marc Huisinga]

Thomas Murrills said:

However, I'm not sure when we would want to use onEnterRules, and when we would want to use indentationRules. The documentation seems to describe an overlapping use case with onEnterRules, but says it also applies to "when you type, paste, and move lines". It doesn't detail what exactly the consequences of a line matching an increaseIndentPattern are. Some googling suggests it also needs a decreaseIndentPattern, which often isn't uniformly definable in lean.

onEnterRules seems to be preferable.

Thomas Murrills said:

Also, I was wondering—can indentation-on-enter be performed in a language-aware way instead of using regexes? It seems like it'd be much better to indent in a manner based on full knowledge of the parsed syntax and infotree instead of just relying on hardcoded, fragile regexes! :) I did some googling but couldn't find anything.

You can do this using the LSP textDocument/onTypeFormatting request, but NeoVim doesn't support it and Emacs' implementation seems to be somewhat broken. So even disregarding the added latency, it may not be a good idea to use it instead of onEnterRules.