RFC: Code actions

[EdAyers]

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: Code actions, to "fill holes" with suggestions from Lean Language Server vscode-lean4#45, RFC: Contextual suggestions #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.

[gebner]

The difference between completions and code actions seems to be that code actions are present as solutions to diagnostics ('squigglies'),

This is not accurate. Code actions are not usually not related to a diagnostic. There's a separate request to fetch code actions.

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.

The infoview already has a function to insert text in the editor. We can and should probably upgrade that to TextEdits though.

Introduce a new InfoTree object called CodeActionInfo.

I think this is a good starting point, and will immediately address existing uses like library_search or squeeze_simp.

I still think we need lazily evaluated actions though (later on). Actions like "expand macro" or "add type to let" apply to a lot of code, are too expensive to compute eagerly, and are not produced by the elaborator itself.

[ReiniervdG]

With respect to existing suggestions like squeeze_simp, you still have to know they exist before you're able to use them. Does it make sense to allow squeeze_simp explicitly to always show the suggestion, but additionally allow to overload simp to give such suggestions when some 'suggestion option' is turned on?

Expensive suggestions may be implemented as a 'suggestion of suggestions', e.g., whenever you run a simp, you get a suggestion it may be useful to squeeze_simp and replace, only executing after you click that suggestion.

[digama0]

I would expect squeeze_simp to continue to work roughly the way it does now: when you run it it produces an info diagnostic (so you can't miss it) which contains a button that triggers the replacement action. simp on the other hand can have a code action "squeeze this simp" that, when selected, runs squeeze_simp under the hood to find the replacement and then just goes ahead and does it (so the user would not explicitly need to write squeeze_simp in this case).

[siddhartha-gadgil]

It would be useful if asynchronous processing is possible, say via the CodeActionInfo. For more complex automation, translation etc it would be useful to keep working in the background (using Task or something built on it) and updating with successively better answers.

[Kha]

By the way, I just took a quick look at how one of the better language servers implements code transformations: synthesis seems to be string-based https://github.com/rust-lang/rust-analyzer/pull/13005/files. Not sure if there is a chance of lost comments from the transformation.

[gebner]

Typescript does AST modification:

• Example code action: https://github.com/microsoft/TypeScript/blob/7910c509c4545517489d6264571bb6c05248fb4a/src/services/codefixes/addMissingAsync.ts#L48-L62
• Some high level docs: https://github.com/microsoft/TypeScript/wiki/Codebase-Services-TextChanges

[Kha]

Ah, this is the kind of hacky adjustment I would like to avoid by reformatting the whole declaration instead of just the synthesized text: https://github.com/microsoft/TypeScript/blob/db9e0079/src/services/textChanges.ts#L1048-L1049