Using `exprDiff` in widgets

Stream: lean4

[Eric Wieser]

I'm trying to print the output of docs#Lean.Widget.exprDiff as a widget, using the <InteractiveCode> widget, but the diff doesn't seem to be showing up:

import Lean
import ProofWidgets.Data.Html
import ProofWidgets.Component.HtmlDisplay

open Lean Json
open ProofWidgets Jsx

def diff (before after : Name) : MetaM Html := do
  let before_t := (← Lean.getConstInfo before).type
  let after_t := (← Lean.getConstInfo after).type
  let diff ← Lean.Widget.exprDiff before_t after_t
  let before_tagged ← Widget.ppExprTagged before_t
  let after_tagged ← Widget.ppExprTagged after_t

  let before_diff ← Lean.Widget.addDiffTags false diff before_tagged
  let after_diff ← Lean.Widget.addDiffTags true diff after_tagged

  return <div>
    <InteractiveCode fmt={before_diff} /><br />
    <InteractiveCode fmt={after_diff} />
  </div>

syntax "#diff_types" ident ident : command
elab_rules : command
| `(#diff_types%$tk $a:ident $b:ident) => Elab.Command.liftTermElabM do
  let h ← diff a.getId b.getId
  Widget.savePanelWidgetInfo (hash ProofWidgets.HtmlDisplayPanel.javascript)
    (return json% { html: $(← Server.RpcEncodable.rpcEncode h) }) tk

/-- begin example -/

theorem foo : 1 + 2 = 3 := sorry
theorem bar : 2 + 1 = 3 := sorry

-- doesn't show any diff
#diff_types foo bar

[Eric Wieser]

(this doesn't seem to work at all in the web editor due to The requested module 'blob:https://live.lean-lang.org/99574127-ee5e-469d-9348-e622cadff5ad' does not provide an export named 'useRpcSession')

[Henrik Böving]

@Joachim Breitner is this the fault of our workaround?

[Anand Rao Tadipatri]

This widget works on v4.8.0-rc1, but without the diff highlighting.

[Eric Wieser]

Yes, to be clear my issue is that the types appear with no highlighting

[Eric Wieser]

It looks to me like Lean.Widget.addDiffTags is not actually populating the tags?

[Henrik Böving]

Ah probably not from our recent workaround then.

[Eric Wieser]

open private ExprDiffTag from Lean.Widget.Diff
deriving instance Repr for ExprDiffTag
deriving instance Repr for Widget.DiffTag
deriving instance Repr for Widget.ExprDiff

partial def Lean.Widget.TaggedText.listTags {α} : Widget.TaggedText α → List α
  | .text _ => []
  | .tag t inner => t :: inner.listTags
  | .append ars => (ars.toList.bind Lean.Widget.TaggedText.listTags)

and running Lean.logInfo m!"{repr (before_diff.listTags.map (·.diffStatus?))}" gives a list of nones

[Patrick Massot]

@Wojciech Nawrocki

[Anand Rao Tadipatri]

Here is one way of rendering diffs of expressions that has worked for me in the past:

import Lean
import ProofWidgets.Data.Html
import ProofWidgets.Component.HtmlDisplay

namespace Lean

open Lean ProofWidgets Widget Server Jsx

def Widget.CodeWithInfos.addDiffs (diffs : AssocList SubExpr.Pos DiffTag) (code : CodeWithInfos) : CodeWithInfos :=
  code.map fun info ↦
    match diffs.find? info.subexprPos with
      | some diff => { info with diffStatus? := some diff }
      |    none   =>   info

def Expr.renderWithDiffs (e : Expr) (diffs : AssocList SubExpr.Pos DiffTag) : MetaM Html := do
  let e' := (← Widget.ppExprTagged e).addDiffs diffs
  return <InteractiveCode fmt={e'} />

def Name.renderWithDiffs (nm : Name) (diffs : AssocList SubExpr.Pos DiffTag) : MetaM Html := do
  let env ← getEnv
  let some ci := env.find? nm | failure
  ci.type.renderWithDiffs diffs

end Lean

open Lean ProofWidgets

elab stx:"#test_diff_render" thm:ident : command => Elab.Command.liftTermElabM do
  let h ← thm.getId.renderWithDiffs (.cons (.root |>.pushBindingBody |>.pushAppArg) .willChange .nil)
  Widget.savePanelWidgetInfo (hash ProofWidgets.HtmlDisplayPanel.javascript)
    (return json% { html: $(← Server.RpcEncodable.rpcEncode h) }) stx

#test_diff_render Nat.mul_zero

[Eric Wieser]

With that example, I have to build the diff myself rather than using Lean.Widget.exprDiff, right?

[Joachim Breitner]

Henrik Böving said:

Joachim Breitner is this the fault of our workaround?

Which work-around again?

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

Eric Wieser said:

(this doesn't seem to work at all in the web editor due to The requested module 'blob:https://live.lean-lang.org/99574127-ee5e-469d-9348-e622cadff5ad' does not provide an export named 'useRpcSession')

Ah, most likely the web editor needs to update its @leanprover/infoview dependency.

[Eric Wieser]

Eric Wieser said:

It looks to me like Lean.Widget.addDiffTags is not actually populating the tags?

Looking more closely; the Pos info in the result of exprDiff doesn't match with the pos info in ppExprTagged

[Eric Wieser]

It works correctly if the theorems being compared start with a pi binder! That is, my original code works with

theorem foo2 {x} : x + 2 = 3 := sorry
theorem bar2 {x} : 2 + x = 3 := sorry

-- works
#diff_types foo2 bar2

[Henrik Böving]

Joachim Breitner said:

Henrik Böving said:

Joachim Breitner is this the fault of our workaround?

Which work-around again?

The one where we hide symbols from the LSP, but it's not it.

[Eric Wieser]

I think the issue here is that the diff highlighting only works if the Subexpr being highlighted already has info attached

[Eric Wieser]

In my original example, it fails because exprDiff detects the diff at the nat_lit 1 in @OfNat.ofNat _ _ (nat_lit 1), but the tagged format only records a node for the entire @OfNat.ofNat node