From 6b8402ff6594eb4708d3ab1e1daa8ad24799ad94 Mon Sep 17 00:00:00 2001 From: "E.W.Ayers" Date: Wed, 22 Jun 2022 12:14:39 -0400 Subject: [PATCH] feat: user widgets See #1225 --- doc/widgets.md | 58 +++++++++++ src/Lean/Elab/InfoTree.lean | 23 +++++ src/Lean/Server/InfoUtils.lean | 1 + src/Lean/Server/Requests.lean | 12 +++ src/Lean/Widget.lean | 1 + src/Lean/Widget/UserWidget.lean | 170 ++++++++++++++++++++++++++++++++ 6 files changed, 265 insertions(+) create mode 100644 doc/widgets.md create mode 100644 src/Lean/Widget/UserWidget.lean diff --git a/doc/widgets.md b/doc/widgets.md new file mode 100644 index 0000000000000..c7fbd925eeef7 --- /dev/null +++ b/doc/widgets.md @@ -0,0 +1,58 @@ +# 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. + +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. + +## How to write your own user-widgets + +You can write your own user-widgets using the `@[widgetSource]` attribute: + +```lean +@[widgetSource] +def widget1 : String := ` + import * as React from "react"; + export default function (props) { + return React.createElement("p", {}, "hello") + }` +``` + +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. + +## Using Lake to build your widgets + +For larger projects, you can use lake to create files that will be used as `widgetSource`. +Here is an example lakefile snippet that sets this up. +Your npm javascript project lives in a subfolder called `./widget` whose build process generates a single file `widget/dist/index.js`. + +```lean +-- ./lakefile.lean + +def jsTarget (pkgDir : FilePath) : FileTarget := + let jsFile := pkgDir / "widget/dist/index.js" + let srcFiles := inputFileTarget <| pkgDir / "widget/src/index.tsx" + fileTargetWithDep jsFile srcFiles fun _srcFile => do + proc { + cmd := "npm" + args := #["install"] + cwd := some <| pkgDir / "widget" + } + proc { + cmd := "npm" + args := #["run", "build"] + cwd := some <| pkgDir / "widget" + } + +package MyPackage (pkgDir) { + extraDepTarget := jsTarget pkgDir |>.withoutInfo + ... +} + +... +``` diff --git a/src/Lean/Elab/InfoTree.lean b/src/Lean/Elab/InfoTree.lean index 8f3cfe7cea288..2c21b9154ee10 100644 --- a/src/Lean/Elab/InfoTree.lean +++ b/src/Lean/Elab/InfoTree.lean @@ -114,6 +114,23 @@ structure CustomInfo where json : Json deriving Inhabited +/-- 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 + stx : Syntax + /-- Id of `WidgetSource` object to use. -/ + widgetSourceId : Name + /-- Json representing the props to be loaded in to the component. + + [todo] how to support Rpc encoding of expressions etc? + -/ + props : Json + /-- Hash of the `WidgetSource` code to use. -/ + hash : String + deriving Inhabited + def CustomInfo.format : CustomInfo → Format | i => Std.ToFormat.format i.json @@ -127,6 +144,7 @@ inductive Info where | ofMacroExpansionInfo (i : MacroExpansionInfo) | ofFieldInfo (i : FieldInfo) | ofCompletionInfo (i : CompletionInfo) + | ofUserWidgetInfo (i : UserWidgetInfo) | ofCustomInfo (i : CustomInfo) deriving Inhabited @@ -285,6 +303,9 @@ def MacroExpansionInfo.format (ctx : ContextInfo) (info : MacroExpansionInfo) : let output ← ctx.ppSyntax info.lctx info.output return f!"Macro expansion\n{stx}\n===>\n{output}" +def UserWidgetInfo.format (info : UserWidgetInfo) : Format := + f!"UserWidget {info.widgetSourceId}\n{Std.ToFormat.format info.props}" + def Info.format (ctx : ContextInfo) : Info → IO Format | ofTacticInfo i => i.format ctx | ofTermInfo i => i.format ctx @@ -292,6 +313,7 @@ def Info.format (ctx : ContextInfo) : Info → IO Format | ofMacroExpansionInfo i => i.format ctx | ofFieldInfo i => i.format ctx | ofCompletionInfo i => i.format ctx + | ofUserWidgetInfo i => pure <| UserWidgetInfo.format i | ofCustomInfo i => pure <| Std.ToFormat.format i def Info.toElabInfo? : Info → Option ElabInfo @@ -301,6 +323,7 @@ def Info.toElabInfo? : Info → Option ElabInfo | ofMacroExpansionInfo _ => none | ofFieldInfo _ => none | ofCompletionInfo _ => none + | ofUserWidgetInfo _ => none | ofCustomInfo _ => none /-- diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean index f055e01b7b8c3..294192d1b4f71 100644 --- a/src/Lean/Server/InfoUtils.lean +++ b/src/Lean/Server/InfoUtils.lean @@ -90,6 +90,7 @@ def Info.stx : Info → Syntax | ofFieldInfo i => i.stx | ofCompletionInfo i => i.stx | ofCustomInfo i => i.stx + | ofUserWidgetInfo i => i.stx def Info.lctx : Info → LocalContext | Info.ofTermInfo i => i.lctx diff --git a/src/Lean/Server/Requests.lean b/src/Lean/Server/Requests.lean index e4588cf6c59e6..aee017e092c0a 100644 --- a/src/Lean/Server/Requests.lean +++ b/src/Lean/Server/Requests.lean @@ -119,6 +119,18 @@ def bindWaitFindSnap (doc : EditableDocument) (p : Snapshot → Bool) let findTask ← doc.allSnaps.waitFind? p bindTask findTask <| waitFindSnapAux notFoundX x +/-- Helper for running an Rpc request at a particular snapshot. -/ +def withWaitFindSnapAtPos + (lspPos : Lean.Lsp.TextDocumentPositionParams) + (f : Snapshots.Snapshot → RequestM α): RequestM (RequestTask α) := do + let doc ← readDoc + let pos := doc.meta.text.lspPosToUtf8Pos lspPos.position + withWaitFindSnap + doc + (fun s => s.endPos >= pos) + (notFoundX := throw $ RequestError.mk JsonRpc.ErrorCode.invalidRequest s!"no snapshot found at {lspPos}") + f + end RequestM /- The global request handlers table. -/ diff --git a/src/Lean/Widget.lean b/src/Lean/Widget.lean index 4345d487dd7a4..9a51cfa25b97f 100644 --- a/src/Lean/Widget.lean +++ b/src/Lean/Widget.lean @@ -8,3 +8,4 @@ import Lean.Widget.InteractiveCode import Lean.Widget.InteractiveDiagnostic import Lean.Widget.InteractiveGoal import Lean.Widget.TaggedText +import Lean.Widget.UserWidget diff --git a/src/Lean/Widget/UserWidget.lean b/src/Lean/Widget/UserWidget.lean new file mode 100644 index 0000000000000..8338f33c1e689 --- /dev/null +++ b/src/Lean/Widget/UserWidget.lean @@ -0,0 +1,170 @@ +/- +Copyright (c) 2022 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Authors: E.W.Ayers +-/ +import Lean.Widget.Basic +import Lean.Data.Json +import Lean.Environment +import Lean.Server + +open Lean + +namespace Lean.Widget + +/-- A custom piece of code that is run on the editor client. + +The editor can use the `Lean.Widget.getWidgetSource` RPC method to +get this object. + +See the [tutorial](doc/widgets.md) above this declaration for more information on +how to use the widgets system. + +-/ +structure WidgetSource where + /-- Unique identifier for the widget. -/ + widgetSourceId : Name + /-- Sourcetext of the code to run.-/ + sourcetext : String + hash : String := toString $ hash sourcetext + deriving Inhabited, ToJson, FromJson + +namespace WidgetSource + +builtin_initialize widgetSourceRegistry : MapDeclarationExtension WidgetSource ← mkMapDeclarationExtension `widgetSourceRegistry + +private unsafe def attributeImplUnsafe : AttributeImpl where + name := `widgetSource + descr := "Mark a string as static code that can be loaded by a widget handler." + applicationTime := AttributeApplicationTime.afterCompilation + add decl _stx _kind := do + let env ← getEnv + let value ← evalConstCheck String ``String decl + setEnv <| widgetSourceRegistry.insert env decl {widgetSourceId := decl, sourcetext := value} + +@[implementedBy attributeImplUnsafe] +opaque attributeImpl : AttributeImpl + +/-- Find the WidgetSource for given widget id. -/ +protected def find? (env : Environment) (id : Name) : Option WidgetSource := + widgetSourceRegistry.find? env id + +/-- Returns true if the environment contains the given widget id. -/ +protected def contains (env : Environment) (id : Name) : Bool := + widgetSourceRegistry.contains env id + +/-- Gets the hash of the static javascript string for the given widget id, or throws if +there is no static javascript registered. -/ +def getHash [MonadEnv m] [Monad m] [MonadError m] (id : Name) : m String := do + let env ← getEnv + let some j := WidgetSource.find? env id | throwError "No code found for {id}." + return j.hash + +builtin_initialize registerBuiltinAttribute attributeImpl + +end WidgetSource + +structure GetWidgetSourceParams where + widgetSourceId : Name + pos : Lean.Lsp.TextDocumentPositionParams + deriving ToJson, FromJson + +open Lean.Server Lean + +open RequestM in +@[serverRpcMethod] +def getWidgetSource (args : GetWidgetSourceParams) : RequestM (RequestTask WidgetSource) := + RequestM.withWaitFindSnapAtPos args.pos fun snap => do + let env := snap.cmdState.env + if let some w := WidgetSource.find? env args.widgetSourceId then + return w + else + throw (RequestError.mk JsonRpc.ErrorCode.invalidParams s!"No registered user-widget with name {args.widgetSourceId}") + +open Lean Elab + +/-- + Try to retrieve the `UserWidgetInfo` at a particular position. +-/ +partial def widgetInfoAt? (text : FileMap) (t : InfoTree) (hoverPos : String.Pos) : List UserWidgetInfo := + t.deepestNodes fun + | _ctx, i@(Info.ofUserWidgetInfo wi), _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 wi + else + failure + | _, _, _ => none + +structure UserWidgetInfoNoStx where + widgetSourceId : Name + hash : String + props : Json + -- [todo] you can't toJson syntax yet. + -- once we can this class can be deleted and replaced with UserWidgetInfo + -- stx : Syntax + range? : Option Lsp.Range + deriving ToJson, FromJson + +structure GetWidgetInfosResponse where + infos : Array UserWidgetInfoNoStx + deriving ToJson, FromJson + +open RequestM in +/-- Get the UserWidgetInfos present at a particular position. -/ +@[serverRpcMethod] +def getWidgetInfos (args : Lean.Lsp.TextDocumentPositionParams) : RequestM (RequestTask (GetWidgetInfosResponse)) := do + let doc ← readDoc + let filemap := doc.meta.text + let pos := filemap.lspPosToUtf8Pos args.position + withWaitFindSnapAtPos args fun snap => do + let ws := widgetInfoAt? filemap snap.infoTree pos + let ws := ws.toArray.map (fun w => { + widgetSourceId := w.widgetSourceId, + hash := w.hash, + props := w.props, + range? := String.Range.toLspRange filemap <$> Syntax.getRange? w.stx, + }) + return {infos := ws} + +/-- Save a user-widget instance to the infotree. -/ +def saveWidgetInfo [Monad m] [MonadEnv m] [MonadError m] [MonadInfoTree m] (widgetSourceId : Name) (props : Json) (stx : Syntax): m Unit := do + let hash ← WidgetSource.getHash widgetSourceId + let info := Info.ofUserWidgetInfo { + widgetSourceId := widgetSourceId, + hash := hash, + props := props, + stx := stx, + } + pushInfoLeaf info + +/-! +# Widget command + +Use this to place a widget. Useful for debugging widgets. +-/ + +syntax (name := widgetCmd) "#widget " ident term : command + +private unsafe def evalJsonUnsafe (stx : Syntax) : TermElabM Json := do + let e ← Term.elabTerm stx (mkConst ``Json) + let e ← Meta.instantiateMVars e + Term.evalExpr Json ``Json e + +@[implementedBy evalJsonUnsafe] +private opaque evalJson (stx : Syntax) : TermElabM Json + +open Elab Command in +@[commandElab widgetCmd] def elabWidgetCmd : CommandElab := fun + | stx@`(#widget $id:ident $props) => do + let props : Json ← runTermElabM none (fun _ => evalJson props) + saveWidgetInfo id.getId props stx + return () + | _ => throwUnsupportedSyntax + + +end Lean.Widget