[Merged by Bors] - feat: add commutative diagram widget

[Vtec234]

Adds a widget for displaying goals in the language of category theory as commutative diagrams. Examples are found in test/CommDiag.lean. The set of diagram shapes which can be visualized is extensible via the @[expr_presenter] attribute. The widget is triggered in a tactic proof using the with_panel_widgets [GoalTypePanel] tactic combinator. Support for globally enabling the widget in a given file is planned for another PR.

Continued from #363, please see there for more discussion.

[kim-em]

This looks promising to me, and works out of the box.

From a UI perspective:

• even when I click into examples, it took me a while to work out I needed to click on the word "default" to find the other display options. More aggressively showing the options, or indeed more aggressively just rendering a non-default option, would be preferable.
• withPanelWidgets [SelectionPanel] is too "low-level" an incantation for someone trying to prove an actual theorem about categories to use in practice. How could be make it more user friendly to invoke?

[kim-em]

@Vtec234, should this have the WIP label still? Do you want to do anything about my comments above (not necessary; up to you).

[Vtec234]

Okay, it's ready! @semorrison / @eric-wieser could you check that it still works, please?

More aggressively showing the options, or indeed more aggressively just rendering a non-default option, would be preferable.

We always show a widget version over non-widget ones now, and a system for user-defined precedences between different widgets is planned.

Sometimes the nodes displayed aren't big enough for the text:

I rewrote the rendering code to be much more robust. If it ever shows an inconsistent state, it will be during loading, and the widget is grayed out then.

Can the colors be made to reflect the color scheme somehow?

They do now.

The idea would be to put show_panel_widgets [CommDiagWidget] at the top of the file, and from then on it would show up in every proof.

This is the only outstanding item left. I'd like to do it in another PR as changes to core are required.

[kim-em]

Still works for me!

[kim-em]

bors merge

[bors]

Build failed (retrying...):

• Check all files imported

[bors]

Build failed (retrying...):

• Check all files imported

[bors]

Build failed (retrying...):

• Check all files imported

[bors]

Build failed:

• Check all files imported

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style