Can code actions output message data to the infoview?

Stream: lean4

[Matthew Ballard]

Is this possible? I thought asking would be quicker than picking through the code.

[Matthew Ballard]

Eg: for simp?, I want to be able to jump to the suggested simp theorems

[Eric Wieser]

simp? outputs a widget, and then I think the widget provides the code-action?

[Eric Wieser]

I think the widget could certainly behave as you describe, but then the UX would need to change, as clicking the theorem name currently applies the suggestion

[Matthew Ballard]

Ah you are right. I conflated steps.

[Matthew Ballard]

Eric Wieser said:

I think the widget could certainly behave as you describe, but then the UX would need to change, as clicking the theorem name currently applies the suggestion

This is me living in nvim land

[Julian Berman]

Something does seem inconsistent but I'm not sure why/whose fault it is without doing a bit of digging (maybe later).

But e.g. (in neovim):

import Mathlib.Algebra.Group.Defs

variable (G : Type) [Group G] (a b c : G)

example {h : P ↔ Q} : Q ↔ P := by
  exact?

example : a * a⁻¹ * 1 * b = b * c * c⁻¹ := by
  simp?

The infoview for exact? will jump to Iff.symm if you gd on it.

But the infoview will not do that with e.g. mul_right_inv in the simp call.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Eric Wieser said:

simp? outputs a widget, and then I think the widget provides the code-action?

Code actions and widgets are entirely separate; you can have a widget which contains a link such as "Try this: some_tac" which inserts that tactic when clicked, but that is not a code action. Code actions are built into LSP, and editors have native support for executing them (e.g. with the lightbulb popup in VSCode). As an implementer, you use savePanelWidgetInfo for the former, and a globally registered @[hole/tactic/command_code_action] for the latter.