feat: widget tutorial and general RequestM lifts

doc/widgets.md

@@ -1,37 +1,175 @@
 # The user-widgets system
 
-Proving is an inherently interactive task. Lots of mathematical objects that we use are visual in nature.
-The user-widget system lets users associate React components with the Lean document which are then rendered in the Lean VSCode infoview.
+Proving and programming are inherently interactive tasks. Lots of mathematical objects and data
+structures are visual in nature. *User widgets* let you associate custom interactive UIs with
+sections of a Lean document. User widgets are rendered in the Lean infoview.
 
-There is nothing about the RPC calls presented here that make the user-widgets system
-dependent on JavaScript. However the primary use case is the web-based infoview in VSCode.
+![Rubik's cube](images/widgets_rubiks.png)
 
-## How to write your own user-widgets
+## Trying it out
 
-You can write your own user-widgets using the `@[widgetSource]` attribute:
+To try it out, simply type in the following code and place your cursor over the `#widget` command.
 
 ```lean
 import Lean
 open Lean Widget
 
 @[widget]
-def widget1 : UserWidgetDefinition := {
-  name := "my fancy widget"
+def helloWidget : UserWidgetDefinition where
+  name := "Hello"
   javascript := "
-  import * as React from 'react';
-  export default function (props) {
-    return React.createElement('p', {}, 'hello')
-  }"
+    import * as React from 'react';
+    export default function(props) {
+      const name = props.name || 'world'
+      return React.createElement('p', {}, name + '!')
+    }"
+
+#widget helloWidget .null
+```
+
+If you want to dive into a full sample right away, check out [`Rubiks`](TODO merge). Below,
+we'll explain the system piece by piece.
+
+⚠️ WARNING: All of the user widget APIs are **unstable** and subject to breaking changes.
+
+## Widget sources and instances
+
+A *widget source* is a valid JavaScript [ESModule](https://developer.mozilla.org/en-US/docs/Web/JavaScript/Guide/Modules)
+which exports a [React component](https://reactjs.org/docs/components-and-props.html). To access
+React, the module must use `import * as React from 'react'`. Our first example of a widget source
+is of course the value of `helloWidget.javascript`.
+
+We can register a widget source with the `@[widget]` attribute, giving it a friendlier name
+in the `name` field. This is bundled together in a `UserWidgetDefinition`.
+
+A *widget instance* is then the identifier of a `UserWidgetDefinition` (so `` `helloWidget ``,
+not `"Hello"`) associated with a range of positions in the Lean source code. In our example,
+the `#widget` command places a widget instance with the entire line as its range. We can think
+of a widget instance as an instruction for the infoview: "when the user places their cursor here,
+please render the following widget".
+
+Every widget instance also contains a `props : Json` value. This value is passed as an argument
+to the React component. In our first invocation of `#widget`, we set it to `.null`. Try out what
+happens when you type in `#widget helloWidget (Json.mkObj [("name", "<your name here>")])`.
+
+💡 NOTE: The RPC system presented below does not depend on JavaScript. However the primary use case
+is the web-based infoview in VSCode.
+
+## Querying the Lean server
+
+The interesting functionality of user widgets comes from their ability to communicate with the Lean
+server. To see this in action, let's implement a `#check` command as a web input form. This example
+assumes some familiarity with React.
+
+The first thing we'll need is to create an *RPC method*. This is basically a Lean function callable
+from widget code (possibly remotely over the internet). Our method will take in the `name : Name`
+of a constant in the environment and return its type. By convention, we represent the input data
+as a `structure`. Since it will be sent over from JavaScript, we need `FromJson` and `ToJson`.
+We'll see below why the position field is needed.
+
+```lean
+structure GetTypeParams where
+  /-- Name of a constant to get the type of. -/
+  name : Name
+  /-- Position of our widget instance in the Lean file. -/
+  pos : Lsp.Position
+  deriving FromJson, ToJson
+```
+
+After its arguments, we define the `getType` method. Every RPC method executes in the `RequestM`
+monad and must return a `RequestTask α` where `α` is its "actual" return type. The `Task` is so
+that requests can be handled concurrently. A first guess for `α` might be `Expr`. However,
+expressions in general can be large objects which depend on an `Environment` and `LocalContext`.
+Thus we cannot directly serialize an `Expr` and send it to the widget. Instead, there are two
+options:
+- One is to send a *reference* which points to an object residing on the server. From JavaScript's
+  point of view, references are entirely opaque, but they can be sent back to other RPC methods for
+  further processing.
+- Two is to pretty-print the expression and send its textual representation called `CodeWithInfos`.
+  This representation contains extra data which the infoview uses for interactivity. We take this
+  strategy here.
+
+RPC methods execute in the context of a file, but not any particular `Environment` so they don't
+know about the available `def`initions and `theorem`s. Thus, we need to pass in a position at which
+we want to use the local `Environment`. This is why we store it in `GetTypeParams`. The `withWaitFindSnapAtPos`
+method launches a concurrent computation whose job is to find such an `Environment` and a bit
+more information for us, in the form of a `snap : Snapshot`. With this in hand, we can call
+`MetaM` procedures to find out the type of `name` and pretty-print it.
+
+```lean
+open Server RequestM in
+@[serverRpcMethod]
+def getType (params : GetTypeParams) : RequestM (RequestTask CodeWithInfos) :=
+  withWaitFindSnapAtPos params.pos fun snap => do
+    runTermElabM snap do
+      let name ← resolveGlobalConstNoOverloadCore params.id
+      let some c ← Meta.getConst? name
+        | throwThe RequestError ⟨.invalidParams, s!"no constant named '{name}'"⟩
+      Widget.ppExprTagged c.type
+```
+
+## Using infoview components
+
+Now that we have all we need on the server side, let's write the widget source. By importing
+`@leanprover/infoview`, widgets can render UI components used to implement the infoview itself.
+For example, the `<InteractiveCode>` component displays expressions with `term : type` tooltips
+as seen in the goal view. We will use it to implement our custom `#check` display.
+
+⚠️ WARNING: Like the other widget APIs, the infoview JS API is **unstable** and subject to breaking changes.
+
+The code below demonstrates useful parts of the API. To make RPC method calls, we use the `RpcContext`.
+The `useAsync` helper packs the results of a call into a `status` enum, the returned `val`ue in case
+the call was successful, and otherwise an `err`or. Based on the `status` we either display
+an `InteractiveCode`, or `mapRpcError` the error in order to turn it into a readable message.
+
+```javascript
+import * as React from 'react';
+const e = React.createElement;
+import { RpcContext, InteractiveCode, useAsync, mapRpcError } from '@leanprover/infoview';
+
+export default function(props) {
+  const rs = React.useContext(RpcContext)
+  const [name, setName] = React.useState('getType')
+
+  const [status, val, err] = useAsync(() =>
+    rs.call('getType', { id: name, pos: props.pos }), [name, rs, props.pos])
+
+  const type = status === 'fulfilled' ? val && e(InteractiveCode, {fmt: val})
+    : status === 'rejected' ? e('p', null, mapRpcError(err).message)
+      : e('p', null, 'Loading..')
+
+  const onChange = (event) => { setName(event.target.value) }
+  return e('div', null,
+    e('input', { value: name, onChange }),
+    ' : ',
+    type)
 }
 ```
 
-This JavaScript text must include `import * as React from "react"` in the imports and may not use JSX.
-The default export of the sourcetext must be a React component whose props are an RPC encoding.
-The React component may accept a props argument whose value will be determined for each particular widget instance (below).
-Widget sources may import the `@lean4/infoview` package ([todo] publish on NPM) in order to use
-components such as `InteractiveMessage` to display `MessageData` interactively.
+Finally we can try out the widget.
 
-## Using Lake to build your widgets
+```lean
+@[widget]
+def checkWidget : UserWidgetDefinition where
+  name := "#check as a service"
+  javascript := "<JS source above>"
 
-For larger projects, you can use Lake to create files that will be used as `widgetSource`.
-To learn how to do this, please view the readme of the [WidgetsMinimal sample](https://github.com/leanprover/lean4-samples/tree/main/WidgetsMinimal) ([todo] merge sample).
+#widget checkWidget .null
+```
+
+![`#check` as a service](images/widgets_caas.png)
+
+## Building widget sources
+
+While typing JavaScript inline is fine for a simple example, for real developments we want to use
+packages from NPM, a proper build system, and JSX. Thus, most actual widget sources are built with
+Lake and NPM. They consist of multiple files and may import libraries which don't work as ESModules
+by default. On the other hand a widget source is just a single string. Readers familiar with web
+development may already have guessed that to obtain such a string, we need a *bundler*. Two popular
+choices are [`rollup.js`](https://rollupjs.org/guide/en/) and [`esbuild`](https://esbuild.github.io/).
+If we go with `rollup.js`, to make a widget work with the infoview we need to:
+- Set [`output.format`](https://rollupjs.org/guide/en/#outputformat) to `'es'`.
+- [Externalize](https://rollupjs.org/guide/en/#external) `react`, `react-dom`, `@leanprover/infoview`.
+  These libraries are already loaded by the infoview so they should not be bundled.
+
+We provide a working build setup sample in [`Rubiks/rollup.config.js`](TODO merge).

src/Lean/Data/JsonRpc.lean

@@ -75,7 +75,7 @@ instance : ToJson ErrorCode := ⟨fun
   | ErrorCode.contentModified      => (-32801 : Int)
   | ErrorCode.requestCancelled     => (-32800 : Int)
   | ErrorCode.rpcNeedsReconnect    => (-32900 : Int)
-  | ErrorCode.workerExited        => (-32901 : Int)
+  | ErrorCode.workerExited         => (-32901 : Int)
   | ErrorCode.workerCrashed        => (-32902 : Int)⟩
 
 /-- Uses separate constructors for notifications and errors because client and server

src/Lean/Server/Requests.lean

@@ -8,23 +8,19 @@ import Lean.DeclarationRange
 
 import Lean.Data.Json
 import Lean.Data.Lsp
+import Lean.Elab.Command
 
 import Lean.Server.FileSource
 import Lean.Server.FileWorker.Utils
 
 import Lean.Server.Rpc.Basic
 
-/-! We maintain a global map of LSP request handlers. This allows user code such as plugins
-to register its own handlers, for example to support ITP functionality such as goal state
-visualization.
-
-For details of how to register one, see `registerLspRequestHandler`. -/
-
 namespace Lean.Server
 
 structure RequestError where
   code    : JsonRpc.ErrorCode
   message : String
+  deriving Inhabited
 
 namespace RequestError
 open JsonRpc
@@ -38,11 +34,13 @@ def methodNotFound (method : String) : RequestError :=
     message := s!"No request handler found for '{method}'" }
 
 def internalError (message : String) : RequestError :=
-  { code := ErrorCode.internalError, message := message }
+  { code := ErrorCode.internalError, message }
 
-instance : Coe IO.Error RequestError where
-  coe e := { code := ErrorCode.internalError
-             message := toString e }
+def ofException (e : Lean.Exception) : IO RequestError :=
+  return internalError (← e.toMessageData.toString)
+
+def ofIoError (e : IO.Error) : RequestError :=
+  internalError (toString e)
 
 def toLspResponseError (id : RequestID) (e : RequestError) : ResponseError Unit :=
   { id := id
@@ -65,31 +63,42 @@ structure RequestContext where
   initParams    : Lsp.InitializeParams
 
 abbrev RequestTask α := Task (Except RequestError α)
+abbrev RequestT m := ReaderT RequestContext <| ExceptT RequestError m
 /-- Workers execute request handlers in this monad. -/
 abbrev RequestM := ReaderT RequestContext <| EIO RequestError
 
-instance : Inhabited (RequestM α) :=
-  ⟨throw ("executing Inhabited instance?!" : RequestError)⟩
-
 instance : MonadLift IO RequestM where
-  monadLift x := x.toEIO fun e => (e : RequestError)
+  monadLift x := do
+    match ←  x.toBaseIO with
+    | .error e => throw <| RequestError.ofIoError e
+    | .ok v => return v
+
+instance : MonadLift (EIO Exception) RequestM where
+  monadLift x := do
+    match ←  x.toBaseIO with
+    | .error e => throw <| ← RequestError.ofException e
+    | .ok v => return v
 
 namespace RequestM
 open FileWorker
 open Snapshots
 
-def readDoc : RequestM EditableDocument := fun rc =>
+def readDoc [Monad m] [MonadReaderOf RequestContext m] : m EditableDocument := do
+  let rc ← readThe RequestContext
   return rc.doc
 
-def asTask (t : RequestM α) : RequestM (RequestTask α) := fun rc => do
-  let t ← EIO.asTask <| t rc
+def asTask (t : RequestM α) : RequestM (RequestTask α) := do
+  let rc ← readThe RequestContext
+  let t ← EIO.asTask <| t.run rc
   return t.map liftExcept
 
-def mapTask (t : Task α) (f : α → RequestM β) : RequestM (RequestTask β) := fun rc => do
+def mapTask (t : Task α) (f : α → RequestM β) : RequestM (RequestTask β) := do
+  let rc ← readThe RequestContext
   let t ← EIO.mapTask (f · rc) t
   return t.map liftExcept
 
-def bindTask (t : Task α) (f : α → RequestM (RequestTask β)) : RequestM (RequestTask β) := fun rc => do
+def bindTask (t : Task α) (f : α → RequestM (RequestTask β)) : RequestM (RequestTask β) := do
+  let rc ← readThe RequestContext
   EIO.bindTask t (f · rc)
 
 def waitFindSnapAux (notFoundX : RequestM α) (x : Snapshot → RequestM α)
@@ -100,7 +109,7 @@ def waitFindSnapAux (notFoundX : RequestM α) (x : Snapshot → RequestM α)
   | Except.error FileWorker.ElabTaskError.aborted =>
     throwThe RequestError RequestError.fileChanged
   | Except.error (FileWorker.ElabTaskError.ioError e) =>
-    throw (e : RequestError)
+    throw (RequestError.ofIoError e)
   | Except.ok none => notFoundX
   | Except.ok (some snap) => x snap
 
@@ -108,54 +117,63 @@ def waitFindSnapAux (notFoundX : RequestM α) (x : Snapshot → RequestM α)
 and if a matching snapshot was found executes `x` with it. If not found, the task executes
 `notFoundX`. -/
 def withWaitFindSnap (doc : EditableDocument) (p : Snapshot → Bool)
-  (notFoundX : RequestM β)
-  (x : Snapshot → RequestM β)
+    (notFoundX : RequestM β)
+    (x : Snapshot → RequestM β)
     : RequestM (RequestTask β) := do
+  let doc ← readDoc
   let findTask ← doc.cmdSnaps.waitFind? p
   mapTask findTask <| waitFindSnapAux notFoundX x
 
 /-- See `withWaitFindSnap`. -/
 def bindWaitFindSnap (doc : EditableDocument) (p : Snapshot → Bool)
-  (notFoundX : RequestM (RequestTask β))
-  (x : Snapshot → RequestM (RequestTask β))
+    (notFoundX : RequestM (RequestTask β))
+    (x : Snapshot → RequestM (RequestTask β))
     : RequestM (RequestTask β) := do
+  let doc ← readDoc
   let findTask ← doc.cmdSnaps.waitFind? p
   bindTask findTask <| waitFindSnapAux notFoundX x
 
-/-- Helper for running an Rpc request at a particular snapshot. -/
+/-- Create a task which waits for the snapshot containing `lspPos` and executes `f` with it.
+If no such snapshot exists, the request fails with an error. -/
 def withWaitFindSnapAtPos
-  (lspPos : Lean.Lsp.Position)
-  (f : Snapshots.Snapshot → RequestM α): RequestM (RequestTask α) := do
+    (lspPos : Lsp.Position)
+    (f : Snapshots.Snapshot → RequestM α)
+    : RequestM (RequestTask α) := do
   let doc ← readDoc
   let pos := doc.meta.text.lspPosToUtf8Pos lspPos
-  withWaitFindSnap
-    doc
-    (fun s => s.endPos >= pos)
-    (notFoundX := throw <| RequestError.mk .invalidParams s!"no snapshot found at {lspPos}")
-    f
+  withWaitFindSnap doc (fun s => s.endPos >= pos)
+    (notFoundX := throw ⟨.invalidParams, s!"no snapshot found at {lspPos}"⟩)
+    (x := f)
 
-open Lean Elab Command in
-/-- Use the command state in the given snapshot to run a `CommandElabM`.-/
-def runCommand (snap : Snapshots.Snapshot) (c : CommandElabM α) : RequestM α := do
-  let r ← read
-  let ctx : Command.Context := {
-    fileName := r.doc.meta.uri,
-    fileMap := r.doc.meta.text,
-    tacticCache? := snap.tacticCache,
-  }
-  let ea ← c.run ctx |>.run snap.cmdState |> EIO.toIO'
-  match ea with
-  | Except.ok (a, _s) => return a
-  | Except.error ex => do
-    throw <| RequestError.internalError <|← ex.toMessageData.toString
+open Elab.Command in
+def runCommandElabM (snap : Snapshot) (c : RequestT CommandElabM α) : RequestM α := do
+  let rc ← readThe RequestContext
+  match ← snap.runCommandElabM rc.doc.meta (c.run rc) with
+  | .ok v => return v
+  | .error e => throw e
 
-/-- Run a `CoreM` using the data in the given snapshot.-/
-def runCore (snap : Snapshots.Snapshot) (c : CoreM α) : RequestM α :=
-  runCommand snap <| Lean.Elab.Command.liftCoreM c
+def runCoreM (snap : Snapshot) (c : RequestT CoreM α) : RequestM α := do
+  let rc ← readThe RequestContext
+  match ← snap.runCoreM rc.doc.meta (c.run rc) with
+  | .ok v => return v
+  | .error e => throw e
+
+open Elab.Term in
+def runTermElabM (snap : Snapshot) (c : RequestT TermElabM α) : RequestM α := do
+  let rc ← readThe RequestContext
+  match ← snap.runTermElabM rc.doc.meta (c.run rc) with
+  | .ok v => return v
+  | .error e => throw e
 
 end RequestM
 
-/-! # The global request handlers table -/
+/-! # The global request handlers table
+
+We maintain a global map of LSP request handlers. This allows user code such as plugins
+to register its own handlers, for example to support ITP functionality such as goal state
+visualization.
+
+For details of how to register one, see `registerLspRequestHandler`. -/
 section HandlerTable
 open Lsp
 
@@ -215,7 +233,7 @@ def chainLspRequestHandler (method : String)
     let handle := fun j => do
       let t ← oldHandler.handle j
       let t := t.map fun x => x.bind fun j => FromJson.fromJson? j |>.mapError fun e =>
-        IO.userError s!"Failed to parse original LSP response for `{method}` when chaining: {e}"
+        .internalError s!"Failed to parse original LSP response for `{method}` when chaining: {e}"
       let params ← liftExcept <| parseRequestParams paramType j
       let t ← handler params t
       pure <| t.map <| Except.map ToJson.toJson
@@ -231,7 +249,9 @@ def routeLspRequest (method : String) (params : Json) : IO (Except RequestError
 
 def handleLspRequest (method : String) (params : Json) : RequestM (RequestTask Json) := do
   match (← lookupLspRequestHandler method) with
-  | none => throw (s!"internal server error: request '{method}' routed through watchdog but unknown in worker; are both using the same plugins?" : RequestError)
+  | none =>
+    throw <| .internalError
+      s!"request '{method}' routed through watchdog but unknown in worker; are both using the same plugins?"
   | some rh => rh.handle params
 
 end HandlerTable

src/Lean/Server/Snapshots.lean

@@ -71,6 +71,25 @@ def infoTree (s : Snapshot) : InfoTree :=
 def isAtEnd (s : Snapshot) : Bool :=
   Parser.isEOI s.stx || Parser.isExitCommand s.stx
 
+open Command in
+/-- Use the command state in the given snapshot to run a `CommandElabM`.-/
+def runCommandElabM (snap : Snapshot) (meta : DocumentMeta) (c : CommandElabM α) : EIO Exception α := do
+  let ctx : Command.Context := {
+    cmdPos := snap.beginPos,
+    fileName := meta.uri,
+    fileMap := meta.text,
+    tacticCache? := snap.tacticCache,
+  }
+  c.run ctx |>.run' snap.cmdState 
+
+/-- Run a `CoreM` computation using the data in the given snapshot.-/
+def runCoreM (snap : Snapshot) (meta : DocumentMeta) (c : CoreM α) : EIO Exception α :=
+  snap.runCommandElabM meta <| Command.liftCoreM c
+
+/-- Run a `TermElabM` computation using the data in the given snapshot.-/
+def runTermElabM (snap : Snapshot) (meta : DocumentMeta) (c : TermElabM α) : EIO Exception α :=
+  snap.runCommandElabM meta <| Command.liftTermElabM none c
+
 end Snapshot
 
 /-- Parses the next command occurring after the given snapshot

src/Lean/Widget/UserWidget.lean

@@ -95,16 +95,17 @@ structure GetWidgetSourceParams where
   pos : Lean.Lsp.Position
   deriving ToJson, FromJson
 
-open Lean.Server Lean RequestM in
+open Server in
 @[serverRpcMethod]
 def getWidgetSource (args : GetWidgetSourceParams) : RequestM (RequestTask WidgetSource) :=
   RequestM.withWaitFindSnapAtPos args.pos fun snap => do
-    let env := snap.cmdState.env
-    if let some id := widgetSourceRegistry.getState env |>.find? args.hash then
-      let d ← Lean.Server.RequestM.runCore snap <| getUserWidgetDefinition id
-      return {sourcetext := d.javascript}
-    else
-      throw <| RequestError.mk .invalidParams s!"No registered user-widget with hash {args.hash}"
+    RequestM.runCoreM snap do
+      let env ← getEnv
+      if let some id := widgetSourceRegistry.getState env |>.find? args.hash then
+        let d ← getUserWidgetDefinition id
+        return {sourcetext := d.javascript}
+      else
+        throwThe RequestError ⟨.invalidParams, s!"No registered user-widget with hash {args.hash}"⟩
 
 open Lean Elab