Command elab starting a tactic proof

Stream: lean4

[Patrick Massot]

I have trouble writing a macro that prepend a tactic sequence with some tactic. The goal is to hide a call to docs#ProofWidgets.withPanelWidgets.

import ProofWidgets.Component.Panel.SelectionPanel

open ProofWidgets

-- The following example, copied from the ProofWidget demo folder, works
example (h : 2 + 2 = 5) : 2 + 2 = 4 := by
  with_panel_widgets [SelectionPanel]
  -- See a widget here :-)
  rfl

section
open Lean Meta Elab Command

open Lean.Parser.Term (bracketedBinder)

elab "exercise : " concl:term "Proof:" prf:tacticSeq : command => do
elabCommand (← `(command|example : $concl := by
      with_panel_widgets [SelectionPanel]
      $prf))
end


exercise : True
Proof:
  -- No widget here :-(
  trivial


exercise : True
Proof:
  with_panel_widgets [SelectionPanel]
  -- See a widget here
  trivial

[Anand Rao Tadipatri]

This could be because the Syntax of the command is not "canonical" (as explained in the docstring here: https://github.com/leanprover-community/ProofWidgets4/blob/main/ProofWidgets/Demos/Macro.lean). However, I found that writing

macro "exercise : " concl:term "Proof:" prf:tacticSeq : command => do
  Lean.TSyntax.mkInfoCanonical <$>
    `(command|example : $concl := by
      with_panel_widgets [SelectionPanel]
      $prf)

does not work either, so the issue could be something deeper.

[Patrick Massot]

Oh, I would have never suspected that. @Wojciech Nawrocki any idea?

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

I cannot investigate at the moment but an issue with whether the info is canonical is likely. The adapted macro may be failing because it's the whole example syntax that is set to have canonical info, but one needs the syntax to which the widget span is associated to be canonical iirc.

[Anand Rao Tadipatri]

Indeed, it seems to work with that modification:

macro "exercise : " concl:term "Proof:" prf:tacticSeq : command => do
  let tac : TSyntax `tactic ←
    Lean.TSyntax.mkInfoCanonical <$>
      `(tactic| with_panel_widgets [SelectionPanel]
                  $prf)
  `(command|example : $concl := by { $tac })
end

[Patrick Massot]

Great! Thank you very much @Anand Rao Tadipatri. The timing is also very good. I'm done with my grading work and was about to get some lunch and then resume trying to get this working.