feat: RefreshComponent

[JovanGerb]

This PR defines RefreshComponent, which allows you to have a refreshing HTML display, which updates whenever the given RefreshTask returns a new HTML.

For cancellation, we store an Option IO.CancelToken. This could be generalized to storing an arbitrary IO Unit function, but I don't think that would be very useful.

[dranov]

In Veil, we have a need for widgets where the data is provided incrementally. Do you intend to merge this (or a similar solution) in the near future?

[JovanGerb]

I just opened the demo file from this PR, and did the countToTen demo, and as you can see whenever I reopen the infoview, the numbers flicker a bit. This is what I mean with the glitching.

WidgetGlitch.mp4

[Vtec234]

I am seeing this in the countToTen demo. To reproduce, uncomment line 33, then check that the counter on line 30 is running, then uncomment line 36. Now line 30 is cancelled. It seems worrying since no shared cancel token is explicitly created here.

[JovanGerb]

Aha interesting! Although it's true that no cancel token is created explicitly, we are implicitly passing around the cancel token that was given to the command in question.

Apparently this cancel token from line 30 gets set when (un)commenting line 36. I find this a bit surprising. I'd have to look more carefully into how/where the cancel tokens usually get passed around.

[Vtec234]

Could this just be From/ToJson? We usually don't impl RpcEncodable directly for types that don't do something with RPC.

[JovanGerb]

The reason for this is that I want to be able to have an RPC method that doesn't return anything, called from JavaScript. And the @[server_rpc_method] attribute requires the RpcEncodable instance. Alternatively I'd have to return a String or something else, and then throw it away.

[Vtec234]

Wdym by 'reloaded/unloaded' here? Is the situation just that a tactic that saves this widget (and launches the thread) is elaborated, then we make an edit, and it gets re-elaborated while leaving the previous thread alive? If so, is it not possible to reuse the standard tactic cancellation mechanism? E.g. what happens if you pass the CoreM cancel token instead of one created manually?

[JovanGerb]

I've updated the description to be more clear. The issue is when clicking on expressions in the goal, every shift-click generates a call to mkGoalRefreshComponent. When shift-clicking as fast as possible, there is not enough time for each of the intermediate widgets to load.

[Vtec234]

The issue is when clicking on expressions in the goal, every shift-click generates a call to mkGoalRefreshComponent.

Ah, if doing that you could also create/cancel cancellation tokens in the outer function (e.g. in cycleSelections). Then you probably wouldn't need the global cancel token map.

[Vtec234]

E.g. what happens if you pass the CoreM cancel token instead of one created manually?

I'm still wondering about this. In particular w.r.t. to "when the infoview gets closed, cancelRefresh isn't run, and I don't know how to fix this." Using the CoreM token wouldn't cause anything to happen when the infoview is closed, of course, but I think we don't care about that. Mainly, we should ensure that no more than one RefreshComponent thread chain is alive at any given time.

[JovanGerb]

Well, my solution with storing the cancel token in a IO.Ref ensures exactly that: whenever a new RefreshComponent thread is started, it cancels the previous one. So there can be at most one alive at any given time.

[JovanGerb]

This form of cancelling is only used for widgets like cycleSelections, where the widget depends on the selections in the goal. I think that there it makes sense to only load the widget that relates to the most recently selected selection.

For try? we instead would use the cancel token that we get implicitly in elaboration. (But that suffers from the issue that you noted above in the countToTen example)

[Vtec234]

I would expect to be able to interact with multiple goals at once; let's just not use the global state.

Screen.Recording.2025-12-09.at.1.02.35.PM.mov

[JovanGerb]

so you can put an IO.Ref in the props

I tried this, but it looks like I need a ToJson instance. But there is only a RpcEncodable instance for WithRpcRef (IO.Ref IO.CancelToken), not ToJson. This is because I think it should go in the json object in

elab stx:"cycleSelections" : tactic => do
  Widget.savePanelWidgetInfo (hash cycleComponent.javascript) (pure <| json% {}) stx

[Vtec234]

The pure <| json% {} is a StateT RpcStore computation, and you should be able to call rpcEncode in there.

[JovanGerb]

@Vtec234, now with the cancellation in the way that you suggested for refreshing panel widgets (passing a IO.Ref IO.CancelToken to the widget, such that each reload cancels the previous one), there is still a problem. It is now possible, e.g. in the cycleSelections demo, to unload the widget without the cancel token being triggered at all:

• Interact with the widget to get it to start its loop.
• Press ctrl + / to comment out the tactic/command.

Now, the loop is still going, but the reference to the corresponding cancel token has been dropped.

I think what should happen is that instead of replacing the implicit cancel token (which we get in elaboration) with this new cancel token, we should stop if either of the cancel tokens was set. That is, we should stop if (1) the user made a new selection in the goal, or (2) if the relevant tactic gets removed or re-elaborated. Currently we just react to (1).

Unfortunately, I don't think it is possible to merge two cancel tokens, and unfortunately, Core.Context stores an Option IO.CancelToken instead of List IO.CancelToken. I think changing this in core would be the easiest fix here.

[JovanGerb]

For the flickering that can be seen in the video, when the message disappears, this is actually the <></> that is the initial/default value for the HTML (which can be seen at the end of the RefreshComponent implementation in TypeScript).

In an earlier version of this widget, instead of disappearing for a bit, the message would change into whatever the initial HTML was set to, which gave a more jarring effect.

[JovanGerb]

I've now made some changes so that each panel widget gets to have its own cancellation of computations of previous selections.

In the demo I now also discovered a bug in Lean.SubExpr.GoalsLocation.saveExprWithCtx: it forgot to use instantiateMVars, which I fixed here as well.

What is remaining is to figure out how to safely have cancellation of widgets like #html countToTen. This is not my main use case, so it is not super important to me. But I think this cancellation is necessary for tactics like try? and hint to work without performance hiccups. The current problem is that if you would call e.g. try?, and then do some changes lower down in the file while try? was still busy, it cancels the try? computation. But if try? has already finished by that time, the result stays up. So I think the problem isn't too terrible.

[dranov]

HI @JovanGerb. Thanks for your work!

We have been using your code in Veil to incrementally display verification results, but found that we had to rewrite the code quite significantly, as the current implementation runs out of stack space (stack overflow) in long-running widgets (on the order of 5-15 minutes), due to having recursive calls in non-tail positions.

Basically, we rewrote the code to use explicit loops rather than recursion. We also removed ReaderT and withReader (which introduces a new stack frame).

We might have lost some of the generality that's necessary for your use-cases with our approach, but I wanted to highlight the issue and a potential solution. Our code is here.

[JovanGerb]

@dranov, thanks for you report! I did indeed not think about stack overflow problems, because in my use case the number of refreshes is fairly small.

I've now refactored my code so that it can be used naturally in a repeat do block instead of recursively, thus avoiding stack overflows over time. And it turns out that this way of implementing it is actually a lot shorter 😄

[Vtec234]

Thanks again for the PR @JovanGerb, and sorry that it's taking a while. I noticed that it still has the issue I mentioned above, namely that if you open cycleSelections twice, one of the widgets will cancel the other. I think cancellation needs to be implemented reliably for this to have good UX. Luckily Lean already includes RequestM.checkCancelled, it just wasn't available to widgets. I have now made a PR to the infoview exposing the core cancellation machinery, and we should be able to implement this PR in terms of that.

[JovanGerb]

I did implement the fix that you suggested, so if you open cycleSelections twice, it will now be able to run twice in parallel. It seems though that I forgot to update the text in the test file - it was still describing the old behaviour.

I have now added explanations for the two main limitations. I don't really understand what the changes in your new PR do. Will it solve one of these limitations?

[JovanGerb]

By the way, the fact that @[server_rpc_method_cancellable] exists is a bit confusing, now that there are all these different ways of doing cancellation. Should it be deprecated?

[Vtec234]

I did implement the fix that you suggested, so if you open cycleSelections twice, it will now be able to run twice in parallel.

I just tried it again on a fresh clone to be sure, and it still behaves as in here when the same position is opened twice (e.g. the cursor is there, and also the position is pinned). This is certainly fixable by creating a new cancel token every time the widget is constructed in the infoview, but I would rather have builtin mechanisms handle as much of this as possible, not users (hence the other PR).

I don't really understand what the changes in your new PR do.

Sorry about the opacity! I added some more explanation to the description there. But in short, a cancellation token is already included in the RequestContext (and is hence readable in RequestM), there just is no way for widgets to set it currently; the PR adds a way.

Will it solve one of these limitations?

if you close the infoview while the widget is active, and then reload
this part of the file, the widget computation keeps running without any way to stop it

My proposal includes an auto-cancellation mechanism that cancels requests started by the infoview when it is closed, so it'd fix part of this. There are really two separate issues here:

1. Runaway computations started by the infoview, which the other PR fixes.
2. Runaway computations started by elaborators, which I hope are fixable by correctly passing through the elaboration cancel token. I take your point about merging tokens. I wonder if it's possible to have a dedicated thread (that mostly sleeps which should take up no cycles) do that.

I haven't looked at the second limitation (earlier elab tokens getting cancelled by later ones) yet.

By the way, the fact that @[server_rpc_method_cancellable] exists is a bit confusing, now that there are all these different ways of doing cancellation. Should it be deprecated?

Yes, I think so, except that it does one extra thing: it turns a synchronous RPC handler into an asynchronous one, i.e., in JS a call to [server_rpc_method] blocks if awaited whereas a call to [server_rpc_method_cancellable] returns immediately. This is possibly useless (it's a Promise in the former case anyway), so deprecation sounds likely. Will look into it.

[JovanGerb]

Aha, I wasn't actually aware of the "pin" feature! I was just testing this by calling separate instances of the widget from Lean, which is now possible. I indeed see no way to, via a Lean change, support the "pin" feature while still cancelling tasks related to old widget instances, so thanks for opening that other PR.

It seems that with the request context cancellation, I will need to add checks for cancellation myself. But what I'm worried about is functions like isDefEq taking very long, and it only checks for cancellation with up to 1 cancel token that is stored in the Core context.