using a widget proof state

Stream: general

[Moritz Firsching]

For @David Renshaw's great chess implementation, I added a widget to render the chess position a little bit more pretty: https://github.com/dwrensha/animate-lean-proofs/pull/4

Now we are wondering: is it possible to use that widget directly in the proof state? Are there good examples of widgets that do that somehow?
I can only find lean3 examples and no good lean4 examples of the usage of widgets.

[Anand Rao Tadipatri]

Have you already looked into docs#Lean.Widget.savePanelWidgetInfo or with_panel_widgets? This demo in the ProofWidgets repository gives a nice example of displaying an additional visualisation of the proof state.

[Moritz Firsching]

Now I was looking into this a bit more, and I thought I would mimic what the StringDiagram widget does and also what you linked to above. So I wrote this @[server_rpc_method] myrpc method which is supposed to return some html for the Position if we are our result prop comes from ForcedWin (Side → Position → Prop) evaluated at a Side and Position,
https://github.com/mo271/animate-lean-proofs/blob/4b84bb0a955a55c8127d0cb0033d34b66bdff7b1/ChessWidgetExample.lean#L53C20-L78

open scoped Jsx in
/-- The RPC method for displaying FEN for ForcedWin (Side → Position → Prop). -/
@[server_rpc_method]
def myrpc (props : PanelWidgetProps) : RequestM (RequestTask Html) :=
  RequestM.asTask do
    let html : Option Html ← (do
      if props.goals.isEmpty then
        return none  -- No goals, return none
      else
        let some g := props.goals[0]? | unreachable!
        g.ctx.val.runMetaM {} do
          g.mvarId.withContext do
            -- Get the goal's type
            let type ← g.mvarId.getType
            -- Extract the function name and arguments using `getAppFnArgs`
            let (fn, args) := type.getAppFnArgs
            if fn == ``ForcedWin && args.size == 2 then
              -- Extract the `Position` argument
              let posExpr := args[1]!  -- The second argument should be the Position
              -- Try to manually interpret `posExpr` as a `Position` somehow
              let posVal ← evalExpr _root_.Position (mkConst ``_root_.Position) posExpr

              -- Convert the interpreted position to FEN
              let fenStr := fenFromPosition posVal
              return some <span>FEN: {Html.text fenStr}</span>
            return none)
    match html with
    | none => return <span>No ForcedWin goal found or invalid type.</span>
    | some inner => return inner

I think it is all more or less correct, but I get (kernel) invalid declaration, it uses unsafe declaration 'Lean.Meta.evalExpr' and when I use unsafe for the def myrpc, I get just get a similar error down the road:
(kernel) invalid declaration, it uses unsafe declaration 'Chess.myrpc'
So therefore my question is:

Is there a safe alternative to Lean.Meta.evalExpr?

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

@Moritz Firsching at first glance I think the issue is that evalExpr can only evaluate _closed_ (variable-free) expressions, whereas you are trying to evaluate part of the goal state which might contain free variables. I think the only solution is to pattern-match on the position Expr and get out what you need from it, otherwise fail.

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

If you are sure that the Position you see there is closed, so that evalExpr can run, the standard solution is to write a safe wrapper around evalExpr at a specific type.

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

Like this.

[Eric Wieser]

Or just use the unsafe term syntax?

[Moritz Firsching]

Thank you both! the unsafe term syntax worked, so I didn't try the other approach.
docs#Lean.Parser.Term.unsafe

[Moritz Firsching]

Now it works great for displaying the FEN. For also displaying the nicely rendered board, I turned my ChessPositionWidget into a component like so:

structure ChessPositionWidgetProps where
  pos? : Option Position := none
  deriving Lean.Server.RpcEncodable

open ProofWidgets

@[widget]
def ChessPositionWidget : Component ChessPositionWidgetProps where
  javascript := "[all the javascript that renders the board, using stuff from `pos`]"

and while it displays the board fine in calls like this:

#widget ChessPositionWidget with { pos? := get_pos Chess.morphy_mates_in_two : ChessPositionWidgetProps }

when I use it as a component in the ForcedWinWidget, it only displays the empty board.
https://github.com/mo271/animate-lean-proofs/blob/5aa3cd3820c9779164be39dee491fc6bb18d718f/ChessWidgetExample.lean#L79
while the FEN for the same Position gets extracted and displayed correctly.
(full working code in that commit)
What am I doing wrong?

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

Hah, I was worried this would happen to somebody eventually. Widgets have a builtin prop called pos, and it is overwriting the one you are providing. If you just change it to boardPos or something, it should work. We should have a warning shown in this edge case, though.

[Moritz Firsching]

Thanks @Wojciech Nawrocki, it works now: https://github.com/dwrensha/animate-lean-proofs/blob/e5e8a4a7c30e4a9e17910aed4c843a17ad226b67/Chess/Widgets.lean,
review/comments welcome at https://github.com/dwrensha/animate-lean-proofs/pull/7

So I suppose the other forbidden prop names are goals, termGoal and selectedLocations (from docs#ProofWidgets.PanelWidgetProps ) ?

Where would we best show a warning, just in the documentation somewhere (where?) or in the code when you try to define such a prop name?