feat: bundle of widget improvements (#2964)

Implements RFC #2963.

Leftover tasks:
- [x] Provide companion PR to vscode-lean4 (leanprover/vscode-lean4#376)
- [x] Companion PR to std4 (leanprover-community/batteries#467)
- [x] Companion PR to ProofWidgets4
(leanprover-community/ProofWidgets4#36)
- [X] Companion commit to mathlib4
(leanprover-community/mathlib4@0f4660f)
- [ ] ~~Update the manual chapter~~ (will do in a follow-up)

doc/examples/widgets.lean

@@ -15,17 +15,16 @@ sections of a Lean document. User widgets are rendered in the Lean infoview.
 To try it out, simply type in the following code and place your cursor over the `#widget` command.
 -/
 
-@[widget]
-def helloWidget : UserWidgetDefinition where
-  name := "Hello"
+@[widget_module]
+def helloWidget : Widget.Module where
   javascript := "
     import * as React from 'react';
     export default function(props) {
       const name = props.name || 'world'
       return React.createElement('p', {}, name + '!')
     }"
 
-#widget helloWidget .null
+#widget helloWidget
 
 /-!
 If you want to dive into a full sample right away, check out
@@ -56,7 +55,11 @@ to the React component. In our first invocation of `#widget`, we set it to `.nul
 happens when you type in:
 -/
 
-#widget helloWidget (Json.mkObj [("name", "<your name here>")])
+structure HelloWidgetProps where
+  name? : Option String := none
+  deriving Server.RpcEncodable
+
+#widget helloWidget with { name? := "<your name here>" : HelloWidgetProps }
 
 /-!
 💡 NOTE: The RPC system presented below does not depend on JavaScript. However the primary use case
@@ -132,9 +135,8 @@ on this we either display an `InteractiveCode` with the type, `mapRpcError` the
 to turn it into a readable message, or show a `Loading..` message, respectively.
 -/
 
-@[widget]
-def checkWidget : UserWidgetDefinition where
-  name := "#check as a service"
+@[widget_module]
+def checkWidget : Widget.Module where
   javascript := "
 import * as React from 'react';
 const e = React.createElement;
@@ -160,7 +162,7 @@ export default function(props) {
 Finally we can try out the widget.
 -/
 
-#widget checkWidget .null
+#widget checkWidget
 
 /-!
 ![`#check` as a service](../images/widgets_caas.png)
@@ -193,9 +195,8 @@ interact with the text editor.
 You can see the full API for this [here](https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview-api/src/infoviewApi.ts#L52)
 -/
 
-@[widget]
-def insertTextWidget : UserWidgetDefinition where
-  name := "textInserter"
+@[widget_module]
+def insertTextWidget : Widget.Module where
   javascript := "
 import * as React from 'react';
 const e = React.createElement;
@@ -213,4 +214,4 @@ export default function(props) {
 
 /-! Finally, we can try this out: -/
 
-#widget insertTextWidget .null
+#widget insertTextWidget

src/Lean/Attributes.lean

@@ -330,7 +330,7 @@ private def AttributeExtension.mkInitial : IO AttributeExtensionState := do
 
 unsafe def mkAttributeImplOfConstantUnsafe (env : Environment) (opts : Options) (declName : Name) : Except String AttributeImpl :=
   match env.find? declName with
-  | none      => throw ("unknow constant '" ++ toString declName ++ "'")
+  | none      => throw ("unknown constant '" ++ toString declName ++ "'")
   | some info =>
     match info.type with
     | Expr.const `Lean.AttributeImpl _ => env.evalConst AttributeImpl opts declName

src/Lean/Elab/InfoTree/Main.lean

@@ -142,7 +142,7 @@ def MacroExpansionInfo.format (ctx : ContextInfo) (info : MacroExpansionInfo) :
   return f!"Macro expansion\n{stx}\n===>\n{output}"
 
 def UserWidgetInfo.format (info : UserWidgetInfo) : Format :=
-  f!"UserWidget {info.widgetId}\n{Std.ToFormat.format info.props}"
+  f!"UserWidget {info.id}\n{Std.ToFormat.format <| info.props.run' {}}"
 
 def FVarAliasInfo.format (info : FVarAliasInfo) : Format :=
   f!"FVarAlias {info.userName.eraseMacroScopes}"

src/Lean/Elab/InfoTree/Types.lean

@@ -9,6 +9,8 @@ import Lean.Data.OpenDecl
 import Lean.MetavarContext
 import Lean.Environment
 import Lean.Data.Json
+import Lean.Server.Rpc.Basic
+import Lean.Widget.Types
 
 namespace Lean.Elab
 
@@ -95,17 +97,12 @@ structure CustomInfo where
   stx : Syntax
   value : Dynamic
 
-/-- An info that represents a user-widget.
-User-widgets are custom pieces of code that run on the editor client.
-You can learn about user widgets at `src/Lean/Widget/UserWidget`
--/
-structure UserWidgetInfo where
+/-- Information about a user widget associated with a syntactic span.
+This must be a panel widget.
+A panel widget is a widget that can be displayed
+in the infoview alongside the goal state. -/
+structure UserWidgetInfo extends Widget.WidgetInstance where
   stx : Syntax
-  /-- Id of `WidgetSource` object to use. -/
-  widgetId : Name
-  /-- Json representing the props to be loaded in to the component. -/
-  props : Json
-  deriving Inhabited
 
 /--
 Specifies that the given free variables should be considered semantically identical.

src/Lean/Server/Rpc/Basic.lean

@@ -62,18 +62,28 @@ def rpcReleaseRef (r : Lsp.RpcRef) : StateM RpcObjectStore Bool := do
   else
     return false
 
-/--
-`RpcEncodable α` means that `α` can be serialized in the RPC system of the Lean server.
-This is required when `α` contains fields which should be serialized as an RPC reference
-instead of being sent in full.
-The type wrapper `WithRpcRef` is used for these fields which should be sent as
-a reference.
-
-- Any type with `FromJson` and `ToJson` instance is automatically `RpcEncodable`.
-- If a type has an `Dynamic` instance, then `WithRpcRef` can be used for its references.
-- `deriving RpcEncodable` acts like `FromJson`/`ToJson` but marshalls any `WithRpcRef` fields
-  as `Lsp.RpcRef`s.
--/
+/-- `RpcEncodable α` means that `α` can be deserialized from and serialized into JSON
+for the purpose of receiving arguments to and sending return values from
+Remote Procedure Calls (RPCs).
+
+Any type with `FromJson` and `ToJson` instances is `RpcEncodable`.
+
+Furthermore, types that do not have these instances may still be `RpcEncodable`.
+Use `deriving RpcEncodable` to automatically derive instances for such types.
+
+This occurs when `α` contains data that should not or cannot be serialized:
+for instance, heavy objects such as `Lean.Environment`, or closures.
+For such data, we use the `WithRpcRef` marker.
+Note that for `WithRpcRef α` to be `RpcEncodable`,
+`α` must have a `TypeName` instance
+
+On the server side, `WithRpcRef α` is just a structure
+containing a value of type `α`.
+On the client side, it is an opaque reference of (structural) type `Lsp.RpcRef`.
+Thus, `WithRpcRef α` is cheap to transmit over the network
+but may only be accessed on the server side.
+In practice, it is used by the client to pass data
+between various RPC methods provided by the server. -/
 -- TODO(WN): for Lean.js, compile `WithRpcRef` to "opaque reference" on the client
 class RpcEncodable (α : Type) where
   rpcEncode : α → StateM RpcObjectStore Json
@@ -103,7 +113,15 @@ instance [RpcEncodable α] [RpcEncodable β] : RpcEncodable (α × β) where
     let (a, b) ← fromJson? j
     return (← rpcDecode a, ← rpcDecode b)
 
-/-- Marks fields to encode as opaque references in LSP packets. -/
+instance [RpcEncodable α] : RpcEncodable (StateM RpcObjectStore α) where
+  rpcEncode fn := fn >>= rpcEncode
+  rpcDecode j := do
+    let a : α ← rpcDecode j
+    return return a
+
+/-- Marks values to be encoded as opaque references in RPC packets.
+
+See the docstring for `RpcEncodable`. -/
 structure WithRpcRef (α : Type u) where
   val : α
   deriving Inhabited

src/Lean/Server/Rpc/Deriving.lean

@@ -42,7 +42,10 @@ private def deriveStructureInstance (indVal : InductiveVal) (params : Array Expr
 
   let paramIds ← params.mapM fun p => return mkIdent (← getFVarLocalDecl p).userName
 
-  `(structure RpcEncodablePacket where
+  let indName := mkIdent indVal.name
+  `(-- Workaround for https://github.com/leanprover/lean4/issues/2044
+    namespace $indName
+    structure RpcEncodablePacket where
       $[($fieldIds : $fieldTys)]*
       deriving FromJson, ToJson
 
@@ -55,6 +58,7 @@ private def deriveStructureInstance (indVal : InductiveVal) (params : Array Expr
       dec j := do
         let a : RpcEncodablePacket ← fromJson? j
         return { $[$decInits],* }
+    end $indName
   )
 
 private def matchAltTerm := Lean.Parser.Term.matchAlt (rhsParser := Lean.Parser.termParser)
@@ -92,7 +96,10 @@ private def deriveInductiveInstance (indVal : InductiveVal) (params : Array Expr
   let paramIds ← params.mapM fun p => return mkIdent (← getFVarLocalDecl p).userName
   let typeId ← `(@$(mkIdent indVal.name) $paramIds*)
 
-  `(inductive RpcEncodablePacket where
+  let indName := mkIdent indVal.name
+  `(-- Workaround for https://github.com/leanprover/lean4/issues/2044
+    namespace $indName
+    inductive RpcEncodablePacket where
       $[$ctors:ctor]*
       deriving FromJson, ToJson
 
@@ -107,6 +114,7 @@ private def deriveInductiveInstance (indVal : InductiveVal) (params : Array Expr
         have inst : RpcEncodable $typeId := { rpcEncode := enc, rpcDecode := dec }
         let pkt : RpcEncodablePacket ← fromJson? j
         id <| match pkt with $[$decodes:matchAlt]*
+    end $indName
   )
 
 /-- Creates an `RpcEncodablePacket` for `typeName`. For structures, the packet is a structure

src/Lean/Widget/Basic.lean

@@ -2,6 +2,7 @@ import Lean.Elab.InfoTree
 import Lean.Message
 import Lean.Server.Rpc.Basic
 import Lean.Server.InfoUtils
+import Lean.Widget.Types
 
 namespace Lean.Widget
 

src/Lean/Widget/Types.lean

@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2023 Wojciech Nawrocki. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Wojciech Nawrocki
+-/
+import Lean.Server.Rpc.Basic
+
+namespace Lean.Widget
+
+/-- An instance of a widget component:
+the identifier of a widget module and the hash of its JS source code
+together with props.
+
+See the [manual entry](https://lean-lang.org/lean4/doc/examples/widgets.lean.html)
+for more information about widgets. -/
+structure WidgetInstance where
+  /-- Name of the `@[widget_module]`. -/
+  id : Name
+  /-- Hash of the JS source of the widget module. -/
+  javascriptHash : UInt64
+  /-- Arguments to be passed to the component's default exported function.
+
+  Props may contain RPC references,
+  so must be stored as a computation
+  with access to the RPC object store. -/
+  props : StateM Server.RpcObjectStore Json
+
+end Lean.Widget