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 :+1: to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add :+1: 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?