Zulip Chat Archive

Stream: general

Topic: Widget that reacts to Lean

Jovan Gerbscheid (Oct 26 2025 at 12:06):

For the rewrite suggestion tactic, rw??, there is the problem that it can take a while for the suggestions to load. This can be improved by using more paralellization, but it can also be improved by having the widget show that progress is happening, for example by showing a partial list of suggestions when only some of the suggestions have been computed.

My understanding is that there is no way for the Lean side of a widget to directly tell the JavaScript to reload, in the way that a setState() in React does. Instead we can write a component in ProofWidgets that periodically queries Lean whether anything has changed, and if so, then reload the widget. In particular the widget could store a reference to an IO.Ref Ξ±, together with the name of a Lean function that takes in this IO.Ref Ξ± and produces Option Html.

@πš πš˜πš“πšŒπš’πšŽπšŒπš‘ πš—πšŠπš πš›πš˜πšŒπš”πš’ is that right, and do you think that this would be a good idea for ProofWidgets?

Jovan Gerbscheid (Oct 26 2025 at 14:31):

Actually, I think the function that repeatedly checks if the IO.Ref has been modified can also be written on the Lean side.

So all that we need to add to ProofWidgets is a component that displays some Html, and simultaneously asks Lean for a new Html object. The Lean function might take some time, and it can either return a new Html object, or none, in which case the widget stops calling Lean.

πš πš˜πš“πšŒπš’πšŽπšŒπš‘ πš—πšŠπš πš›πš˜πšŒπš”πš’ (Oct 26 2025 at 20:46):

there is no way for the Lean side of a widget to directly tell the JavaScript to reload

The LSP protocol does support server->client notifications and requests. IIRC RequestM doesn't expose any API for sending notifications; it does allow requests via the ServerRequestEmitter, though I'm not sure whether user widgets can respond to those. Anyhow your idea of polling the Lean server multiple times sounds like it'd result in more understandable code.

πš πš˜πš“πšŒπš’πšŽπšŒπš‘ πš—πšŠπš πš›πš˜πšŒπš”πš’ (Oct 26 2025 at 20:51):

Are you using mk_rpc_widget% or also writing custom JS? If the former, one idea would be to extend mk_rpc_widget% to support signatures of the form MyProps β†’ RequestM (RequestTask (Html βŠ• CallMeLater Html)) where CallMeLater specifies a delay after which the function will be called again.

Jovan Gerbscheid (Oct 27 2025 at 00:35):

My current working version has the following TypeScript that repeatedly calls Lean. Since the Lean function does some polling, waiting for various Tasks to finish (interspersed with IO.sleep), there is no need to also have a delay on the JavaScript side. The Lean function thas is passed as RefreshPanelProps.next is tagged with @[server_rpc_method], but for some reason it doesn't work if I tag it @[server_rpc_method_cancellable]

export interface RefreshPanelProps {
  /** The initial HTML to display */
  initial: Html
  /** The Lean function to call next */
  next: Name
  /** A reference to a Lean object that will be passed to `next` */
  state: RpcPtr<''>
}

export interface IncrementalResult {
  /** The new HTML to display */
  html : Html
  /** Wether to try refreshing the HTML again */
  refresh : boolean
}
export interface WidgetStateProps {
  /** A reference to a Lean object that will be passed to `next` */
  ctx : RpcPtr<''>
}
export default function RefreshPanel(props: RefreshPanelProps): JSX.Element {
  const rs = useRpcSession()
  const [html, setHtml] = React.useState<Html>(props.initial)

  // Repeatedly call Lean to update
  React.useEffect(() => {
    let cancelled = false
    async function loop() {
      const result = await rs.call<WidgetStateProps, IncrementalResult>(props.next, { ctx: props.state })
      if (cancelled) return
      setHtml(result.html)
      if (result.refresh) loop()
    }
    loop()
    return () => { cancelled = true }
  }, [])
  return <HtmlDisplay html={html}/>
}

Jovan Gerbscheid (Oct 27 2025 at 00:38):

On the Lean side I can maintain a state by storing an IO.Ref in the WidgetStateProps

πš πš˜πš“πšŒπš’πšŽπšŒπš‘ πš—πšŠπš πš›πš˜πšŒπš”πš’ (Oct 27 2025 at 18:14):

That all makes sense. If you want to make a PR, it would be nice to have a general component that is parameterized over an RPC method with this general signature, perhaps as a new macro like mk_rpc_widget% (maybe we shouldn't tack too much functionality onto mk_rpc_widget%).

for some reason it doesn't work if I tag it @[server_rpc_method_cancellable]

Have a look at ProofWidgets.Cancellable. Cancellable RPC methods should be called using callCancellable from widget/src/cancellable.ts. I guess this is not available in the @leanprover-community/proofwidgets4 package, so maybe we should expose it. Are you using that package?

Jovan Gerbscheid (Oct 27 2025 at 23:21):

I have now implemented it slightly differently. Instead of passing a function (as a string), and a state (as a WithRpcRef) to JavaScript, I now just pass a Lean Task (as a WithRpcRef) to Javascript when I want to reload something. The Task returns Html, and optionally another Task, which can then be called again by JavaScript.

On the Lean side, this looks like this:

structure RefreshTask where
  go : Task (Except IO.Error (Html Γ— Option RefreshTask))
deriving TypeName

structure RefreshResult where
  html : Html
  refresh : Option (WithRpcRef RefreshTask)
  deriving RpcEncodable

@[server_rpc_method]
def runRefresh (task : WithRpcRef RefreshTask) : RequestM (RequestTask RefreshResult) :=
  RequestM.asTask do
    match task.val.go.get with
    | .error e => throw (.ofIoError e)
    | .ok (html, go) => return { html, refresh := ← go.mapM (WithRpcRef.mk Β·) }

structure RefreshComponentProps where
  initial : Html
  next : Name
  refresh : WithRpcRef RefreshTask
deriving RpcEncodable

@[widget_module]
def RefreshComponent : Component RefreshComponentProps where
  javascript :=

and on the JavaScript side it looks like this

export interface RefreshPanelProps {
  /** The initial HTML to display */
  initial: Html
  /** A Lean task for iteratively refreshing the HTML display */
  refresh: RpcPtr<''>
}

export interface IncrementalResult {
  /** The new HTML to display */
  html : Html
  refresh? : RpcPtr<''>
}

export default function RefreshPanel(props: RefreshPanelProps): JSX.Element {
  const rs = useRpcSession()
  const [html, setHtml] = React.useState<Html>(props.initial)

  // Repeatedly call Lean to update
  React.useEffect(() => {
    let cancelled = false
    async function loop(refresh: RpcPtr<''>) {
      const result = await rs.call<RpcPtr<''>, IncrementalResult>("runRefresh", refresh)
      if (cancelled) return
      setHtml(result.html)
      if (result.refresh) loop(result.refresh)
    }
    loop(props.refresh)
    return () => { cancelled = true }
  }, [])
  return <HtmlDisplay html={html}/>
}

This approach has the advantage of not forcing the use of a single function and state.

Additionally, by using Task, we have the benefit that the task can be spawned before stuff is sent over to JavaScript, instead of having to wait for JavaScript to call the Lean function.

πš πš˜πš“πšŒπš’πšŽπšŒπš‘ πš—πšŠπš πš›πš˜πšŒπš”πš’ (Oct 28 2025 at 03:51):

That sounds good, too. You can remove RefreshComponentProps.next now, right? I would also make RefreshComponentProps.refresh an Option so that the immediately-ready case is supported. And this is a matter of taste, but you could consider making RefreshTask.go just a Task (Html Γ— Option RefreshTask) for simplicity; you can still have a combinator which transforms Except IO.Error (Html Γ— Option RefreshTask) into this by producing some error message HTML.

Jovan Gerbscheid (Oct 28 2025 at 09:25):

That sounds good. Though I don't see the advantage of supporting the immediately ready case, since then you could just return the html directly rather than wrapping it in this component.

πš πš˜πš“πšŒπš’πšŽπšŒπš‘ πš—πšŠπš πš›πš˜πšŒπš”πš’ (Oct 28 2025 at 14:03):

I just had simplicity in mind - you could merge RefreshComponentProps and RefreshResult - but it seems fine either way.

Jovan Gerbscheid (Oct 28 2025 at 15:33):

Ah yes, it would be nice to merge them. But, I think another feature that would be nice is to allow the RefreshResult to say that the computation is finished, without providing any new html. This would make sense if rw?? was still checking some lemmas, but in the end it turned out that none of them were applicable. Then it would be silly to create and send the same Html to JavaScript again.

Jovan Gerbscheid (Oct 28 2025 at 16:32):

Another thing to think about would be cancellation, although I don't think it is super important for rw??, because the new version is pretty fast.

If I used @[server_rpc_method_cancellable] on runRefresh, this would mean that IO.checkCancelled in that task will tell whether the task was cancelled. However, the problem with runRefresh is that that it calls Task.get, which blocks the thread until the Task has evaluated, so it cannot really react to being cancelled. Instead, we should tell the Task directly that it was cancelled, so that it can act accordingly. I haven't looked too closely how ProofWidgets.CancellableTask works, which seems relevant to this.

The function I pass to mk_rpc_widget% is tagged with @[server_rpc_method_cancellable], but I'm not so sure that cancelling it (after it has already finished) would also cancel any child Task that it spawned.

Jovan Gerbscheid (Oct 28 2025 at 16:36):

I suppose I can just implement a function cancelRefresh which calls IO.cancel on the Task.

πš πš˜πš“πšŒπš’πšŽπšŒπš‘ πš—πšŠπš πš›πš˜πšŒπš”πš’ (Oct 28 2025 at 16:48):

If you don't want to rely on implicit task cancellation behaviour (probably a bad thing to rely on), I'd use a docs#IO.CancelToken.

Thomas Murrills (Oct 28 2025 at 16:57):

Whoa, this looks really cool! :D

One thing I’d love to be able to do eventually is show a loading throbber in the spot where new parts of the html are going to appear (e.g. at the bottom of the suggestion list, where the next suggestion will load in).

I’ve actually created a couple of React Lean logo throbbers for fun, which I could make public if they could be used like this! :)

Just curious, would this approach be able to handle that smoothly, without making the throbber start a new animation cycle each time we add a suggestion to the end? Or would that need a second iteration?

Jovan Gerbscheid (Oct 28 2025 at 17:37):

πš πš˜πš“πšŒπš’πšŽπšŒπš‘ πš—πšŠπš πš›πš˜πšŒπš”πš’ said:

I'd use a docs#IO.CancelToken.

Oh I seen now that e.g. whnf calls checkInterrupted (and not IO.checkCancelled), so it's looking at the IO.CancelToken in the CoreM context. So, I should make a (optional) IO.CancelToken, pass it to Javascript, and put it in my CoreM context wherever I'd like to support cancellation. And then I can have JavaScript, in case of cancellation, call a lean function that sets the cancel token.

This also has the advantage over IO.cancel that we can cancel all parallel tasks in one go.

Jovan Gerbscheid (Oct 28 2025 at 18:03):

Thomas Murrills said:

One thing I’d love to be able to do eventually is show a loading throbber in the spot where new parts of the html are going to appear

Yes, this is one nice advantage of the interactivity. The mathlib version of rw?? doesn't tell the user that anything is happening, it keeps saying rw??: Please shift-click an expression.. But the new version will say rw?? is searching for rewrite lemmas... when searching. And we could certainly add a throbber to this :smile:

I wouldn't worry too much about the throbber starting a new cycle with each reload, because the new results come in very fast, so a user wouldn't be able to keep track of the throbber anyways.

But, this can be achieved as follows. At the start we make a new let promise : IO.Promise Unit ← IO.Promise.new and make a RefreshComponent for the throbber that starts off as a throbber, and then awaits promise.result?. Then when you finish loading all results in another thread, you call promise.resolve (), which unblocks the promise.result?, allowing it to return and replace the throbber with an empty Html.

Jovan Gerbscheid (Oct 28 2025 at 19:34):

(To be clear, I've never used IO.Promise, but this is what the source code documentation says that it does)

Thomas Murrills (Oct 28 2025 at 19:47):

Ah, I think I seeβ€”so the throbber would be its own widget, separate from the updating list, essentially? Or do I have that wrong?

Thomas Murrills (Oct 28 2025 at 19:49):

Also, by the way, the results coming in fast is actually the case in which I think it would be most noticeable to restart the throbber each update! :grinning_face_with_smiling_eyes: We’d essentially see a still or slightly jittering image making its way down the page underneath the results.

Jovan Gerbscheid (Oct 28 2025 at 19:51):

The throbber would be a separate part of the Html tree. On the Lean side you would construct an Html tree which contains one component that shows the rewrite suggestions, and another component for the throbber, which could come before or after eachother. Both components would be a RefreshComponent.

Jovan Gerbscheid (Oct 28 2025 at 19:52):

Well, the results come in so fast that the throbber would be off the page immediately :sweat_smile:

Thomas Murrills (Oct 28 2025 at 19:52):

Jovan Gerbscheid said:

Well, the results come in so fast that the throbber would be off the page immediately :sweat_smile:

Oh, I see… :laughing:

Jovan Gerbscheid (Oct 29 2025 at 01:31):

Maybe the solution for the continuous throbber that I sketched above is overcomplicated, assuming that it is possible to have let statements in an Html tree. Because then you can just put let throbber := ... at the root of the Html tree, and refer to throbber in the RefreshComponent. But I have next to no experience with html, so I don't know.

Jovan Gerbscheid (Oct 29 2025 at 01:39):

I implemented the cancellation with IO.CancelToken. It works most of the time, but not always. I tested it with the help of an infinite loop and a dbg_trace.

  • If I double click (i.e. click and then un-click) an expression, then the cancel token won't be set. I presume this is because the JavaScript is never run in the first place, and hence it also cannot be cancelled.
  • If I click an expression, then reload the lean file (which stops the ongoing infinite loops), and wait for Lean to load again, then the same expression stays selected, so the tactic will run on it again. But if I now unselect that expression, the cancel token won't be set either.

πš πš˜πš“πšŒπš’πšŽπšŒπš‘ πš—πšŠπš πš›πš˜πšŒπš”πš’ (Oct 29 2025 at 02:04):

Jovan Gerbscheid said:

Maybe the solution for the continuous throbber that I sketched above is overcomplicated, assuming that it is possible to have let statements in an Html tree. Because then you can just put let throbber := ... at the root of the Html tree, and refer to throbber in the RefreshComponent. But I have next to no experience with html, so I don't know.

If all the in-progress Html objects that you send over to JS include a throbber component, its state will be preserved across renders. This is how React works in general (see here). You may have to set a key on the throbber to ensure React identifies it across renders.

πš πš˜πš“πšŒπš’πšŽπšŒπš‘ πš—πšŠπš πš›πš˜πšŒπš”πš’ (Oct 29 2025 at 02:05):

Jovan Gerbscheid said:

I implemented the cancellation with IO.CancelToken. It works most of the time, but not always. I tested it with the help of an infinite loop and a dbg_trace.

  • If I double click (i.e. click and then un-click) an expression, then the cancel token won't be set. I presume this is because the JavaScript is never run in the first place, and hence it also cannot be cancelled.
  • If I click an expression, then reload the lean file (which stops the ongoing infinite loops), and wait for Lean to load again, then the same expression stays selected, so the tactic will run on it again. But if I now unselect that expression, the cancel token won't be set either.

Hard to say what's going on without code.

Jovan Gerbscheid (Oct 29 2025 at 09:57):

Jovan Gerbscheid said:

I implemented the cancellation with IO.CancelToken. It works most of the time, but not always.

I managed to fix this on the Lean side by having a global ref of the most recent rw?? cancel token. Then each new call to rw?? cancels the previous:

initialize currentCancelToken : IO.Ref (Option IO.CancelToken) ←
  IO.mkRef none

At the start of the server_rpc_method in Lean I use

  if let some cancelTk ← currentCancelToken.get then
    cancelTk.set

And later

  currentCancelToken.set cancelTk

Henrik BΓΆving (Oct 29 2025 at 10:58):

So you're implicitly assuming here that there is only one rw?? in the document at any given time yes?

Jovan Gerbscheid (Oct 29 2025 at 10:59):

To be more precise, I'm assuming there is only one rw?? widget running in the infoview at any given time.

Jovan Gerbscheid (Oct 30 2025 at 01:05):

Although this is not indended to but used, I've tested having two different rw?? widgets in the infoview at the same time, and (after I was careful to use IO.Ref.modifyGet instead of a separate get and set) exactly one of the two widgets gets cancelled. The cancelled one originally said Error refreshing this component:Β internal exception #0, but I've now special cased it to say This component was cancelled.

πš πš˜πš“πšŒπš’πšŽπšŒπš‘ πš—πšŠπš πš›πš˜πšŒπš”πš’ (Oct 30 2025 at 01:09):

There is probably a way to refactor this to avoid any global refs by passing the cancel token around through RPC, no?

Jovan Gerbscheid (Oct 30 2025 at 01:14):

Yes, I am storing the cancel token in 2 places:

  • in a global ref in Lean
  • in the RefreshComponent (in a WithRpcRef)

The problem is that if I double click really fast, then the token passed around through RPC is lost.

Jovan Gerbscheid (Oct 30 2025 at 17:25):

I have made the PR now: ProofWidgets4#141

I tried to document the content as well as possible. I haven't added any tests so far. How does ProofWidgets usually go about testing? Or is the testing done in use cases in e.g. Mathlib?

Julian Berman (Oct 30 2025 at 18:49):

Adding a trivial demo to https://github.com/leanprover-community/ProofWidgets4/tree/main/ProofWidgets/Demos is super helpful for me when reverse engineering these to add to lean.nvim.

Jovan Gerbscheid (Oct 30 2025 at 22:51):

What sort of reverse engineering is this? Are you rewriting the TypeScript to some nvim compatible language?

Julian Berman (Oct 30 2025 at 22:52):

Correct, generally lean.nvim has to reimplement any widget typescript code in Lua.

Julian Berman (Oct 30 2025 at 22:52):

So it's helpful to see the minimal possible usage of things being added so that I can have a simple example to play with.

Julian Berman (Oct 30 2025 at 22:56):

If you're curious to see what that looks like, the ExprPresentation demo file for example, I literally just load and use as a test case: https://github.com/Julian/lean.nvim/blob/main/spec/widgets/proofwidgets_spec.lua#L31-L57 which gets me my reimplementation here: https://github.com/Julian/lean.nvim/blob/main/lua/proofwidgets/expr_presentation.lua

Patrick Massot (Oct 30 2025 at 23:07):

In general it is really useful if as much as possible is done on the Lean side and as little as possible on the JS side.

Jovan Gerbscheid (Nov 05 2025 at 01:56):

I have continued to work on this RefreshComponent, and I've now significantly redesigned it. With the previous approach, one would create a new task for each refreshing computation. Instead of that, the computation can now happen on the same thread, and it instead uses IO.Promise to notify the Javascript when an update has happened.

I've added a test file to the Demos folder with 3 demos that show the RefreshComponent in action.

(And the code is still in ProofWidgets4#141

Jovan Gerbscheid (Nov 05 2025 at 02:00):

An additions that I needed that seems like it doesn't really belong to Proofwidgets is the MonadDrop type class:

/--
The class `MonadDrop m n` allows a computation in monad `m` to be run in monad `n`.
For example, a `MetaM` computation can be ran in `EIO Exception`,
which can then be ran as a task using `EIO.asTask`.
-/
class MonadDrop (m : Type β†’ Type) (n : outParam <| Type β†’ Type) where
  /-- Translates an action from monad `m` into monad `n`. -/
  dropM {Ξ±} : m Ξ± β†’ m (n Ξ±)

export MonadDrop (dropM)

variable {m n : Type β†’ Type} [Monad m] [MonadDrop m n]

instance : MonadDrop m m where
  dropM := pure

instance {ρ} : MonadDrop (ReaderT ρ m) n where
  dropM act := fun ctx => dropM (act ctx)

instance {Οƒ} : MonadDrop (StateT Οƒ m) n where
  dropM act := do liftM <| dropM <| act.run' (← get)

instance {Ο‰ Οƒ} [MonadLiftT (ST Ο‰) m] : MonadDrop (StateRefT' Ο‰ Οƒ m) n where
  dropM act := do liftM <| dropM <| act.run' (← get)

Thomas Murrills (Nov 05 2025 at 02:10):

Hmm, can dropM always be given by Functor.map pure, or is it different? (I’m just looking at the types!)

Jovan Gerbscheid (Nov 05 2025 at 02:12):

Yes, it could be given by that, but the purpose of dropM is that the computation is moved to the inner monad, instead of leaving it in the outer monad, as would happen with Functor.map pure.

Jovan Gerbscheid (Nov 05 2025 at 02:20):

Oh and I still haven't understood why we need so many words nowadays to import things (i.e. public meta import). In the PR I've just used import so far.

Thomas Murrills (Nov 05 2025 at 02:39):

Ah, okay, I see! Makes sense. :)

Thomas Murrills (Nov 05 2025 at 03:01):

Jovan Gerbscheid said:

Oh and I still haven't understood why we need so many words nowadays to import things (i.e. public meta import). In the PR I've just used import so far.

There’s some relatively new documentation in the reference manual if you haven’t seen it yet, by the way; pointing it out because I was unaware of it until it was pointed out to me. :grinning_face_with_smiling_eyes:

Jovan Gerbscheid (Nov 07 2025 at 13:49):

@πš πš˜πš“πšŒπš’πšŽπšŒπš‘ πš—πšŠπš πš›πš˜πšŒπš”πš’, when do you think you could review the code?

Last updated: Dec 20 2025 at 21:32 UTC