-
Notifications
You must be signed in to change notification settings - Fork 444
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Add user widgets tutorial #1407
Merged
Merged
Changes from all commits
Commits
Show all changes
10 commits
Select commit
Hold shift + click to select a range
848204a
feat: widget tutorial and general RequestM lifts
Vtec234 dd73d87
doc: move widgets chapter to Lean file
Vtec234 4bdab83
chore: move tutorial to examples folder
Vtec234 98513fa
feat: add include_str
Vtec234 6d0edbd
feat: make include_str a builtin
Vtec234 67429de
hack: rm JavaScript snippet
Vtec234 4f73119
fix: unused arg
Vtec234 ecdea52
doc: clarify widget tutorial
Vtec234 8796e56
chore: move includeStr elaborator
Vtec234 eb1cee2
Merge branch 'widget-doc' of https://github.com/Vtec234/lean4 into wi…
Vtec234 File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,186 @@ | ||
import Lean | ||
open Lean Widget | ||
|
||
/-! | ||
# The user-widgets system | ||
|
||
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. | ||
|
||
![Rubik's cube](images/widgets_rubiks.png) | ||
|
||
## Trying it out | ||
|
||
To try it out, simply type in the following code and place your cursor over the `#widget` command. | ||
-/ | ||
|
||
@[widget] | ||
def helloWidget : UserWidgetDefinition where | ||
name := "Hello" | ||
javascript := " | ||
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 | ||
[`RubiksCube`](https://github.com/leanprover/lean4-samples/blob/main/RubiksCube/). | ||
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. Widget instances | ||
are stored in the *infotree* in the same manner as other information about the source file | ||
such as the type of every expression. In our example, the `#widget` command stores 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 | ||
|
||
Besides enabling us to create cool client-side visualizations, user widgets come with the ability | ||
to communicate with the Lean server. Thanks to this, they have the same metaprogramming capabilities | ||
as custom elaborators or the tactic framework. 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. | ||
-/ | ||
|
||
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. | ||
-/ | ||
|
||
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.name | ||
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. | ||
-/ | ||
|
||
@[widget] | ||
def checkWidget : UserWidgetDefinition where | ||
name := "#check as a service" | ||
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', { 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) | ||
} | ||
" | ||
|
||
/-! | ||
Finally we can try out the widget. | ||
-/ | ||
|
||
#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 must be a single, self-contained ESModule in the form | ||
of a 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. | ||
|
||
In the RubiksCube sample, we provide a working `rollup.js` build configuration in | ||
[rollup.config.js](https://github.com/leanprover/lean4-samples/blob/main/RubiksCube/widget/rollup.config.js). | ||
-/ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,5 @@ | ||
(this chapter is rendered by Alectryon in the CI) | ||
|
||
```lean | ||
{{#include widgets.lean}} | ||
``` |
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
This file was deleted.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
"contains" is a bit vague here. Could you say more about the value's lifetime regarding server and client?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I left that in but clarified widget instances a little above, is it better? In this case
contains
just means that wherever a widget instance is stored, we also store props.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Hah, now I understand why it's a JSON