## Stream: general

### Topic: widget

#### Edward Ayers (May 07 2020 at 11:47):

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:

#### Gabriel Ebner (May 07 2020 at 11:53):

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 (May 07 2020 at 11:56):

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 (May 07 2020 at 12:02):

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 (May 07 2020 at 12:04):

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 (May 07 2020 at 12:05):

Oooh, this is slick!

#### Johan Commelin (May 07 2020 at 12:06):

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 (May 07 2020 at 12:06):

Yes the counter replaces the goal state widget.

#### Edward Ayers (May 07 2020 at 12:07):

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

#### Johan Commelin (May 07 2020 at 12:08):

But what does the comment after the split mean?

#### Johan Commelin (May 07 2020 at 12:08):

Should I then see two counters?

#### Edward Ayers (May 07 2020 at 12:08):

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 (May 07 2020 at 12:41):

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 (May 07 2020 at 12:43):

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 (May 07 2020 at 12:48):

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 (May 07 2020 at 12:52):

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

#### Jason Rute (May 07 2020 at 12:52):

Yes I just found that. Makes more sense.

#### Jason Rute (May 07 2020 at 12:53):

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 (May 07 2020 at 12:55):

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

#### Edward Ayers (May 07 2020 at 12:57):

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 (May 07 2020 at 13:10):

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

#### Edward Ayers (May 07 2020 at 13:25):

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 (May 07 2020 at 13:31):

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

#### Patrick Massot (May 07 2020 at 15:09):

This looks so awesome!

#### Patrick Massot (May 07 2020 at 15:13):

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

#### Patrick Massot (May 07 2020 at 15:14):

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

#### Edward Ayers (May 07 2020 at 15:15):

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 (May 07 2020 at 15:19):

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 (May 07 2020 at 15:23):

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

Great!

#### Edward Ayers (May 07 2020 at 15:40):

Gabriel Ebner said:

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

done

#### Gabriel Ebner (May 07 2020 at 15:41):

This is super nice!

#### Edward Ayers (May 07 2020 at 15:52):

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 (May 07 2020 at 15:52):

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:

#### Edward Ayers (May 07 2020 at 15:53):

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

#### Edward Ayers (May 07 2020 at 15:53):

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

#### Gabriel Ebner (May 07 2020 at 15:53):

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

#### Gabriel Ebner (May 07 2020 at 15:54):

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

#### Edward Ayers (May 07 2020 at 15:54):

Gabriel Ebner said:

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

wow that is wierd

#### Gabriel Ebner (May 07 2020 at 15:55):

MWE:

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


#### Edward Ayers (May 07 2020 at 15:55):

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 (May 07 2020 at 15:57):

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 (May 07 2020 at 16:06):

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 (May 07 2020 at 16:14):

It would make things easier

#### Edward Ayers (May 07 2020 at 16:27):

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

#### Gabriel Ebner (May 07 2020 at 16:30):

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 (May 07 2020 at 18:02):

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 (Jun 22 2020 at 16:15):

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

#### Rob Lewis (Jun 22 2020 at 16:16):

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

#### Jeremy Avigad (Jun 22 2020 at 16:37):

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 (Jun 22 2020 at 16:41):

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 (Jun 22 2020 at 16:42):

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 (Jun 22 2020 at 16:52):

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 (Jun 22 2020 at 16:57):

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 (Jun 22 2020 at 17:24):

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

#### Gabriel Ebner (Jun 22 2020 at 17:29):

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

Last updated: May 17 2021 at 23:14 UTC