octopus emoji

Stream: general

[Sean Leather]

What do you use :octopus: for? I'm struggling to understand it, and searching doesn't clarify much.

[Kevin Buzzard]

It's for achievements

[Kevin Buzzard]

you level up

[Kevin Buzzard]

well, that's what I use it for.

[Sean Leather]

So, it's like a “woo hoo!” kind of thing?

[Sean Leather]

Arms in the air and all that?

[Kevin Buzzard]

I think that it was just the community's reaction to the fact that the octopus emoji was constantly listed as "popular"

[Kevin Buzzard]

so we had to make it popular

[Sean Leather]

Which community, @Kevin Buzzard?

[Kevin Buzzard]

The Zulip lean-user community

[Sean Leather]

Okay.

[Kevin Buzzard]

Someone just randomly used it for something because it was there

[Kevin Buzzard]

and then it just became a bit of a meme

[Kevin Buzzard]

as far as I can see, at least

[Sean Leather]

I think those emojis under “Popular” were there from the beginning of https://leanprover.zulipchat.com/ and not as a result of being used more.

[Sean Leather]

I've also been confused about :hammer_and_wrench:.

[Patrick Massot]

Most :octopus: come from Simon who indeed use them as “woo hoo!” . I have no idea what :hammer_and_wrench: means

[Simon Hudon]

At last some credit! :stuck_out_tongue_closed_eyes:

[Simon Hudon]

I think I'm also guilty of propagating :hammer_and_wrench: it's more of a "cool technical thing there" note

[Simon Hudon]

Appropriate for instance when one has a quiet "mind blown" moment

[Simon Hudon]

But I am quite liberal with them

[Johan Commelin]

There should be a "+1" emoji

[Kevin Buzzard]

You would imagine that a +1 emoji would be more useful than the "waxing gibbous moon" emoji they have...