RFC: User widgets

[Vtec234]

RFC for the user widgets system

Authors: @EdAyers, @Vtec234

Goals

The idea of user-widgets is to give Lean users the ability to write their own GUIs shown within the Lean infoview without having to muck around with custom versions of the infoview code.

The widgets in Lean 3 got some hype, but there were many limitations of the approach, the main one being that no user-written code ran 'client side' on the infoview.

With the Lean 4 extension, we want to instead let the infoview dynamically load React components from JavaScript served by the Lean server. This has the advantage of allowing users to bundle and use arbitrary JavaScript libraries within the infoview. For example, we can now do things like 3d rendering, diagram drawing, TeX rendering and so on without needing to modify the infoview. Moreover Lake integration makes building widget bundles from TypeScript + NPM modules nice and easy.

Proposal

The current prototype widget protocol can be found here.

JavaScript widgets

A widget source is a valid JavaScript ESModule which exports a React component. The module must include import * as React from 'react' in the imports. 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 (which we intend to publish on NPM) in order to use components such as InteractiveMessage to display MessageData interactively. The precise API surface exposed in @lean4/infoview is orthogonal to this RFC.

NB: While only JavaScript is officially supported, we do not actually require that a widget source be JavaScript. As such, other formats can be stored as widget sources and fetched by custom infoview implementations written in other languages.

Widget source storage

On the Lean side, we use the @[widgetSource] attribute on definitions of type String to register them as widget sources. A widget source registered with @[widgetSource] has a unique widgetSourceId : Name which is just the fully qualified definition name. Alternatively, instead of naming sources we could use content-addressing and associated each source with its hash.

We define the Lean.Widget.getWidgetSource RPC call with a widgetSourceId (or again, hash) argument to retrieve widget sources from the Lean server at a source position following the @[widgetSource] registration. On the infoview side, we treat the Lean server as a kind of content delivery network which can send us widget sources via getWidgetSource.

Associating widgets to positions

A widget instance consists of a widgetSourceId and props : Json. Widget instances are stored in the infotree as .ofCustomInfo json!{ widget: { widgetSourceId, props } }. (We could add a new .ofWidgetInfo, although .ofCustomInfo seems to suffice for now.) This method of storage means each widget instance is associated with a position range in the source code. saveWidget is a method that saves these to the infotree.

We add a Lean.Widget.getWidget RPC call which retrieves the widget instance, if one exists, at a position in the source code. The structure of the infotree makes it possible that multiple widgets may exist at the same cursor position, but currently this RPC just returns the most specific widget.

In the infoview, we add a new "widget" panel which, whenever the cursor position changes, makes a call to the Lean.Widget.getWidget. If a widget is returned, it then fetches the source with getWidgetSource and displays it. Note that JS sources can be many megabytes long due to bundled libraries. Because of this, it is important that getWidgetSource is not called frequently, so we cache widget sources in the client. The props from the widget instance are passed as props to the React component.

Restricting props to Json means that they cannot contain references to non-Json-serializable Lean objects such as contexts and expressions. However, widget sources have full access to the RPC interface, and users can write their own RPC methods to invoke from their widget sources. In all our experiments this sufficed for passing data around.

As for custom goal views, see below, but note that a "custom goal widget" can be implemented by placing a widget instance at the entire range of a by tactic script.

User widgets are entirely separate to the tactic state widget.

Note that this design doesn't let you place widgets within the Lean goal view. Instead, user widgets are entirely separate and live in their own panel of the infoview. The original design of user-widgets was to give lots of 'extension points' within the goal view where users could inject their own widgets. For example, in the type tooltips. However, this may become quite complex and it is not clear at the moment whether extension points of this generality are needed. We may reconsider it in the future.

We do propose one, specific, such extension point in #1223. There, a user can click somewhere within an expression in the infoview and is presented with a set of suggestions such as tactics/rewrites available at that expression.

Links

• WIP feat: user widgets vscode-lean4#194
• prototype npm-widget
• lean core PR tbd
• gitpod demo tbd

[david-christiansen]

How would users of non-Javascript-based editors use this feature? Could the Lean server also serve other formats, for example?

[gebner]

The precise API surface exposed in @lean4/infoview is orthogonal to this RFC.

Can you post a proposal for this API?

The current prototype widget protocol can be found here.

For the record, the RPC protocol seems to be the following (in some made-up syntax):

Lean.Widget.getWidget(pos: TextDocumentPositionParams)
 -> { id: Name, hash: UInt64, props: any } | undefined

Lean.Widget.getStaticJS({ widgetId: Name, pos: TextDocumentPositionParams })
 -> { javascript: string, hash: UInt64 }

(I really wish we could generate this kind of protocol API summary automatically.)

1. I'd simplify getStaticJS to getStaticJS(hash: UInt64) -> string.
2. The current ToJson UInt64 implementation is not safe for the default javascript JSON parser (which converts the number into a float).
3. getWidget should probably also return the range of the widget.
4. id is used both as the declaration name of the javascript as well as a user-facing identifier in the vscode extension. This should be split into two names.

Restricting props to Json means that they cannot contain references to non-Json-serializable Lean objects such as contexts and expressions.

Could we do something like (α : Type) × RpcEncoding α × α (maybe written StateT RpcSession Id Json to avoid universe issues)?

The original design of user-widgets was to give lots of 'extension points' within the goal view where users could inject their own widgets. For example, in the type tooltips. However, this may become quite complex and it is not clear at the moment whether extension points of this generality are needed. We may reconsider it in the future.

That's a good argument for associating widgets "only" to ranges for now. Is there anything we can do now to make it easier to add further extension points in the future? For example, right now widgets are expected to get additional information like goal states by querying at the document position (possible via custom RPC functions). This won't work if we add widgets in tooltips, etc.

We do propose one, specific, such extension point in #1223.

That's a red herring, right? #1223 says nothing about widgets. But it would of course be possible to add a getContextualWidget call.

[gebner]

How would users of non-Javascript-based editors use this feature? Could the Lean server also serve other formats, for example?

HTML is just as much of an issue as Javascript here. You really need a web browser to display these widgets as-is. Broadly speaking I see two ways to make it work for editors which do not have web browsers:

1. We can reimplement the GUI part of the widget in the editor plugin, reusing the exposed RPC functions. I'm pretty sure that some (non-graphical) widgets will get such an "aftermarket" implementation in lean.nvim.

2. A more brutal solution is to start a web server, serve (a part of) the vscode infoview implementation, and show it in a web browser. This should work in most editors.

Note that e.g. Emacs includes a web browser (if you enable the right configure options), so we could potentially port the vscode widget implementation to Emacs.

[david-christiansen]

Using Emacs, I would normally expect widgets to use all the usual Emacs UI conventions, rather than just embedding blobs of Web. I would fully expect to implement them using ordinary elisp, and there's no reason why that can't be graphical (though using different graphics primitives than a Web-based implementation, of course). The concern here was more that the code hosting on the server side not bake-in Javascript-only approaches. Your option 1 seems quite reasonable!

[EdAyers]

The way I see it, the use cases for widgets are heavily dependent on web. Eg this demo widget uses three.js to render a rubiks cube.

I don't think it's going to be possible to do this in emacs without a web browser.

[Vtec234]

The concern here was more that the code hosting on the server side not bake-in Javascript-only approaches.

The RFC references JavaScript as that is what we use, but no part of the server-side implementation is specific to it. So I renamed the RPC calls to avoid JS and added a note that other formats can be stored as widget sources. For example, ELisp that is then retrieved by an Emacs-specific infoview, or Lua (?) retrieved by lean.nvim.

Using Emacs, I would normally expect widgets to use all the usual Emacs UI conventions, rather than just embedding blobs of Web. I would fully expect to implement them using ordinary elisp, and there's no reason why that can't be graphical (though using different graphics primitives than a Web-based implementation, of course).

As an ex-long-time-Emacs-user, I am very sympathetic to this approach. However, I have found that pragmatically one can't get even close to competing with the resources that tech companies pour into browser engines, and that the open source community pours into JS libraries. So even for Emacs, in #737 I suggested the approach of embedding Webkit. It would be a lot of work, but I tried fairly hard to keep the infoview code more or less independent of VSCode for this purpose.