Lean4 code snippets

[dalps]

These are some code snippets I defined to help me write Lean code, following the example of the ocaml-platform extension.

From VS Code user guide's article on snippets:

Code snippets are templates that make it easier to enter repeating code patterns, such as loops or conditional-statements.

I think the Lean programming experience on VS Code could really benefit from some of these snippets.

[mhuisi]

One huge issue with snippets is that they always pop up in the VS Code auto-completion menu and so users trigger them by accident all the time while typing when hitting enter, which is extremely annoying. This is why we prefer to use code actions for snippets, why we are relatively careful not to provide completion items in the language server when users are likely to hit enter (e.g. on keywords) and why Mathlib has even decided to disable enter for auto-completions entirely (though we are looking to revert this in the future).
Snippets also clutter the completion menu when you are using auto-completion for discovery, not just for reducing the typing overhead.

You can find some prior discussion here and here.

If vscode-lean4 is to provide auto-completion code snippets, it must be configurable with a setting and be disabled by default.

[dalps]

If I can add my two cents, as an OCamler starting out with Lean, I'm used to ocaml-platform showing me a list of modules and functions from the stdlib or the packages I included in my dune project matching the letter I just typed; this happens wherever my cursor happens to be in an .ml file. I'm really missing this kind of assistance from the Lean extension.

In a Lean file, most of the time I type something I get a list of irrelevant workspace suggestions (those with the 'abc' icon), which I think is more annoying than accepting relevant suggestions by mistake on enter.

Hence these snippets, to fill that void when the Lean extension has nothing better to show.

[mhuisi]

In a Lean file, most of the time I type something I get a list of irrelevant workspace suggestions (those with the 'abc' icon), which I think is more annoying than accepting relevant suggestions by mistake on enter.

These are provided by VS Code, not vscode-lean4. You can disable them using the 'Editor: Word Based Suggestions' VS Code setting. We've considered disabling those language-wide in the past, but it turns out that some users do like word based suggestions, and VS Code makes it very difficult to change language-defaults, so we've decided against it for now.

If you are experiencing failures of auto-completion, please report those in the Lean 4 repository. The Lean language server currently provides identifier auto-completions for the import closure of the file you are working on. I'd estimate that we will have auto-completion for identifiers in the full project regardless of import closure within the next six months.

[dalps]

Thank you, I've followed your advice and disabled word-based suggestions for Lean files, that helps.

After reading the vscode-lean4 manual on auto-completion, I realized my instance of the extension is indeed behaving correctly; also I didn't know that some snippets were already available through code actions.

I'd be happy to see the kind of snippet I proposed integrated in vscode-lean4 one day, or even keyword suggestions. But I agree that they should be done in a context-sensitive and configurable way. Until that becomes feasible, feel free to close this PR.

[mhuisi]

Alright, I'll close this PR. Thanks for the suggestions regardless, there's definitely lots that still needs to be improved about the Lean editing experience :-)