code actions in linters

Stream: general

[Thomas Murrills]

Mario Carneiro said:

The point of a linter is to suggest a modification which it thinks is better. (Ideally with a code action to perform it.)

Can you actually add a code action through a linter? My impression was that the major route for adding a code action at a specific spot was by pushing something onto the infotree—but docs#Lean.Elab.Command.runLinters obliterates changes to the info state after running each linter, preserving only the messages. Is there a back door somehow?

[Notification Bot]

A message was moved here from #general > pointless tactic linter by Thomas Murrills.

[Damiano Testa]

For what it's worth, I have tried a bit to get a Try this suggestion, I could register it, but was unable to make it trigger a code action.

[Matthew Ballard]

Can this be done with Std linters instead?

[Mario Carneiro]

src#Std.CodeAction.deprecatedCodeActionProvider is an example of a code action that triggers on a message, not something in the info tree. But the code action will otherwise be recomputing the result that the linter produced, using the linter message only as a filter

[Thomas Murrills]

I wonder what the right design for a standard way to add suggestions from a linter would be.

It would be nice to just call addSuggestion or a simple variant, but I’m guessing we want to call each linter with a fresh info state. One way of handling this would be to manually distinguish infotrees added by the linter by some token or other, and have runLinters accumulate those trees before resetting the state (and finally push them all onto the info state at the end).

Another would be to support only very limited try-this suggestions that can be gleaned from the structure of message data in messages. This at least wouldn’t require a core change, but would be limited and possibly fragile.

But maybe there are better designs out there?