From 4e2b3b8345f6cd1573dd1a4a01bff13add510826 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Tue, 2 Aug 2022 17:02:59 -0400 Subject: [PATCH] doc: move widgets chapter to Lean file --- doc/widgets.lean | 203 +++++++++++++++++++++++++++++++++++++++++++++++ doc/widgets.md | 174 +--------------------------------------- 2 files changed, 205 insertions(+), 172 deletions(-) create mode 100644 doc/widgets.lean diff --git a/doc/widgets.lean b/doc/widgets.lean new file mode 100644 index 0000000000..191d73aa3e --- /dev/null +++ b/doc/widgets.lean @@ -0,0 +1,203 @@ +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 [`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. +-/ + +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 `` 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', { 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] +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) +} +" + +#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/doc/widgets.md b/doc/widgets.md index 451e0f0b59..c674d80be5 100644 --- a/doc/widgets.md +++ b/doc/widgets.md @@ -1,175 +1,5 @@ -# 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. +(this chapter is rendered by Alectryon in the CI) ```lean -import Lean -open Lean Widget - -@[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 +{{#include widgets.lean}} ``` - -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) -} -``` - -Finally we can try out the widget. - -```lean -@[widget] -def checkWidget : UserWidgetDefinition where - name := "#check as a service" - javascript := "" - -#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).