RFC: Widget messages #2064
Comments
This function is spelled
This is implemented using |
|
I'm still pretty concerned about backwards (forwards?) compatibility and deployment (where to put the javascript) when using widgets for core functionality.
This would be my preferred solution. |
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 |
You usually want to set more options than just the "obvious" one. E.g. Vice versa, I often want to enable |
All this is a detail of how you implement the particular message widget. The point of the new
Oh right, I even reviewed that PR 🤦 In light of that, what I am suggesting is to turn
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. |
Allows embedding user widgets in structured messages. Companion PR is leanprover/vscode-lean4#449. Some technical choices: - The `MessageData.ofWidget` constructor might not be strictly necessary as we already have `MessageData.ofFormatWithInfos`, and there is `Info.ofUserWidget`. However, `.ofUserWidget` also requires a `Syntax` object (as it is normally produced when widgets are saved at a piece of syntax during elaboration) which we do not have in this case. More generally, it continues to be a bit cursed that `Elab.Info` nodes are used both for elaboration and delaboration (pretty-printing), so entrenching that approach seems wrong. The better approach would be to have a separate notion of pretty-printer annotation; but such a refactor would not be clearly beneficial right now. - To support non-JS-based environments such as https://github.com/Julian/lean.nvim, `.ofWidget` requires also providing another message which approximates the widget in a textual form. However, in practice these environments might still want to support a few specific user widgets such as "Try this". --- Closes #2064.
Implementation of leanprover/lean4#2064. Besides adding support for widget messages, this adds an `EnvPosContext` that stores the position that a component is "about" (see the docstring for more detail). This was originally proposed in #197 and eventually dismissed (see #226 for a detailed discussion), but I think it warrants a reconsideration. While Gabriel's point that there are many positions around remains true, the `EnvPosContext` stores a very specific one. This position is only used to retrieve a snapshot, and from that a `Lean.Environment`, on the server-side. Widgets currently have to pass this position around manually; this has led to [errors](leanprover-community/ProofWidgets4@ca66ebb) in user code. Furthermore, so far I have not encountered any situation where it makes sense to modify the position; thus a context seems like a preferable approach. If needed, the context can still be set by users. I also had to update some package versions to have tests building again. I hope that didn't break anything!
Implementation of leanprover/lean4#2064. Besides adding support for widget messages, this adds an `EnvPosContext` that stores the position that a component is "about" (see the docstring for more detail). This was originally proposed in #197 and eventually dismissed (see #226 for a detailed discussion), but I think it warrants a reconsideration. While Gabriel's point that there are many positions around remains true, the `EnvPosContext` stores a very specific one. This position is only used to retrieve a snapshot, and from that a `Lean.Environment`, on the server-side. Widgets currently have to pass this position around manually; this has led to [errors](leanprover-community/ProofWidgets4@ca66ebb) in user code. Furthermore, so far I have not encountered any situation where it makes sense to modify the position; thus a context seems like a preferable approach. If needed, the context can still be set by users. I also had to update some package versions to have tests building again. I hope that didn't break anything!
Implementation of leanprover/lean4#2064. Besides adding support for widget messages, this adds an `EnvPosContext` that stores the position that a component is "about" (see the docstring for more detail). This was originally proposed in #197 and eventually dismissed (see #226 for a detailed discussion), but I think it warrants a reconsideration. While Gabriel's point that there are many positions around remains true, the `EnvPosContext` stores a very specific one. This position is only used to retrieve a snapshot, and from that a `Lean.Environment`, on the server-side. Widgets currently have to pass this position around manually; this has led to [errors](leanprover-community/ProofWidgets4@ca66ebb) in user code. Furthermore, so far I have not encountered any situation where it makes sense to modify the position; thus a context seems like a preferable approach. If needed, the context can still be set by users. I also had to update some package versions to have tests building again. I hope that didn't break anything!
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 → WidgetMsgwheretryThis stxRef newStxis the data of a "Try this" display that replacesstxRefwithnewStxupon a click. We would then include it in messages output by tactic code using something likem!"<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 settingtrace.Meta.synthInstance true. However we must either do so on the entire enclosing command which produces lots of irrelevant output, or extract a self-containedtrace.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.isDefEqtraces forexpected .. 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
MessageData.ofExpr e. This is a bit more thanMessageData.ofWidget (displayTheExpr e)because it contains more data than just "display this". For example, we can inspect it to check if a message containssorryexpressions. An alternative along these lines would be to addMessageData.ofTryThis,MessageData.ofTraceOnClicketc. The problem with this approach is that it's not user-extensible.WidgetMsgshould likely include atoTextfield, even if just to emit a placeholder in the case of inherently graphical messages.The text was updated successfully, but these errors were encountered: