feat: adapt to lean4#2964

ProofWidgets/Compat.lean

@@ -1,30 +1,10 @@
-import Lean.Attributes
-import Lean.Widget.UserWidget
-import Std.Data.Json
-
-/-!
-A compatibility layer aimed at redefining the user widget API in terms of modules and components.
-New features:
-- component props have Lean types
-- props can be RpcEncodable
-- we distinguish between an arbitrary 'widget module' (any ES module) and a 'widget component',
-  that is a module which can be rendered
-- moreover only 'panel widget components' can appear as top-level panels in the infoview
-
-TODO: If the design works out, it could replace the current Lean core definitions.
--/
+import Lean.Elab.InfoTree.Main
 
 namespace ProofWidgets
 open Lean Server Elab
 
-deriving instance TypeName for Expr
-
 abbrev LazyEncodable α := StateM RpcObjectStore α
 
-instance : RpcEncodable (LazyEncodable Json) where
-  rpcEncode fn := fn
-  rpcDecode j := return return j
-
 -- back from exile
 structure ExprWithCtx where
   ci : Elab.ContextInfo
@@ -42,151 +22,4 @@ def ExprWithCtx.save (e : Expr) : MetaM ExprWithCtx :=
     expr := e
   }
 
-open Command in
-/-- Derive `Lean.Server.RpcEncodable` for a type.
-
-HACK: around https://leanprover.zulipchat.com/#narrow/stream/341532-lean4-dev/topic/Should.20instance.20names.20inherit.20macro.20scopes.3F -/
-elab "#mkrpcenc" n:ident : command => do
-  elabCommand <| ← `(
-    namespace $n
-    deriving instance Lean.Server.RpcEncodable for $n
-    end $n
-  )
-
-def widgetDefPostfix : Name := `_userWidgetDef
-
--- NOTE: Compared to core, this is almost like UserWidgetDefinition but with a different "attitude":
--- the module itself need not be a user widget, i.e. it can also be a support library. It doesn't
--- need a displayable `name`.
-/-- A widget module is a unit of source code that can execute in the infoview. -/
-structure Module where
-  /-- A JS [module](https://developer.mozilla.org/en-US/docs/Web/JavaScript/Guide/Modules) intended
-  for use in user widgets.
-
-  To initialize this field from an external JS file, use `include_str "path"/"to"/"file.js"`.
-  However **beware** that this does not register a dependency with Lake, so your Lean module will
-  not automatically be rebuilt when the `.js` file changes. -/
-  javascript : String
-
--- This could maybe be a macro but good luck actually writing it.
-open Lean Meta Elab Command in
-initialize
-  registerBuiltinAttribute {
-    name := `widget_module
-    descr := "Registers a widget module. Its type must extend ProofWidgets.Module."
-    applicationTime := AttributeApplicationTime.afterCompilation
-    -- The implementation is a hack due to the fact that widgetSource is tied to the storage
-    -- of user widgets. I think a single widgetModuleRegistry should suffice. TODO fix in core.
-    add := fun nm _ _ => do
-      let dc : TSyntax ``Parser.Command.docComment :=
-        mkNode ``Parser.Command.docComment #[
-          mkAtom "/--",
-          mkAtom s!"User widget definition for the widget module {nm}. -/"]
-      -- The type of `nm` is not checked,
-      -- so technically any type with a `javascript : String` projection will work.
-      let proc : CommandElabM Unit := do
-        elabCommand <| ← `(command|
-          $dc:docComment
-          @[widget]
-          def $(mkIdent <| nm ++ widgetDefPostfix) : Lean.Widget.UserWidgetDefinition where
-            name := $(quote nm.toString)
-            javascript := $(mkIdent nm).javascript)
-      let ctx ← read
-      let st ← get
-      -- Cursed manual CommandElabM => CoreM lift punning all fields
-      let (_, st') ← proc.run { st, ctx with tacticCache? := none } |>.run { st, ctx with }
-      set { st' with : Core.State }
-  : AttributeImpl }
-
--- "goal widget"/"at cursor widget"/"panel widget"/"info block widget"
-structure PanelWidgetInfo where
-  /-- Name of the `widget_module` to show. -/
-  id : Name
-  props : LazyEncodable Json
-  -- Compatibility hack. Remove if in core.
-  infoId : Name
-  deriving TypeName
-
-/-- A widget component with a resolved source hash and its props. -/
-structure WidgetInstance where
-  /-- Name of the `widget_module`. -/
-  id : Name
-  srcHash : UInt64
-  props : LazyEncodable Json
-  -- Compatibility hack. Remove if in core.
-  infoId : Name
-
-#mkrpcenc WidgetInstance
-
-structure PanelWidgetInstance extends WidgetInstance where
-  range? : Option Lsp.Range
-
-#mkrpcenc PanelWidgetInstance
-
-structure GetPanelWidgetsParams where
-  pos : Lsp.Position
-  deriving FromJson, ToJson
-
-structure GetPanelWidgetsResponse where
-  widgets : Array PanelWidgetInstance
-
-#mkrpcenc GetPanelWidgetsResponse
-
-def customInfosAt? (text : FileMap) (t : InfoTree) (hoverPos : String.Pos) : List CustomInfo :=
-  t.deepestNodes fun
-    | _ctx, i@(Info.ofCustomInfo ci), _cs => do
-      if let (some pos, some tailPos) := (i.pos?, i.tailPos?) then
-        let trailSize := i.stx.getTrailingSize
-        -- show info at EOF even if strictly outside token + trail
-        let atEOF := tailPos.byteIdx + trailSize == text.source.endPos.byteIdx
-        guard <| pos ≤ hoverPos ∧ (hoverPos.byteIdx < tailPos.byteIdx + trailSize || atEOF)
-        return ci
-      else
-        failure
-    | _, _, _ => none
-
-open RequestM in
-@[server_rpc_method]
-def getPanelWidgets (args : GetPanelWidgetsParams) : RequestM (RequestTask GetPanelWidgetsResponse)
-    := do
-  let doc ← readDoc
-  let filemap := doc.meta.text
-  let pos := filemap.lspPosToUtf8Pos args.pos
-  withWaitFindSnap doc (·.endPos >= pos) (notFoundX := return ⟨∅⟩) fun snap => do
-    let ws := customInfosAt? filemap snap.infoTree pos
-    let mut widgets := #[]
-    for w in ws do
-      let some wi := w.value.get? PanelWidgetInfo
-        -- We may encounter other custom infos of unknown type. Ignore them.
-        | continue
-      let some widgetDef := Widget.userWidgetRegistry.find? snap.env (wi.id ++ widgetDefPostfix)
-        | throw <| RequestError.invalidParams s!"No registered widget source with id {wi.id}"
-      widgets := widgets.push { wi with
-        srcHash := widgetDef.javascriptHash
-        range? := String.Range.toLspRange filemap <$> Syntax.getRange? w.stx
-      }
-    return {widgets}
-
-@[widget]
-def metaWidget : Lean.Widget.UserWidgetDefinition where
-  -- The header is sometimes briefly visible before compat.tsx loads and hides it
-  name := "Loading ProofWidgets.."
-  javascript := include_str ".." / ".lake" / "build" / "js" / "compat.js"
-
-open scoped Json in
-/-- Save the data of a panel widget which will be displayed whenever the text cursor is on `stx`.
-`id` must be the name of a definition annotated with `@[widget_module]`. See `PanelWidgetProps`. -/
-def savePanelWidgetInfo [Monad m] [MonadInfoTree m] [MonadNameGenerator m]
-    (stx : Syntax) (id : Name) (props : LazyEncodable Json) : m Unit := do
-  let infoId := `panelWidget ++ (← mkFreshId)
-  pushInfoLeaf <| .ofUserWidgetInfo {
-    stx
-    widgetId := ``metaWidget
-    props := json% {
-      infoId : $(infoId)
-    }
-  }
-  let wi : PanelWidgetInfo := { id, props, infoId }
-  pushInfoLeaf <| .ofCustomInfo { stx, value := Dynamic.mk wi }
-
 end ProofWidgets

ProofWidgets/Component/Basic.lean

@@ -1,7 +1,9 @@
 import Lean.Widget.InteractiveCode
+import Lean.Widget.UserWidget
 import ProofWidgets.Compat
 
 namespace ProofWidgets
+open Lean
 
 /-- A component is a widget module with a `default` or named export which is a
 [React component](https://react.dev/learn/your-first-component). Every component definition must
@@ -28,11 +30,11 @@ specifying how to encode props as JSON.
 
 Note that by defining a `Component Props` with a specific JS implementation,
 you are *asserting* that `Props` is a correct representation of `JsProps`. -/
-structure Component (Props : Type) extends Module where
+structure Component (Props : Type) extends Widget.Module where
   /-- Which export of the module to use as the component function. -/
   «export» : String := "default"
 
-open Lean
+instance : Widget.ToModule (Component Props) := ⟨Component.toModule⟩
 
 structure InteractiveCodeProps where
   fmt : Widget.CodeWithInfos

ProofWidgets/Component/HtmlDisplay.lean

@@ -1,4 +1,5 @@
 import Lean.Server.Rpc.Basic
+import Std.Data.Json
 
 import ProofWidgets.Data.Html
 
@@ -35,8 +36,9 @@ def elabHtmlCmd : CommandElab := fun
   | stx@`(#html $t:term) =>
     runTermElabM fun _ => do
       let ht ← evalHtml t
-      savePanelWidgetInfo stx ``HtmlDisplayPanel do
-        return json% { html: $(← rpcEncode ht) }
+      Widget.savePanelWidgetInfo (hash HtmlDisplayPanel.javascript)
+        (return json% { html: $(← rpcEncode ht) }) stx
+
   | stx => throwError "Unexpected syntax {stx}."
 
 syntax (name := htmlTac) "html! " term : tactic
@@ -46,8 +48,8 @@ open Elab Tactic Json in
 def elabHtmlTac : Tactic
   | stx@`(tactic| html! $t:term) => do
     let ht ← evalHtml t
-    savePanelWidgetInfo stx ``HtmlDisplayPanel do
-      return json% { html: $(← rpcEncode ht) }
+    Widget.savePanelWidgetInfo (hash HtmlDisplayPanel.javascript)
+      (return json% { html: $(← rpcEncode ht) }) stx
   | stx => throwError "Unexpected syntax {stx}."
 
 end ProofWidgets

ProofWidgets/Component/Panel/Basic.lean

@@ -29,19 +29,6 @@ structure PanelWidgetProps : Type where
 
 #mkrpcenc PanelWidgetProps
 
-def processIdent (stx : Syntax) (nmStx : TSyntax `ident) : CoreM Unit := do
-  let nm ← resolveGlobalConstNoOverloadWithInfo nmStx
-  let const ← getConstInfo nm
-  if ← (pure (!const.type.isAppOfArity' ``Component 1) <||>
-        pure (!const.type.appArg!'.isConstOf ``PanelWidgetProps)) then
-    let expType := Expr.app (mkConst ``Component) (mkConst ``PanelWidgetProps)
-    logWarningAt nmStx
-      m!"unexpected panel widget type, got{indentExpr const.type}\nbut expected{indentExpr expType}"
-  if !Widget.userWidgetRegistry.contains (← getEnv) (nm ++ widgetDefPostfix) then
-    logWarningAt nmStx
-      m!"panel widget{indentExpr (mkConst nm)}\nwas not registered with `@[widget_module]`"
-  savePanelWidgetInfo stx nm (pure .null)
-
 /-- Display the selected panel widgets in the nested tactic script. For example,
 assuming we have written a `GeometryDisplay` component,
 ```lean
@@ -51,12 +38,16 @@ by with_panel_widgets [GeometryDisplay]
 ```
 will show the geometry display alongside the usual tactic state throughout the proof.
 -/
-syntax (name := withPanelWidgetsTacticStx) "with_panel_widgets" "[" ident,+ "]" tacticSeq : tactic
+syntax (name := withPanelWidgetsTacticStx)
+  "with_panel_widgets" "[" Widget.widgetInstanceSpec,+ "]" tacticSeq : tactic
 
 @[tactic withPanelWidgetsTacticStx]
 def withPanelWidgets : Tactic
-  | stx@`(tactic| with_panel_widgets [ $nms,* ] $seq) => do
-    liftM <| nms.getElems.forM (processIdent stx)
+  | stx@`(tactic| with_panel_widgets [ $specs,* ] $seq) => do
+    specs.getElems.forM fun specStx => do
+      let spec ← Widget.elabWidgetInstanceSpec specStx
+      let wi ← Widget.evalWidgetInstance spec
+      Widget.savePanelWidgetInfo wi.javascriptHash wi.props stx
     evalTacticSeq seq
   | _ => throwUnsupportedSyntax
 

ProofWidgets/Component/Recharts.lean

@@ -4,7 +4,7 @@ namespace ProofWidgets.Recharts
 open Lean
 
 @[widget_module]
-def Recharts : Module where
+def Recharts : Widget.Module where
   javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "recharts.js"
 
 inductive LineChartLayout where

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "d3049643f6dded69eb7ce8124796cb1ec8df8840",
+   "rev": "ee49cf8fada1bf5a15592c399a925c401848227f",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.3.0-rc2
+leanprover/lean4:v4.5.0-rc1