RFC: linters should be able to use try this

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.

Start by reading runLinters, ContextInfo.runMetaM, and Lean.Elab.InfoTree.visitM, then compare their handling of infoState and traceState with Meta.Tactic.TryThis.addSuggestion. The work is complete when linter suggestions can appear as clickable “Try this:” widgets without causing info-tree panics.