!4#3583 comm diagram widget

Stream: mathlib4

[Kevin Buzzard]

@Wojciech Nawrocki is !4#3583 marked WIP for a good reason? I would love to see this in mathlib so I can start experimenting with it.

[Scott Morrison]

Sorry, this is probably my fault. I would really like it in too, but I had complained a bit about the user interface issues (weird command to enable the widget, and then not particularly discoverable how to use the widget).

However I think I was mistaken, and the right steps here are to get it in, as I'm pretty certain we want it, and then improve UX as people actually want to use it.

[Scott Morrison]

Objections to merging in 3...2...1... / the next couple of days, should be expressed somewhere soon!

[Johan Commelin]

I agree with that strategy. Let's merge it, use it for a bit, and improve UX inspired by those experiences.

[Jake Levinson]

Random idea for a further usage of such a widget (inspired by @Heather Macbeth 's description of a wishlist for a relational congruence widget): it would be neat to have drag-and-drop from the commutative diagram widget to the Lean file. When I did a tiny bit of category theory last summer, I remember it sometimes being laborious to write (or even remember) the full name of an object or morphism. If the widget can show the diagram, I can probably see at a glance which objects / arrows I have to prove things about, and it would be neat to be able to click on them directly and get their name in the proof.

[Scott Morrison]

Is that actually just achievable via copy-and-paste from a label in the displayed commutative diagram?

[Jake Levinson]

That would work fine too yes! I think any term that can be selected in the infoview can also be copy-pasted(?)

[Wojciech Nawrocki]

Hi! Yes, the WIP is mostly due to Scott's objections.. which I absolutely agree with! The main issue is that there is no way to say 'I want to see commutative diagrams in every proof in this file', and beyond that there is some awkwardness in the UX. I can make a stopgap fix to the awkwardness ASAP if you'd like to merge, but the global widget-toggle will need a larger PR to core that's on my TODO list.

[Kevin Buzzard]

I guess you shouldn't do anything in the short term if it will mean more work in the long term. My enthusiasm for having something merged so I can play with it can be taken with a pinch of salt if it will cause strictly more work behind the scenes