std4#231, and code actions

Stream: std4

[Scott Morrison]

Some questions about code actions.

• Is there a mechanism (whether generic or Lean specific) to run all code actions in a file? Or all code actions of a specified kind??
• What if I wanted to run all code actions across many files (ideally able to do this from the command line / a script)?

[Scott Morrison]

(I'm thinking here that there are some things which are useful both as user prompts and library-wide edit tools, and hoping that one can just implement these as code actions.)

[Mario Carneiro]

No, not really. We would need another interface for that, a framework for plugging in to a "do all the things" edit API

[Mario Carneiro]

What would the front end of such an API be? Something like cargo --fix, or a custom command in vscode?

[Mario Carneiro]

The way I would describe cargo --fix in lean terms is that compilation can produce diagnostics (warnings and errors) that are change requests tagged as "machine-applicable", and then --fix collects all of these by running lean in a special mode where it outputs these diagnostics in JSON format and then follows up with a global file edit which applies all machine-applicable diagnostic change suggestions.

[Scott Morrison]

Oh, I was imagining instead some tool that collected all the change requests via the LSP (hence wondering if there might be something generic for all langauges).

[Scott Morrison]

But a quick google finds nothing, which is a pity.

[Mario Carneiro]

The LSP interface (which is reflected in the lean interface) is that the client asks about what code actions exist at a given location or selection, the server responds with a list of suggestions, then the client picks one and the server sends a text edit

[Mario Carneiro]

so if you wanted to use the LSP interface directly you would (1) have to ask at each character and (2) identify and filter out duplicate suggestions, which would be very inefficient

[Mario Carneiro]

It is probably possible to come up with a combined interface which is usable for both workflows though, so that the code actions can share code with the autofix