RFC: Code actions

Hi I've collected some thoughts on how to proceed with making a good code completions / actions interface for Lean:

Scope

This RFC intends to cover an API for the protocol between Lean and an editor (initially vscode-lean4) for handling code actions. By code action, I mean the process of Lean presenting suggested semantic code changes to the user via the editor or infoview interface. Examples are (source):

• Suggested expressions to fill _ holes with
• More advanced suggestions with {! ... !}-style holes as described by @david-christiansen here.
• Suggestions to fix syntax errors and elaboration errors.
• From the infoview; contextual suggestions where the user clicks on a certain part of the goal state in the infoview, causing the tactic state to update. Examples are clicking on a subexpression in the infoview and generating a conv at or suggesting potential rewrite rules for a particular position.
• Replace a tactic by another tactic. For example: squeeze_simp [...].
• Insert a tactic. For example: library_search.
• Replace an expression by another expression. For example: by show_term { exact ... }.
• Insert an expression. For example: insert structure instance stub, by library_search.
• Replace (non-expression) syntax by another syntax. For example: unfold macro.

Out of scope: code formatting, snippets.

Existing work and discussion

• LSP code actions,
• CodeActionProvider in VSCode extension API
• Lean 3 VSCode extension: Hole support, "Try this" feature.
• Previous discussions: https://github.com/leanprover/vscode-lean4/issues/45, https://github.com/leanprover/lean4/issues/1223
• @kasequark (Robin Bohne ) is working on a Conv-zoom command.

Summary of existing discussion

• It's important that CPU-intensive suggestions for code actions (eg finding rewrites, calling a hammer) are only triggered upon a user action explicitly for suggesting code actions.
• There is a worry that there will be cases where there are too many suggestions, in particular for unbounded cases where you are suggesting potential terms to fill a hole or lemmas to close a goal.
• @david-christiansen notes that there is some potential to include the more innovative Agda-style holes.
• @digama0 was sceptical about {! !} holes at least in terms of notation and calls for a retrospective. Leo says this is because it was underdeveloped
• @Kha likes the snippets in rust-analyser, where you get the action using a snippet-style workflow when you type match. @gebner is less keen.

Design proposal

Available mechanisms for implemention of code actions

• The LSP Code Actions system. That is, the 'lightbulbs'.
• The LSP completions system. That is, they appear in the 'intellisense' completion tooltip.
• A custom API, eg something like the contextual suggestions RPC. The Lean server then modifies the source document directly.
• When a tactic is elaborated, they can dump a user-widget to the infotree. Users can interact with this custom UI and eventualy cause a call an RPC method that the Lean server runs.

I think there are cases where you want to use all of the above. I think the code actions give the best solution to the hinting/replacing style tactics such as squeeze_simp. The right way to implement these I think is to get the tactic to emit a code action diagnostic that is stored on the infotree. A similar approach can be used when holes are elaborated. In addition to the editor-specific code actions menu, these actions could also be presented in the infoview to make them more promenant.

The difference between completions and code actions seems to be that code actions are present as solutions to diagnostics ('squigglies'), whereas completions appear as you type new code. These completions can make arbitrary text edits, so we can do things like get match x with to suggest a completion where it autofills all of the cases. I think the rule should be that if you are inserting a new command such as while typing a term or a tactic script, it should give completions, otherwise if it is replacing it should use code actions.

Modifying the document.

Currently, tactics can also put a user-widget on the infotree. User-widgets are able to send a command to the editor requesting a text edit, but it is currently clunky and isn't syntax aware.

I think that the best approach here is for Lean to provide a function diff : Syntax → Syntax → TextEdit or something similar, where the first argument is the existing syntax (stored on the infotree) and the second argument is the new syntax, the TextEdit object is then sent to the client editor. This is better than the Lean server editing the file directly because the resulting edit will not appear in the user's undo stack, and there may be some complications with buffers getting out of sync with the file on disk.

In the case of code actions and code completions, I propose that the TextEdit is computed at elaboration time, rather than asynchronously. This is acceptable because code actions that might take a long time to compute (like squeeze_simp) will be explicitly invoked by the user.

By storing these completions on the infotree at elaboration time, we don't have to decide here on an API for working with holes or deciding exactly which completions should be supported for a different PR. If we want any custom UI for working with holes, they can use the user-widget system.

Changes proposed:

• Introduce a new InfoTree object called CodeActionInfo. Interactive tactics such as squeeze_simp will put one of these on the infotree.
• Implement textDocument/codeAction LSP request.
• Add support to CompletionInfo for sending TextEdit objects.
• Write a diff : Syntax → Syntax → TextEdit function to generate LSP text edits from a syntax change.
• Write a Lean → client RPC call commanding a TextEdit, this can then be used by the infoview ( calls from contextual suggestions and user-widgets) to control the editor.

Start with the linked LSP code-action and completion specifications, then inspect the existing InfoTree, CompletionInfo, user-widget mechanisms, and the Lean 3 extension's src/holes.ts reference. The proposed work spans CodeActionInfo, textDocument/codeAction, TextEdit diffing, and a Lean-to-client RPC; done means the unchecked design items are implemented and their editor interactions are validated.