RFC: Widget messages

[Vtec234]

RFC: Widget messages

The current user widgets system supports exactly one kind of user widget - a widget panel, that is a piece of UI which can appear as a top-level panel next to the tactic state, messages, etc, in the infoview. Since we already have all the infrastructure for dynamic code loading in the infoview set up, there is no reason to limit ourselves to panels. Here I would like to propose widget messages. Implementation-wise, these would need one new constructor of MessageData, MessageData.ofWidget (msg : WidgetMsg). I have not implemented this, but I am happy to do it if there is interest/approval. Widget messages are primarily motivated by the use-cases they would enable:

Example 1: "Try this"

We can write a generic "Try this" UI component resulting in tryThis : Syntax → Syntax → WidgetMsg where tryThis stxRef newStx is the data of a "Try this" display that replaces stxRef with newStx upon a click. We would then include it in messages output by tactic code using something like m!"<some tactic output>{.tryThis stxRef newStx}".

Example 2: Contextual traces in failure messages

It is currently not always easy to view extra detail associated with a failure message. For instance, suppose the system prints a failed to synthesize instance SomeClass α message. In cases where it is not obvious why the synthesis failed (e.g. when debugging typeclass hierarchies), we can debug it by setting trace.Meta.synthInstance true. However we must either do so on the entire enclosing command which produces lots of irrelevant output, or extract a self-contained trace.Meta.synthInstance true in #synth SomeClass α which may be non-trivial if α depends on local context. And in any case we have to type the option in every time! It would be convenient if the failure message directly included a [Trace] button below it which would show this output when clicked. This could be achieved straightforwardly with a widget message. The idea extends to other failures, e.g. trace.Meta.isDefEq traces for expected .. but got ... Note that this is not supposed to collect traces eagerly as these can use up substantial memory. Rather, the data of a [Trace] button is just the inputs to the failed computation, and clicking it would rerun the computation with tracing enabled.

Pitfalls and alternatives

• We already have specialized data associated with message, for example MessageData.ofExpr e. This is a bit more than MessageData.ofWidget (displayTheExpr e) because it contains more data than just "display this". For example, we can inspect it to check if a message contains sorry expressions. An alternative along these lines would be to add MessageData.ofTryThis, MessageData.ofTraceOnClick etc. The problem with this approach is that it's not user-extensible.
• We need to maintain compatibility with text-based environments and ones without the JS-based infoview, so WidgetMsg should likely include a toText field, even if just to emit a placeholder in the case of inherently graphical messages.

[gebner]

MessageData.ofTraceOnClick

This function is spelled id. 😄 Note that trace messages are already MessageData.

MessageData.ofExpr

This is implemented using MessageData.ofPPFormat these days.

[gebner]

I'm still pretty concerned about backwards (forwards?) compatibility and deployment (where to put the javascript) when using widgets for core functionality.

MessageData.ofTryThis

This would be my preferred solution.

[Vtec234]

MessageData.ofTraceOnClick

This function is spelled id. 😄 Note that trace messages are already MessageData.

It is not, this is what I was trying to get at with "Note that this is not supposed to collect traces eagerly as these can use up substantial memory.". The point of a "trace on click" widget is to store the input data to some failed computation but not the trace of said computation because that takes additional memory and computation (to create the MessageData) time. When the user clicks the button, the computation is re-ran with the same inputs but with tracing now enabled, and the trace is displayed. So it is a very-lazy trace in that it is not even gathered until you request it to be. Think of it like a convenient "add the trace.Foo option and recompute whatever with it" button.

[gebner]

For instance, suppose the system prints a failed to synthesize instance SomeClass α message. In cases where it is not obvious why the synthesis failed (e.g. when debugging typeclass hierarchies), we can debug it by setting trace.Meta.synthInstance true.

You usually want to set more options than just the "obvious" one. E.g. trace.Meta.isDefEq to see why Lean couldn't apply an instance that should work. Or maxHeartbeats 1000 to reduce the waiting time. In #400 we've proposed to add even more interesting filtering options.

Vice versa, I often want to enable trace.Meta.synthInstance for other errors.

[Vtec234]

You usually want to set more options than just the "obvious" one

All this is a detail of how you implement the particular message widget. The point of the new MessageData constructor (and this RFC) would only be to have a direct "handle" on (RPC reference to) the input data to the failed computation (or to one that you otherwise care about).

This is implemented using MessageData.ofPPFormat these days.

Oh right, I even reviewed that PR 🤦 In light of that, what I am suggesting is to turn ofPPFormat into a pair of (current type, a PP function which runs in StateM RpcObjectStore and may produce a widget).

I'm still pretty concerned about backwards (forwards?) compatibility and deployment (where to put the javascript) when using widgets for core functionality.

What do you think about the pair of formatters? The expectation is that one element of the pair works in text-based environments but the other need not.