mathlib GitHub bot icon

Stream: general

[Joachim Breitner]

Is someone inspired and authorized to set a profile photo for the mathlib GitHub bot (https://github.com/leanprover-community-mathlib4-bot)? Or, it only authorized, but not inspired, is willing to set it if I draw something? It would prevent being curiously exited on the GitHub notification page because you think someone real commented, and is generally nicer :-)

[Yaël Dillies]

Yes please! I've previously asked the same of all community-owned accounts and organisation, to no avail so far.

[Mario Carneiro]

do you have any particular proposals? It's not technically difficult to add a profile pic, the question is what to put there

[Mario Carneiro]

mathlib-bors has

[Patrick Massot]

That icon is funny but I would prefer something more serious.

[Mario Carneiro]

unfortunately we don't really have a graphic designer in the community AFAICT

[Kyle Miller]

While this might not really be serious, here's a really serious octopus that's thinking very hard about whether our PRs merge properly.

octopus-serious-3.png

(edited to have the version now on bors)