widget

Stream: general

[Edward Ayers]

Hi everyone, I've built a prototype functional UI framework for lean that you can try out here: https://demo.edayers.com
It's still very much WIP but I thought I would share it here now because I am now happy with it as a proof of concept.
The idea is that you can use widget.component and widget.html to build a virtual HTML tree in Lean (with support for stateful components).
There is a new constant called save_widget which performs the analogue of save_info_thunk. If this is called, then instead of rendering the goal state, the editor will render an interactive widget. It is also possible for the widget to send commands to the editor.
This means that it is possible to make an interactive UI for tactic states (eg you could click on a goal and it would give you a list of available tactics) entirely within lean, without having to write any javascript or C++.
The UI building API is still very rough and subject to change.

The source code is on a branch called 'widget' in the following places:

• lean: https://github.com/EdAyers/lean/tree/widget
• vscode extension: https://github.com/EdAyers/vscode-lean/tree/widget
• lean-web-editor: https://github.com/EdAyers/lean-web-editor/tree/widget
  Also massive thanks to @Bryan Gin-ge Chen for helping me get the emscripten build working!

[Gabriel Ebner]

So apparently this can be used to implement go-to-definition in the goal view. And it should also be possible to implement a feature where you can click on a subterm and it expands the implicit arguments.

[Edward Ayers]

Yep, go-to-definition would require writing a hook in the client editor but subterm implicit arguments is straightforward. The tooltip message is generated by lean and it has the full tactic state and subexpression to work with when generating the UI.

[Jason Rute]

And it should also be possible to implement a feature where you can click on a subterm and it expands the implicit arguments.

I would love to have something similar to IntelliJ's Scala Plugin's "show implicits".

The other IntelliJ feature that I'd love to have is to select a subexpression (not just a single word) and to get the type of the whole subexpression.

... and "reverse go to definition" which finds all uses of a definition in the codebase.

[Edward Ayers]

Jason Rute said:

The other IntelliJ feature that I'd love to have is to select a subexpression (not just a single word) and to get the type of the whole subexpression.

That works on the demo right now.

[Johan Commelin]

Oooh, this is slick!

[Johan Commelin]

Only, when I have the counter, I don't see any other goal state anymore. And after the split, I only have 1 counter, whereas I interpret the comments as saying that I should see two. Is that right?

[Edward Ayers]

Yes the counter replaces the goal state widget.

[Edward Ayers]

But you could easily make a component that shows both the counter and the tactic state

[Johan Commelin]

But what does the comment after the split mean?

[Johan Commelin]

Should I then see two counters?

[Edward Ayers]

There is a separate counter state (the number between buttons) for each command in the block. So if you click between the counters you can observe that the state is preserved, the idea is that you would use this state for ephemeral things like whether a UI menu is open or scroll position or whatever

[Jason Rute]

This means that it is possible to make an interactive UI for tactic states (eg you could click on a goal and it would give you a list of available tactics) entirely within lean, without having to write any javascript or C++.

To flesh this out a little more, how would you implement this "available tactics" example? Would you write a "widget" (formally a function of type component tactic_state string) in lean similar to your counter example, but which looks at the tactic_state and then figures out which tactics are applicable (sort of a like many of the current tactics which generate Try it:s). Then the result of that widget tactic would be printed on the right?

[Jason Rute]

I'm mixing up my types a little. Can you call tactics from within your widgets (again, functions of type component tactic_state string)? Maybe you would directly apply the tactic to the tactic_state?

[Edward Ayers]

Yes that's the rough idea. Since tactic a := tactic_state -> interaction_monad (tactic_state x a) (OWTTE) you can run tactics inside the 'view' method of a component. But you can't output a tactic_state to anywhere, instead you have to get the component to emit a string (as it does in the counter example) which is a command in the begin/end block.

[Edward Ayers]

There is a helper def widget.mk_tactic_widget for making widgets which use tactics

[Jason Rute]

Yes I just found that. Makes more sense.

[Jason Rute]

Also, one big advantage of this over just adding a tactic at the end of your block is that you can delay running this "suggest" tactic (which might be expensive) until the user clicks on the goal (or some button which says "find relevant tactics"). Is that the idea?

[Edward Ayers]

Yes. Eg the contents of the type tooltip is not computed until you click on it

[Edward Ayers]

currently there is no support for having a long-running computation in a task a and having the UI update when it is done, so the user experience is not going to be great if there is a long-running comp that is needed before showing the UI

[Edward Ayers]

Here is an example that @Wojciech Nawrocki made, put your cursor on line 135!

[Edward Ayers]

Gabriel Ebner said:

So apparently this can be used to implement go-to-definition in the goal view. And it should also be possible to implement a feature where you can click on a subterm and it expands the implicit arguments.

You can now view the implicit arguments of an expression (recursively!). This was about 4 lines of lean code to add. No C++ changes.

[Gabriel Ebner]

Now this is really neat! Can you also make it work without the [widget_tactic]?

[Patrick Massot]

This looks so awesome!

[Patrick Massot]

What is the plan here? Getting this into a next version of Lean + VScode extension?

[Patrick Massot]

Is there already something we can do to have it in our VScode instead of online?

[Edward Ayers]

Patrick Massot said:

Is there already something we can do to have it in our VScode instead of online?

Yes there is a vscode extension but it's a bit of a faff to set up at the moment

[Edward Ayers]

Patrick Massot said:

What is the plan here? Getting this into a next version of Lean + VScode extension?

My main plan is to use it to make some UI for my thesis work, but eventually get it in to core Lean in the near future. The long term plan I guess is to convince the Lean 4 squad that allowing lean to have its own customisable UI system and having lots of interactivity is useful and feasible.

[Bryan Gin-ge Chen]

As you can see, there's a lot of enthusiasm here for this. Definitely reach out if you want a hand!

[Patrick Massot]

Great!

[Edward Ayers]

Gabriel Ebner said:

Now this is really neat! Can you also make it work without the [widget_tactic]?

done

[Gabriel Ebner]

This is super nice!

[Edward Ayers]

One thing that I'd like some type-theory advice on is whether it is possible to write the definitions of html a and component p a without having to use C++ implementations. When I tried to do it all in Lean, I couldn't get the universes to work correctly. Namely, I want to make the following definitions:

inductive html (Action : Type) : Type
| of_element : element Action → html
| of_string : string → html
| of_component : Π {Props : Type} → Props → component Props Action → html

structure html.element (α : Type) : Type :=
(tag : string)
(attributes : list (attr α))
(children : list (html α))

structure component (Props Action : Type) :=
(InnerAction : Type)
(State : Type)
(init : Props → option State → State)
(update : Props → State → InnerAction → State × option Action)
(view : Props → State → html InnerAction)

Even accounting for the mutual induction issues, I still have problems because of_component takes a type argument which causes the universe level to increment.

[Gabriel Ebner]

I could use this today... You can click on an coercion and it tells you what types it coerces between. In some cases the selection behaves a bit weird, I guess this is a bug:
widget_address_bug.png

[Edward Ayers]

hmm yes the logic for when to show and unshow tooltips is still a bit rough

[Edward Ayers]

but if you click on the expression that made the tooltip it should vanish

[Gabriel Ebner]

You can use meta inductive, this disables all checks for universes.

[Gabriel Ebner]

That's the problem, it always selects both subterms at once.

[Edward Ayers]

Gabriel Ebner said:

That's the problem, it always selects both subterms at once.

wow that is wierd

[Gabriel Ebner]

MWE:

example : ((1 : ℕ) : ℤ) = (fun x : ℤ, x + 3) 2 :=
by skip

[Edward Ayers]

ah yes I think that's because I didn't get round to implementing properly how coercion expressions are addressed when it does a structural pp

[Edward Ayers]

Gabriel Ebner said:

You can use meta inductive, this disables all checks for universes.

hmm when I tried this it was still doing universe checks i'll have another go

[Gabriel Ebner]

Oh, then I remembered this incorrectly. We only skip the positivity check for meta inductives, but not universes. We can remove that check as well if it makes your life easier.

[Edward Ayers]

It would make things easier

[Edward Ayers]

Ok I fixed the pp bug, I'll update the site when the emscripten build finishes

[Gabriel Ebner]

While I still think we should disable the universes check for meta inductive, here is a workaround:

universes u v

def attr' (html : Type → Type) : Type → Type := id -- fill in

structure element' (html : Type → Type) (α : Type) : Type :=
(tag : string)
(attributes : list (attr' html α))
(children : list (html α))

structure component' (html : Type → Type) (Props Action : Type) :=
(InnerAction : Type)
(State : Type)
(init : Props → option State → State)
(update : Props → State → InnerAction → State × option Action)
(view : Props → State → html InnerAction)

section uchange

/-- Like `unchecked_cast`, but across universes. -/
@[inline, irreducible]
meta def unchecked_cast' {α : Type u} {β : Type v} : α → β :=
(cast undefined (λ _ a, a : β → α → α) : β → α → β) (cast undefined punit.star)

meta def uchange (α : Type v) : Type u :=
unchecked_cast' α

meta def uchange.down {α} (a : α) : uchange α :=
unchecked_cast' a

meta def uchange.up {α} (a : uchange α) : α :=
unchecked_cast' a

end uchange

meta inductive html' (html : Type → Type) (Action : Type) : Type
| of_element : element' html Action → html'
| of_string : string → html'
| of_component : uchange.{0} (Σ Props (p : Props), component' html Props Action) → html'

meta def html := html' html
meta def component := component' html
meta def element := element' html
meta def attr := attr' html

meta example : html unit := html'.of_component (uchange.down ⟨unit, (), _, _, _, _, _⟩)

[Mario Carneiro]

Oh wow, uchange should definitely be PR'd to mathlib. The trick with casting the second projection function is great, I had thought it wasn't possible to use cast for this because of the single universe in eq

[Rob Lewis]

Ever felt like writing some Mathematica code in the middle of your Lean file? mm_ex1.png

[Rob Lewis]

What about throwing some Lean expressions in there for fun?
mm_ex2.png

[Jeremy Avigad]

That is really great! What is your sense of how hard it would be to translate your Mathematica connection to another CAS like Sage or GAP? In the long run, I'd like to see online textbooks that combine formal proving and CASs. Open source CASs and integration in CoCalc seem to be big wins.

[Rob Lewis]

Mathematica is a functional language with a simple term structure that makes it super convenient for this kind of thing. Last year Minchao and I looked a bit into translating it to Sage. How hard is it? Somewhere between "difficult" and "needs an entirely different architecture." I'd need to learn a lot more about the Sage internals to say more.

[Rob Lewis]

This demo is nothing big, by the way, just an afternoon of work. It's the old link + Ed's widgets + a bit of parser hackery inspired by Sebastian's Lean 4 demo.

[Patrick Massot]

If one of us goes into cryostat for a couple of years it won't recognize proof assistants when he'll wake up.

[Jeremy Avigad]

Somewhere between "difficult" and "needs an entirely different architecture."

This demo is nothing big, by the way, just an afternoon of work.

That's why I asked... It's often hard to tell what is hard and what is easy. https://xkcd.com/1425/.

[Rob Lewis]

There must be a black box bird identifier by now, right?

[Gabriel Ebner]

Yeah, that xkcd was pretty spot on. Its been five years and deep learning has pretty much solved this problem.