Zulip Chat Archive

Stream: general

Topic: widget


view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 07 2020 at 12:05):

Oooh, this is slick!

view this post on Zulip 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?

view this post on Zulip Edward Ayers (May 07 2020 at 12:06):

Yes the counter replaces the goal state widget.

view this post on Zulip Edward Ayers (May 07 2020 at 12:07):

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

view this post on Zulip Johan Commelin (May 07 2020 at 12:08):

But what does the comment after the split mean?

view this post on Zulip Johan Commelin (May 07 2020 at 12:08):

Should I then see two counters?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Edward Ayers (May 07 2020 at 12:52):

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

view this post on Zulip Jason Rute (May 07 2020 at 12:52):

Yes I just found that. Makes more sense.

view this post on Zulip 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?

view this post on Zulip Edward Ayers (May 07 2020 at 12:55):

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

view this post on Zulip 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

view this post on Zulip Edward Ayers (May 07 2020 at 13:10):

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

view this post on Zulip 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.

view this post on Zulip Gabriel Ebner (May 07 2020 at 13:31):

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

view this post on Zulip Patrick Massot (May 07 2020 at 15:09):

This looks so awesome!

view this post on Zulip Patrick Massot (May 07 2020 at 15:13):

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

view this post on Zulip Patrick Massot (May 07 2020 at 15:14):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Patrick Massot (May 07 2020 at 15:35):

Great!

view this post on Zulip 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

view this post on Zulip Gabriel Ebner (May 07 2020 at 15:41):

This is super nice!

view this post on Zulip 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.

view this post on Zulip 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:
widget_address_bug.png

view this post on Zulip Edward Ayers (May 07 2020 at 15:53):

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

view this post on Zulip Edward Ayers (May 07 2020 at 15:53):

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

view this post on Zulip Gabriel Ebner (May 07 2020 at 15:53):

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

view this post on Zulip Gabriel Ebner (May 07 2020 at 15:54):

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

view this post on Zulip 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

view this post on Zulip Gabriel Ebner (May 07 2020 at 15:55):

MWE:

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Edward Ayers (May 07 2020 at 16:14):

It would make things easier

view this post on Zulip Edward Ayers (May 07 2020 at 16:27):

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

view this post on Zulip 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, (), _, _, _, _, _⟩)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Rob Lewis (Jun 22 2020 at 16:16):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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/.

view this post on Zulip Rob Lewis (Jun 22 2020 at 17:24):

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

view this post on Zulip 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