Zulip Chat Archive

Stream: general

Topic: octopus emoji


view this post on Zulip Sean Leather (Apr 10 2018 at 08:02):

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

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:03):

It's for achievements

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:03):

you level up

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:04):

well, that's what I use it for.

view this post on Zulip Sean Leather (Apr 10 2018 at 08:04):

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

view this post on Zulip Sean Leather (Apr 10 2018 at 08:04):

Arms in the air and all that?

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:04):

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

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:05):

so we had to make it popular

view this post on Zulip Sean Leather (Apr 10 2018 at 08:05):

Which community, @Kevin Buzzard?

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:06):

The Zulip lean-user community

view this post on Zulip Sean Leather (Apr 10 2018 at 08:06):

Okay.

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:06):

Someone just randomly used it for something because it was there

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:06):

and then it just became a bit of a meme

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:06):

as far as I can see, at least

view this post on Zulip Sean Leather (Apr 10 2018 at 08:08):

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.

view this post on Zulip Sean Leather (Apr 10 2018 at 08:09):

I've also been confused about :hammer_and_wrench:.

view this post on Zulip Patrick Massot (Apr 10 2018 at 08:17):

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

view this post on Zulip Simon Hudon (Apr 10 2018 at 15:46):

At last some credit! :stuck_out_tongue_closed_eyes:

view this post on Zulip Simon Hudon (Apr 10 2018 at 15:46):

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

view this post on Zulip Simon Hudon (Apr 10 2018 at 15:47):

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

view this post on Zulip Simon Hudon (Apr 10 2018 at 15:47):

But I am quite liberal with them

view this post on Zulip Johan Commelin (Apr 11 2018 at 07:00):

There should be a "+1" emoji

view this post on Zulip Kevin Buzzard (Apr 11 2018 at 07:11):

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


Last updated: May 13 2021 at 06:15 UTC