diff --git a/doc/images/widgets_caas.png b/doc/images/widgets_caas.png new file mode 100644 index 0000000000..d6e09531e5 Binary files /dev/null and b/doc/images/widgets_caas.png differ diff --git a/doc/images/widgets_rubiks.png b/doc/images/widgets_rubiks.png new file mode 100644 index 0000000000..e0c0f1215d Binary files /dev/null and b/doc/images/widgets_rubiks.png differ diff --git a/doc/widgets.md b/doc/widgets.md index c471d211fc..451e0f0b59 100644 --- a/doc/widgets.md +++ b/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", "")])`. + +💡 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 `` 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 := "" -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). diff --git a/src/Lean/Data/JsonRpc.lean b/src/Lean/Data/JsonRpc.lean index dc42ce3611..066e354f54 100644 --- a/src/Lean/Data/JsonRpc.lean +++ b/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 diff --git a/src/Lean/Server/Requests.lean b/src/Lean/Server/Requests.lean index 27bf2ed6c6..32d8d28e4d 100644 --- a/src/Lean/Server/Requests.lean +++ b/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 diff --git a/src/Lean/Server/Snapshots.lean b/src/Lean/Server/Snapshots.lean index f3b6d77627..b157bd426a 100644 --- a/src/Lean/Server/Snapshots.lean +++ b/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 diff --git a/src/Lean/Widget/UserWidget.lean b/src/Lean/Widget/UserWidget.lean index b99b903719..6a193cbb84 100644 --- a/src/Lean/Widget/UserWidget.lean +++ b/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