Zulip Chat Archive

Stream: general

Topic: widgets in conv mode

Johan Commelin (Jul 21 2020 at 20:00):

It seems that widgets don't work in conv mode. How hard would it be to enable them there?

Johan Commelin (Jul 21 2020 at 20:00):

They're really good! As soon as they're not there... I miss them, and I'm completely stuck and helpless :oops:

Bryan Gin-ge Chen (Jul 21 2020 at 20:07):

It'd also be nice to upgrade #print, #eval, #reduce, etc. to output widgets as well...

@Edward Ayers wanna give us some hints?

Edward Ayers (Jul 21 2020 at 20:08):

Yeah you should be able to get widgets for other interactive modes by overriding conv.save_info

Edward Ayers (Jul 21 2020 at 20:09):

The #xs sound a little more fiddly because if I recall correctly they are implemented in c++

Kevin Buzzard (Jun 23 2021 at 19:00):

I'm exploring some terms coming from mathematics in conv mode and I have goals like this:

2 goals
card_five_points : ?m_1 := (fintype.card (fintype (E.p_points 5, five_is_good⟩)))
| 5, five_is_good

card_five_points : ?m_1 := (fintype.card (fintype (E.p_points 5, five_is_good⟩)))
| (fintype.card (fintype (E.p_points 5, five_is_good⟩)))

and I really want the infoview to tell me what those coercions are. Can we have widgets in conv mode? Is that a one-line hack or a 2 month research project?

Gabriel Ebner (Jun 23 2021 at 19:07):

I'd estimate 20 lines of code. If somebody wants to take it on, you need to copy this file for conv: https://github.com/leanprover-community/lean/blob/25b46580d9f57be6242dcb3bf764ff11cd19b580/library/init/meta/widget/replace_save_info.lean (and probably tweak the rendering a bit to show | instead of )

Bryan Gin-ge Chen (Jun 23 2021 at 19:07):

Seems like the sort of thing we'd want for almost all tactics, right?

Gabriel Ebner (Jun 23 2021 at 19:08):

conv is a different "tactic mode" (no idea how it's called)

Bryan Gin-ge Chen (Jun 23 2021 at 19:08):

Oh, right.

Last updated: Aug 03 2023 at 10:10 UTC