feat: user widgets

doc/SUMMARY.md

@@ -65,6 +65,7 @@
 - [Frequently Asked Questions](./faq.md)
 - [Significant Changes from Lean 3](./lean3changes.md)
 - [Syntax Highlighting Lean in LaTeX](./syntax_highlight_in_latex.md)
+- [User Widgets](./widgets.md)
 
 # Development
 

doc/widgets.md

@@ -0,0 +1,37 @@
+# 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
+import Lean
+open Lean Widget
+
+@[widget]
+def widget1 : UserWidgetDefinition := {
+  name := "my fancy widget"
+  javascript := "
+  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`.
+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).

src/Lean/Data/Parsec.lean

@@ -55,6 +55,11 @@ def attempt (p : Parsec α) : Parsec α := λ it =>
 instance : Alternative Parsec :=
 { failure := fail "", orElse }
 
+protected def run (p : Parsec α) (s : String) : Except String α :=
+  match p s.mkIterator with
+  | Parsec.ParseResult.success _ res => Except.ok res
+  | Parsec.ParseResult.error it err  => Except.error s!"offset {repr it.i.byteIdx}: {err}"
+
 def expectedEndOfInput := "expected end of input"
 
 @[inline]
@@ -86,6 +91,7 @@ def manyChars (p : Parsec Char) : Parsec String := manyCharsCore p ""
 @[inline]
 def many1Chars (p : Parsec Char) : Parsec String := do manyCharsCore p (←p).toString
 
+/-- Parses the given string. -/
 def pstring (s : String) : Parsec String := λ it =>
   let substr := it.extract (it.forward s.length)
   if substr = s then

src/Lean/Elab/InfoTree.lean

@@ -114,6 +114,18 @@ 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. -/
+  widgetId : Name
+  /-- Json representing the props to be loaded in to the component. -/
+  props : Json
+  deriving Inhabited
+
 def CustomInfo.format : CustomInfo → Format
   | i => Std.ToFormat.format i.json
 
@@ -127,6 +139,7 @@ inductive Info where
   | ofMacroExpansionInfo (i : MacroExpansionInfo)
   | ofFieldInfo (i : FieldInfo)
   | ofCompletionInfo (i : CompletionInfo)
+  | ofUserWidgetInfo (i : UserWidgetInfo)
   | ofCustomInfo (i : CustomInfo)
   deriving Inhabited
 
@@ -285,13 +298,17 @@ 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.widgetId}\n{Std.ToFormat.format info.props}"
+
 def Info.format (ctx : ContextInfo) : Info → IO Format
   | ofTacticInfo i         => i.format ctx
   | ofTermInfo i           => i.format ctx
   | ofCommandInfo i        => i.format ctx
   | 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 +318,7 @@ def Info.toElabInfo? : Info → Option ElabInfo
   | ofMacroExpansionInfo _ => none
   | ofFieldInfo _          => none
   | ofCompletionInfo _     => none
+  | ofUserWidgetInfo _     => none
   | ofCustomInfo _         => none
 
 /--

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

src/Lean/Server/Requests.lean

@@ -37,6 +37,9 @@ def methodNotFound (method : String) : RequestError :=
   { code := ErrorCode.methodNotFound
     message := s!"No request handler found for '{method}'" }
 
+def internalError (message : String) : RequestError :=
+  { code := ErrorCode.internalError, message := message }
+
 instance : Coe IO.Error RequestError where
   coe e := { code := ErrorCode.internalError
              message := toString e }
@@ -119,6 +122,37 @@ def bindWaitFindSnap (doc : EditableDocument) (p : Snapshot → Bool)
   let findTask ← doc.cmdSnaps.waitFind? p
   bindTask findTask <| waitFindSnapAux notFoundX x
 
+/-- Helper for running an Rpc request at a particular snapshot. -/
+def withWaitFindSnapAtPos
+  (lspPos : Lean.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
+
+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
+
+/-- 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
+
 end RequestM
 
 /- The global request handlers table. -/

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

src/Lean/Widget/UserWidget.lean

@@ -0,0 +1,193 @@
+/-
+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
+import Lean.Elab.Eval
+
+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 [manual entry](doc/widgets.md) above this declaration for more information on
+how to use the widgets system.
+
+-/
+structure WidgetSource where
+  /-- Sourcetext of the code to run.-/
+  sourcetext : String
+  deriving Inhabited, ToJson, FromJson
+
+/-- Use this structure and the `@[widget]` attribute to define your own widgets.
+
+```lean
+@[widget]
+def rubiks : UserWidgetDefinition :=
+  { name := "Rubiks cube app"
+    javascript := include_str ...
+  }
+```
+-/
+structure UserWidgetDefinition where
+  /-- Pretty name of user widget to display to the user. -/
+  name : String
+  /-- An ESmodule that exports a react component to render. -/
+  javascript: String
+  deriving Inhabited, ToJson, FromJson
+
+structure UserWidget where
+  id : Name
+  /-- Pretty name of widget to display to the user.-/
+  name : String
+  javascriptHash: UInt64
+  deriving Inhabited, ToJson, FromJson
+
+private abbrev WidgetSourceRegistry := SimplePersistentEnvExtension
+    (UInt64 × Name)
+    (Std.RBMap UInt64 Name compare)
+
+-- Mapping widgetSourceId to hash of sourcetext
+builtin_initialize userWidgetRegistry : MapDeclarationExtension UserWidget ← mkMapDeclarationExtension `widgetRegistry
+builtin_initialize widgetSourceRegistry : WidgetSourceRegistry ←
+  registerSimplePersistentEnvExtension {
+    name          := `widgetSourceRegistry
+    addImportedFn := fun xss => xss.foldl (Array.foldl (fun s n => s.insert n.1 n.2)) ∅
+    addEntryFn    := fun s n => s.insert n.1 n.2
+    toArrayFn     := fun es => es.toArray
+  }
+
+private unsafe def getUserWidgetDefinitionUnsafe
+  (decl : Name) : CoreM UserWidgetDefinition :=
+  evalConstCheck UserWidgetDefinition ``UserWidgetDefinition decl
+
+@[implementedBy getUserWidgetDefinitionUnsafe]
+private opaque getUserWidgetDefinition
+  (decl : Name) : CoreM UserWidgetDefinition
+
+private def attributeImpl : AttributeImpl where
+  name := `widget
+  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 defn ← getUserWidgetDefinition decl
+    let javascriptHash := hash defn.javascript
+    let env := userWidgetRegistry.insert env decl {id := decl, name := defn.name, javascriptHash}
+    let env := widgetSourceRegistry.addEntry env (javascriptHash, decl)
+    setEnv <| env
+
+builtin_initialize registerBuiltinAttribute attributeImpl
+
+/-- Input for `getWidgetSource` RPC. -/
+structure GetWidgetSourceParams where
+  /-- The hash of the sourcetext to retrieve. -/
+  hash: UInt64
+  pos : Lean.Lsp.Position
+  deriving ToJson, FromJson
+
+open Lean.Server Lean 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 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}"
+
+open Lean Elab
+
+/--
+  Try to retrieve the `UserWidgetInfo` at a particular position.
+-/
+def widgetInfosAt? (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
+
+/-- UserWidget accompanied by component props. -/
+structure UserWidgetInstance extends UserWidget where
+  /-- Arguments to be fed to the widget's main component. -/
+  props : Json
+  /-- The location of the widget instance in the Lean file. -/
+  range? : Option Lsp.Range
+  deriving ToJson, FromJson
+
+/-- Output of `getWidgets` RPC.-/
+structure GetWidgetsResponse where
+  widgets : Array UserWidgetInstance
+  deriving ToJson, FromJson
+
+open Lean Server RequestM in
+/-- Get the `UserWidget`s present at a particular position. -/
+@[serverRpcMethod]
+def getWidgets (args : Lean.Lsp.Position) : RequestM (RequestTask (GetWidgetsResponse)) := do
+  let doc ← readDoc
+  let filemap := doc.meta.text
+  let pos := filemap.lspPosToUtf8Pos args
+  withWaitFindSnapAtPos args fun snap => do
+    let env := snap.env
+    let ws := widgetInfosAt? filemap snap.infoTree pos
+    let ws ← ws.toArray.mapM (fun (w : UserWidgetInfo) => do
+      let some widget := userWidgetRegistry.find? env w.widgetId
+        | throw <| RequestError.mk .invalidParams s!"No registered user-widget with id {w.widgetId}"
+      return {
+        widget with
+        props := w.props
+        range? := String.Range.toLspRange filemap <$> Syntax.getRange? w.stx
+      })
+    return {widgets := ws}
+
+/-- Save a user-widget instance to the infotree.
+    The given `widgetId` should be the declaration name of the widget definition. -/
+def saveWidgetInfo [Monad m] [MonadEnv m] [MonadError m] [MonadInfoTree m] (widgetId : Name) (props : Json) (stx : Syntax):  m Unit := do
+  let info := Info.ofUserWidgetInfo {
+    widgetId := widgetId
+    props := props
+    stx := stx
+  }
+  pushInfoLeaf info
+
+/-!  # Widget command
+
+Use `#widget <widgetname> <props>` to display a widget.
+-/
+
+syntax (name := widgetCmd) "#widget " ident term : command
+
+open Lean Lean.Meta Lean.Elab Lean.Elab.Term in
+private unsafe def evalJsonUnsafe (stx : Syntax) : TermElabM Json :=
+  Lean.Elab.Term.evalTerm Json (mkConst ``Json) stx
+
+@[implementedBy evalJsonUnsafe]
+private opaque evalJson (stx : Syntax) : TermElabM Json
+
+open Elab Command in
+
+/-- Use this to place a widget. Useful for debugging widgets. -/
+@[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
+  | _ => throwUnsupportedSyntax
+
+end Lean.Widget

src/Std/Data/RBMap.lean

@@ -243,6 +243,8 @@ def RBMap (α : Type u) (β : Type v) (cmp : α → α → Ordering) : Type (max
 instance (α : Type u) (β : Type v) (cmp : α → α → Ordering) : EmptyCollection (RBMap α β cmp) :=
   ⟨RBMap.empty⟩
 
+instance (α : Type u) (β : Type v) (cmp : α → α → Ordering) : Inhabited (RBMap α β cmp) := ⟨∅⟩
+
 namespace RBMap
 variable {α : Type u} {β : Type v} {σ : Type w} {cmp : α → α → Ordering}
 

tests/common.sh

@@ -28,7 +28,7 @@ function compile_lean {
 function exec_capture {
     # mvar suffixes like in `?m.123` are deterministic but prone to change on minor changes, so strip them
     # also strip intermittent "building '/nix/store/..." messages
-    LEAN_BACKTRACE=0 "$@" 2>&1 | perl -pe 's/(\?\w)\.[0-9]+/\1/g;s!building '\''/nix/.*\n!!g' > "$f.produced.out"
+    LEAN_BACKTRACE=0 "$@" 2>&1 | perl -pe 's/(\?(\w|_\w+))\.[0-9]+/\1/g;s!building '\''/nix/.*\n!!g' > "$f.produced.out"
 }
 
 # Remark: `${var+x}` is a parameter expansion which evaluates to nothing if `var` is unset, and substitutes the string `x` otherwise.