RFC: linters should be able to use try this

[eric-wieser]

Proposal

It should be possible for linters to use Meta.Tactic.TryThis.addSuggestion and friends to add "Try this:" suggestions

Often, a linter can not only identify the problem, but also suggest a fix.
It would be very convenient in these cases to apply the fix with a single click, and not have to write a separate code action.
Some examples include

• Deprecations: the suggestion can substitute the new function
• Unused arguments: the suggestion can delete the argument
• Syntax transformations to remove antipatterns.

Currently, when addSuggestion is used, the suggestion appears in the info view, but only as a log message and not as a widget.

An outline of how this might look:

• runLinters should preserve infoState (and traceState for good measure?)
• ContextInfo.runMetaM should do the same (as linters may need this to run elaborators from the info tree)
• A top level info tree node needs to be created for linters, to avoid a panic from Lean.Elab.InfoTree.visitM; or linters need to be very conservative about accidentally creating other infotree nodes.

Community Feedback

Zulip conversation

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

[kmill]

Something that would improve this RFC is a concrete example or two of the impact of this on this from a user's point of view. What's a piece of user code that would trigger a linter, and what kind of 'try this' suggestion would it give?

[vlad902]

Concrete example: Writing a Linter to automatically generalize type classes in theorem decls, and I can no longer add the suggestion for the correct type class for the user to easily click on, and have to print a message instead.

[nomeata]

Does #4254 help here? It seems it allows embedding widgets into messages. Also see #4551 (comment).

So maybe it’s possible to include a try-this-like widget in arbitrary MessageData already?

(Although it doesn't seem to be unreasonable to expect widgets as they exist now to work.)

[nomeata]

I just wrote a linter that uses suggestions in message data, and it seems to work, using the MessageData.hint framework, so there is a clickable link and it works (but no code action, which is probably unrelated to this.)