feat: CodeActionProvider

[EdAyers]

trafficstars

This is a low-level system for registering LSP code actions. LSP code actions are editor integrated code actions. In VScode, you can trigger the textDocument/codeAction handler by hitting Ctrl+. (Cmd+. on macs). If a code action is of the kind "quickfix" this will also cause a little lightbulb to appear next to the cursor.

Rather than having a hard-coded handler, users can register their own code actions by creating a CodeActionProvider : CodeActionParams → RequestM (RequestTask (Array CodeAction)) and registering with the @[codeActionProvider] attribute. In future commits I am going to add features on top of this. In particular I have implemented a special TacticSuggestion with some infoview compatibility so users can see the tactic state after the suggestion is applied.

This interface can be used to implement the following applications:

• refactoring code: adding underscores to unused variables,
• suggesting imports
• document-level refactoring: removing unused imports, sorting imports, formatting.
• Helper suggestions for working with type holes (_)
• Helper suggestions for tactics.

Related issue: https://github.com/leanprover/lean4/issues/1494

[gebner]

Rather than having a hard-coded handler, users can register their own code actions

I think it is a good approach to make the codeAction extensible in this way, and we should do the same with all the other requests as well.

But I don't think we should corral users into writing low-level handlers for every code action. I think you're already planning to do this based on the TacticSuggestion reference. The documentation should reflect this, and make clear that this is a low-level API and users should not use it directly.

[Kha]

My suggestion would be: keep the current LazyCodeAction API, but implement it using (2) for now.

SGTM