Interactive definitions using the InfoView

Stream: lean4

[Joachim Breitner]

In case you are curious, this is my (still moving) goal for the hackathon:
“interactively editable definitions” that you can use in lean to have a UI to define a value of a given type.

The common infrastructure could be a type class for type t consisting of

• a function String → t (for some possibly quite opaque representation of t, possibly with extra information used in the UI) and
• a react component with state of type String.

Then you could write

def answer : graph = by interactive ""

and as long as the cursor is over the tactic, you get a suitable widget for the type (here graph) in the info view where you can define and manipulate the value (for graph it could be a graph editor) .
You changes are then automatically persisted in the source in the string parameter; you do _not_ replace that tactic with the value in the end! This means that you, or your collaborators, can edit this any time, and there can be extra information stored (e.g. the actual positions of the graph nodes, even if the graph type itself only stores the edges).
Of course the tactic returns (elaborates to? what’s the right term) a term of type graph here.

The idea is that the string should be opaque to the user. It might be Base-encoded just to drive down that point :-). At least in this iteration of this idea… maybe there could also be a variant where after interactive you can have the normal lean source definition of the value, and can edit either the text of the graphical version.

With this setup I hope that many such interactive editors for various types can be spun up quite quickly.

[Sebastian Ullrich]

Finally an interaction idea for which we do not need to worry about code formatting :laughing: