widgets in conv mode

Stream: general

[Johan Commelin]

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

[Johan Commelin]

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]

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]

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

[Edward Ayers]

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

[Kevin Buzzard]

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]

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]

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

[Gabriel Ebner]

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

[Bryan Gin-ge Chen]

Oh, right.