Zulip Chat Archive

Stream: Zulip meta

Topic: Logo


view this post on Zulip Patrick Massot (Jul 16 2020 at 08:53):

Is it only me or Zulip just suddenly changed its logo?

view this post on Zulip Markus Himmel (Jul 16 2020 at 08:54):

Yes, it changed a few minutes ago

view this post on Zulip Sebastien Gouezel (Jul 16 2020 at 08:54):

Same here.

view this post on Zulip Rob Lewis (Jul 16 2020 at 08:55):

Whoa, so high tech.

view this post on Zulip Patrick Massot (Jul 16 2020 at 08:55):

This is crap: the new Z is much further away from Bourbaki's dangerous bend sign that was so fitting for this Zulip instance.

view this post on Zulip Rob Lewis (Jul 16 2020 at 08:55):

I feel like we've made it to 2012 now.

view this post on Zulip Markus Himmel (Jul 16 2020 at 09:28):

Patrick Massot said:

This is crap: the new Z is much further away from Bourbaki's dangerous bend sign that was so fitting for this Zulip instance.

It looks like this can be changed? https://zulip.com/help/create-your-organization-profile#add-a-wide-logo

view this post on Zulip Patrick Massot (Jul 16 2020 at 09:32):

I actually like the idea of using a Bourbaki Z followed by the word Zulip

view this post on Zulip Patrick Massot (Jul 16 2020 at 09:33):

Rob Lewis said:

I feel like we've made it to 2012 now.

That's the retro-futuristic look. Let's go retro instead.

view this post on Zulip Anne Baanen (Jul 16 2020 at 09:33):

We should add a ☡ emoji reaction as well!

view this post on Zulip Patrick Massot (Jul 16 2020 at 09:33):

Is that possible?

view this post on Zulip Anne Baanen (Jul 16 2020 at 09:34):

The Zulip emoji is in a section called 'custom', so I assume it should be?

view this post on Zulip Patrick Massot (Jul 16 2020 at 09:34):

But, at least in the font I see now, this is not quite orthodox. Someone clearly decided that Bourbaki's version was hard to distinguish from a Z and decided to rotate it.

view this post on Zulip Patrick Massot (Jul 16 2020 at 09:34):

In the printed book there absolutely no possible confusion because it's too large and bold to be a Z

view this post on Zulip Mario Carneiro (Jul 16 2020 at 09:35):

Doesn't that imply that lean is dangerous and/or easily misunderstood?

view this post on Zulip Patrick Massot (Jul 16 2020 at 09:35):

Yes?

view this post on Zulip Patrick Massot (Jul 16 2020 at 09:35):

How could it be fun otherwise?

view this post on Zulip Johan Commelin (Jul 16 2020 at 09:35):

Patrick Massot said:

Is that possible?

admins can add emoji

view this post on Zulip Patrick Massot (Jul 16 2020 at 09:36):

They also changed the menu icon on messages

view this post on Zulip Anne Baanen (Jul 16 2020 at 09:36):

Hmm, how difficult would it be to hack a font so ':warning:️☡' displays as Knuth's symbol? :thinking:

view this post on Zulip Patrick Massot (Jul 16 2020 at 09:37):

Knuth's symbol is also deviant. He also clearly thought Bourbaki's symbol looked too much like a Z

view this post on Zulip Mario Carneiro (Jul 16 2020 at 09:38):

isn't that what the actual "dangerous bend" sign looks like?

view this post on Zulip Anne Baanen (Jul 16 2020 at 09:38):

We should preface each use of '☡' with '☡' because people might think the dangerous bend symbol looks like '☡'.

view this post on Zulip Patrick Massot (Jul 16 2020 at 09:39):

Mario, that's the American version

view this post on Zulip Patrick Massot (Jul 16 2020 at 09:39):

Actually the current French version now looks like a N rather than a Z

view this post on Zulip Patrick Massot (Jul 16 2020 at 09:40):

Anne Baanen said:

We should preface each use of '☡' with '☡' because people might think the dangerous bend symbol looks like '☡'.

Don't forget the meta keyword then.

view this post on Zulip Kevin Buzzard (Jul 16 2020 at 09:53):

On the Xena discord, when I made a bunch of students admins, the first thing they did was added loads of extra emojis.

view this post on Zulip Kevin Buzzard (Jul 16 2020 at 09:53):

We have several Lean emojis

view this post on Zulip Rob Lewis (Jul 16 2020 at 09:54):

:bourbaki:

view this post on Zulip Rob Lewis (Jul 16 2020 at 09:54):

Ah, that image didn't have a transparent background

view this post on Zulip Kevin Buzzard (Jul 16 2020 at 09:55):

hmmskell.png

view this post on Zulip Kevin Buzzard (Jul 16 2020 at 09:55):

We have a "hmmskell" emoji

view this post on Zulip Kevin Buzzard (Jul 16 2020 at 10:00):

If you care about emojis you should switch to discord. We have a stream for cat pictures and everything

view this post on Zulip Rob Lewis (Jul 16 2020 at 10:00):

Ugh, I hate Gimp, if someone sends me logos/emoji I'll add them but I'm not gonna give that a transparent background myself

view this post on Zulip Anne Baanen (Jul 16 2020 at 10:03):

Deal. My vacation starts in one week, fear the worst :smiley:

view this post on Zulip Bhavik Mehta (Jul 16 2020 at 11:41):

Oh yeah I need to make a hmmlean emoji

view this post on Zulip Kenny Lau (Jul 16 2020 at 18:14):

2020-07-17.png

view this post on Zulip Kenny Lau (Jul 16 2020 at 18:14):

this is how the tab looks on my side

view this post on Zulip Kenny Lau (Jul 16 2020 at 18:14):

the number (of new messages) got displaced and is much blurrier

view this post on Zulip Kenny Lau (Jul 16 2020 at 18:15):

I tried to find a screenshot from before the change happened to no avail

view this post on Zulip Bryan Gin-ge Chen (Jul 16 2020 at 18:58):

Looks like the new logo is for Zulip 3.0: https://blog.zulip.com/2020/07/16/zulip-3-0-released/

I also noticed the numbers in the favicon looking a lot uglier. I didn't see an issue on their github and don't feel like making one though.

view this post on Zulip Sebastian Ullrich (Jul 16 2020 at 20:03):

I looked at the new logo for too long and now all I see is a \rightharpoondown and \leftharpoonup

view this post on Zulip Mario Carneiro (Jul 28 2020 at 08:54):

The logo changed again. Was that our doing?

view this post on Zulip Johan Commelin (Jul 28 2020 at 08:56):

Hmm, the new :bourbaki: is not so readable on a dark background :sad:

view this post on Zulip Mario Carneiro (Jul 28 2020 at 08:56):

I'm on night mode and I see it in blue in the top left

view this post on Zulip Mario Carneiro (Jul 28 2020 at 08:57):

are you talking about the emoji?

view this post on Zulip Rob Lewis (Jul 28 2020 at 08:58):

Everyone has permission to add (and maybe edit?) emoji now

view this post on Zulip Mario Carneiro (Jul 28 2020 at 08:58):

perhaps that's why all the letter emoji are in big colored boxes

view this post on Zulip Gabriel Ebner (Jul 28 2020 at 08:58):

No, the Zulip logo has changed.

view this post on Zulip Gabriel Ebner (Jul 28 2020 at 08:58):

The Z is the mirrored slightly rotated dangerous bend symbol now.

view this post on Zulip Mario Carneiro (Jul 28 2020 at 08:59):

The emoji question was directed at Johan, not myself :grinning_face_with_smiling_eyes:

view this post on Zulip Mario Carneiro (Jul 28 2020 at 09:00):

I guess if the ☡ was in a yellow box it would solve the problem

view this post on Zulip Patrick Massot (Jul 28 2020 at 14:16):

Who changed the logo? I think having two weird Z next to each other feels very weird.

view this post on Zulip Patrick Massot (Jul 28 2020 at 14:17):

I would rather have the Bourbaki sign replacing the double-harpoon Z and keep a regular Z at the beginning of the Zulip word.

view this post on Zulip Rob Lewis (Jul 28 2020 at 14:18):

The unicode Bourbaki sign isn't heavy enough to replace the big Z and I wasn't willing to spend the time to make a good looking extra-bold version...

view this post on Zulip Rob Lewis (Jul 28 2020 at 14:19):

This was just a joke anyway, I was planning to change it back in a few days. If someone wants to make it look good just post an image.

view this post on Zulip Johan Commelin (Jul 28 2020 at 14:22):

@Rob Lewis I see that you added :coq: and :isabelle: , but where is :lean:? The closest I get is :nuclear: (:nuclear:)... :grinning_face_with_smiling_eyes:

view this post on Zulip Rob Lewis (Jul 28 2020 at 14:23):

Is the "L" favicon the closest we have to a logo?

view this post on Zulip Johan Commelin (Jul 28 2020 at 14:26):

Probably

view this post on Zulip Sebastian Ullrich (Jul 28 2020 at 14:48):

You can stack the four letters in the Lean logo and you get, uhhh image.png

view this post on Zulip Rob Lewis (Jul 28 2020 at 15:22):

Someone should get the Lean one from Kevin's discord.
Kevin Buzzard said:

hmmskell.png

view this post on Zulip Rob Lewis (Jul 28 2020 at 15:22):

Also :yeet: please.

view this post on Zulip Patrick Massot (Jul 28 2020 at 15:22):

What does yeet mean?

view this post on Zulip Gabriel Ebner (Jul 28 2020 at 15:25):

I absolutely loove the colorful leanmoji!

view this post on Zulip Rob Lewis (Jul 28 2020 at 15:34):

Yeet, a surprisingly clean Urban Dictionary entry!

view this post on Zulip Alex J. Best (Jul 28 2020 at 15:36):

I guess number 3 is the most reasonable one for the discord emoji

Yeet is a versatile word that can be used as an exclamation, a verb, or even a noun.

As an exclamation it can be used to express excitement, usually happily but also nervously. (See Ex. 1)
It can also be used as an exclamation of victory. (See Ex. 2)
Or as a battle cry or focus-shout while throwing or hitting something, like "HIII-YA". (See Ex. #3)

view this post on Zulip Shing Tak Lam (Jul 29 2020 at 01:44):

Rob Lewis said:

Someone should get the Lean one from Kevin's discord.
Kevin Buzzard said:

hmmskell.png

Rob Lewis said:

Also :yeet: please.

I think Bhavik has the original images (he uploaded them), but here's what I downloaded off discord.
image.png
image.png
image.png

view this post on Zulip Johan Commelin (Jul 29 2020 at 04:27):

@Bhavik Mehta :up:

view this post on Zulip Shing Tak Lam (Jul 29 2020 at 07:41):

mhm... why does :yeet: have a black background? Here's the link to the image

view this post on Zulip Rob Lewis (Jul 29 2020 at 08:00):

FYI, everyone should be able to add emoji now. https://leanprover.zulipchat.com/#organization/emoji-settings

view this post on Zulip Rob Lewis (Jul 29 2020 at 08:01):

The Lean one is a little small to read :(

view this post on Zulip Rob Lewis (Jul 29 2020 at 08:01):

Maybe :lean: is better

view this post on Zulip Rob Lewis (Jul 29 2020 at 08:02):

Barely...

view this post on Zulip Mario Carneiro (Jul 29 2020 at 08:11):

Where's that thread with corporate themed lean logos?

view this post on Zulip Johan Commelin (Jul 29 2020 at 08:11):

O.ooo.....

view this post on Zulip Mario Carneiro (Jul 29 2020 at 08:13):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Leaked.20Lean.204.20Logos

view this post on Zulip Johan Commelin (Jul 29 2020 at 11:26):

@Mario Carneiro Does MM0 have a logo already?

view this post on Zulip Mario Carneiro (Jul 29 2020 at 11:27):

No

view this post on Zulip Bhavik Mehta (Jul 29 2020 at 14:39):

Hmm I made :lean: to look good on a dark background, it's unfortunately not great on a white background

view this post on Zulip Kenny Lau (Aug 08 2020 at 03:27):

view this post on Zulip Kenny Lau (Aug 08 2020 at 03:28):

the numbers go like 1, 2, 3, ..., 97, 98, 99, infinity

view this post on Zulip Kevin Buzzard (Aug 08 2020 at 16:27):

That's how nat works

view this post on Zulip Kevin Buzzard (Aug 08 2020 at 16:28):

They just rely on the fact that nobody counts as many as 100 things these days

view this post on Zulip Kevin Buzzard (Aug 08 2020 at 16:28):

So they removed everything from 100 onwards to save space


Last updated: May 08 2021 at 22:13 UTC