Select and insert widgets

Stream: mathlib4

[Patrick Massot]

I just opened the work in progress PR #7260. This is the long overdue PR bringing the conv?, congrm?, gcongr and calc widgets. More generally it provides a framework to easily build such widgets where users click on some sub-expressions and get links that generate bits of tactic scripts. It is currently blocked by https://github.com/EdAyers/ProofWidgets4/issues/26 and, more seriously, it will require a lot of review work by @Wojciech Nawrocki that will probably happen at least partly in the real world. But I already encourage users to play with this branch and give feedback from a user perspective. The example widgets are meant as minimal versions, especially for the calc widgets, but I could already implement small improvements or bug fixes. @Heather Macbeth

[Patrick Massot]

@Sebastian Ullrich I'm also interested in your opinion about the way this PR redefines calc to hook up the calc widget. Is this the way to go? Or should the core calc tactic somehow provide hooks that would allow to build the same functionality without the corresponding code duplication? Note that duplicated code is already out of sync with core master since Mathlib uses a version of core that has neither https://github.com/leanprover/lean4/commit/3e755dc0e199b40367a8ec9a592a343108a71c5a nor https://github.com/leanprover/lean4/commit/0a59fd96a5189e92bfb7e9d58396d8bb6a9d1d8e.

[Sebastian Ullrich]

Good question. It looks like all you're collecting for the widget is syntax, is that right? Wouldn't it be easier then to do that separately and then simply call the core elaborator?

[Patrick Massot]

I just recorded widgets.gif to show what this PR is about.

[Patrick Massot]

Sebastian Ullrich said:

Good question. It looks like all you're collecting for the widget is syntax, is that right? Wouldn't it be easier then to do that separately and then simply call the core elaborator?

I'm collecting only syntax but I'm also calling savePanelWidgetInfo which somehow records information about the goal.

[Sebastian Ullrich]

It probably does that later on from the info tree, so I believe you could call it strictly before or after running the core calc elaborator

[Sebastian Ullrich]

I'm somewhat guessing here though

[Sebastian Ullrich]

By the way, the fact that you have to construct that JSON yourself instead of relying on ToJson seems like a weakness in the API to me

[Patrick Massot]

I originally had a dedicated structure with a deriving ToJson for only one use but it felt silly.

[Patrick Massot]

Using the json% macro seemed to be a nice alternative. The open scope isn't nice but it will soon become unnecessary (we are waiting for #7258).

[Patrick Massot]

I don't really see how to implement that idea of " call it strictly before or after running the core calc elaborator" but Wojciech probably will.

[Patrick Massot]

Sebastian Ullrich said:

By the way, the fact that you have to construct that JSON yourself instead of relying on ToJson seems like a weakness in the API to me

Maybe I misunderstood. Do you mean the API of ProofWidgets.savePanelWidgetInfo?

[Sebastian Ullrich]

Yes, since you are already passing it the type name anyway. It feels like there should be a more strongly typed API possible here. I understand that SelectInsertParams contains more fields than just the params but maybe that could be split somehow

[Sebastian Ullrich]

Patrick Massot said:

I don't really see how to implement that idea of " call it strictly before or after running the core calc elaborator" but Wojciech probably will.

"Running" here really just means call core evalCal as a regular function after doing your savePanelWidgetInfo calls

[Patrick Massot]

But savePanelWidgetInfo is called for each calc line, not only once for the whole calc tactic.

[Patrick Massot]

Sebastian Ullrich said:

Yes, since you are already passing it the type name anyway. It feels like there should be a more strongly typed API possible here. I understand that SelectInsertParams contains more fields than just the params but maybe that could be split somehow

This somehow bumps into https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Inheritance.20question again.

[Sebastian Ullrich]

Patrick Massot said:

But savePanelWidgetInfo is called for each calc line, not only once for the whole calc tactic.

Yes, you still need to walk through the syntax. But that's only a small part of the elaborator copied, isn't it?

[Patrick Massot]

Maybe I understood your suggestion. Do you mean https://github.com/leanprover-community/mathlib4/commit/180da0d94cf6bbf674c9c84331c1d394be75d55a?

[Sebastian Ullrich]

Ah yes, that works too (assuming it works). But I believe you can still be more radical and also remove most code in the elab_rules by calling evalCalc stx there instead

[Patrick Massot]

Sebastian Ullrich said:

that works too (assuming it works) := by tauto

Indeed it seems to work.

[Patrick Massot]

I tried the more radical

/-- Elaborator for the `calc` tactic mode variant with widgets. -/
elab_rules : tactic
| `(tactic|(calc%$calcstx $stx)%$full) => do
  let steps : TSyntax ``calcSteps := ⟨stx⟩
  let some calcRange := (← getFileMap).rangeOfStx? calcstx | unreachable!
  let indent := calcRange.start.character
  let mut isFirst := true
  for step in ← Lean.Elab.Term.getCalcSteps' steps do
    let some replaceRange := (← getFileMap).rangeOfStx? step | unreachable!
    let `(calcStep| $(_) := $proofTerm) := step | unreachable!
    let json := open scoped ProofWidgets.Json in json% {"replaceRange": $(replaceRange),
                                                        "isFirst": $(isFirst),
                                                        "indent": $(indent)}
    ProofWidgets.savePanelWidgetInfo proofTerm `CalcPanel (pure json)
    isFirst := false
  evalCalc full

but my widgets are gone.

[Heather Macbeth]

@Patrick Massot I'm really excited for this! Can't wait to try it!

[Patrick Massot]

You don't have to wait, you can fetch this branch and download the oleans (actually the oleans are not even necessary since no file import those tactics so old oleans would be good enough).

[Patrick Massot]

With the latest bump of the ProofWidget library, #7260 now pleases the linters and can be reviewed.

[Patrick Massot]

Patrick Massot said:

I just recorded widgets.gif to show what this PR is about.

This is now live in mathlib. Feel free to try and suggest improvements. Note also that a lot of this PR was about building a framework to make such widgets easy to build. So if you have any idea of a widget where you select stuff in the infoview and insert a tactic call then feel free to work on it (I have ideas if you want to play).