Zulip Chat Archive

Stream: general

Topic: How do we like Zulip

Sean Leather (Feb 27 2018 at 06:16):

I must say that the linear conversation of Gitter is easier to follow. This interleaving of streams and topics: having to figure out where the conversation flows and which topic to post to is a bit of a cognitive load for casual chat.

Sean Leather (Feb 27 2018 at 06:19):

Perhaps I'm expecting a chat service when maybe I should be expecting a message board.

Moses Schönfinkel (Feb 27 2018 at 06:20):

I completely agree, this is just a dash too much perusing and clicking around and such.

Simon Hudon (Feb 27 2018 at 06:24):

That's too bad. I really like this one. I especially like that it makes it easier to join a conversation after it ran for a while. Often on gitter, so many conversations happened intertwined that I can't get the gist of it when I come back

Moses Schönfinkel (Feb 27 2018 at 06:25):

I've come to accept it as a reality of live chats. One can't follow everything.

Sean Leather (Feb 27 2018 at 06:25):

Yeah, it certainly has some benefits over the single linear thread.

Sean Leather (Feb 27 2018 at 06:26):

But it does naturally require more thought.

Sean Leather (Feb 27 2018 at 06:26):

As is the case for a message board or email.

Sean Leather (Feb 27 2018 at 06:27):

For example, with an email, you have to choose a subject. For chat like Gitter, you don't.

Simon Hudon (Feb 27 2018 at 06:27):

@Moses Schönfinkel But what if one could? maniacal laughter

Simon Hudon (Feb 27 2018 at 06:27):

@Sean Leather That's true but you can still pick a subject halfway through

Moses Schönfinkel (Feb 27 2018 at 06:28):

I am surprised this chat doesn't want me to specify my shoe size when I want to write a message. It feels like an official e-mail requires less mental overhead :).

Sean Leather (Feb 27 2018 at 06:30):

Ooh...

$\int_{0}^{1} f(x) dx$

Mario Carneiro (Feb 27 2018 at 06:30):

I get cheapo mathjax looking at that now

Simon Hudon (Feb 27 2018 at 06:31):

@Moses Schönfinkel Are you saying that you've been reckless enough to not specify your shoe size? gasp

Simon Hudon (Feb 27 2018 at 06:31):

@Sean Leather @Mario Carneiro I sense one more reason to stay

Moses Schönfinkel (Feb 27 2018 at 06:31):

It is sensitive personal information!

Sean Leather (Feb 27 2018 at 06:32):

@Moses Schönfinkel Because you have sensitive feet? :footprints:

Mario Carneiro (Feb 27 2018 at 06:32):

I'm happy to stay for the time being. There really was an issue on gitter with many overlapping conversations

Mario Carneiro (Feb 27 2018 at 06:32):

I don't know if this is the best solution, but I'd like to seriously try to acclimatize before I declaim it

Sean Leather (Feb 27 2018 at 06:33):

I don't know if this is the best solution, but I'd like to seriously try to acclimatize before I declaim it

I agree. I'm just giving my first impressions: a mix of good and bad, not too ugly.

Moses Schönfinkel (Feb 27 2018 at 06:36):

It doesn't. (Mmm, deleting messages doesn't appear to be a thing here.)

Sean Leather (Feb 27 2018 at 06:38):

Is there some way to bless a topic such as this one as the “default” topic? To avoid the needless spawning of new topics.

Andrew Ashworth (Feb 27 2018 at 06:39):

the topics under stream are already sorted by most-recent-use; i don't think it's a big issue?

Sean Leather (Feb 27 2018 at 06:40):

I get cheapo mathjax looking at that now

The fact that it even formats it is better than nothing, I guess. But, yeah, nothing like LaTeX for doing a proper integral.

Sean Leather (Feb 27 2018 at 06:42):

the topics under stream are already sorted by most-recent-use; i don't think it's a big issue?

Perhaps not. It feels like it is, because I'm forced to look at a list of topics under the stream and spend time thinking about it.

Simon Hudon (Feb 27 2018 at 06:42):

(I took the freedom to rename the topic, please, join back :) )

Sean Leather (Feb 27 2018 at 06:42):

I see somebody change the topic, but my latest message didn't make the deadline.

Moses Schönfinkel (Feb 27 2018 at 06:43):

Oh there's a list of topics under streams... I've been clicked on the "All messages" thing.

Andrew Ashworth (Feb 27 2018 at 06:43):

if it's good enough for your L1 processor cache, it should be good enough for you :)

Sean Leather (Feb 27 2018 at 06:43):

@Simon Hudon So the topic changed from your last message? That's interesting, I guess.

Simon Hudon (Feb 27 2018 at 06:44):

I tried to change the topic from the first message I wrote in this conversation

Sean Leather (Feb 27 2018 at 06:44):

@Andrew Ashworth I prefer to keep my L1 flushed as much as possible. :)

Moses Schönfinkel (Feb 27 2018 at 06:46):

Hey that's what Java programmers strive to do! ;)

Sean Leather (Feb 27 2018 at 06:46):

I tried to change the topic from the first message I wrote in this conversation

Oh, I see now that you can change the topic when you edit a message.

Simon Hudon (Feb 27 2018 at 06:47):

I think it's not really well made though. Maybe I should have announced "Changing topic name"

Sean Leather (Feb 27 2018 at 06:47):

Oh, I see now that you can change the topic when you edit a message.

Oh, that's sneaky. So, I can choose to change the topic for any thread and force all of the following messages onto that topic.

Simon Hudon (Feb 27 2018 at 06:47):

Right now @Sean Leather , you could go at the beginning of this segment and merge back into the topic I created

Moses Schönfinkel (Feb 27 2018 at 06:47):

Next thing you know you're contributing to "Trump is an excellent president" topic.

Simon Hudon (Feb 27 2018 at 06:48):

I think we're protected from that: studying logic requires some amount of brain matter

Sean Leather (Feb 27 2018 at 06:49):

Right now @Sean Leather , you could go at the beginning of this segment and merge back into the topic I created

Indeed, you are right.

Simon Hudon (Feb 27 2018 at 06:49):

congrats @Sean Leather, you've done your first topic highjack

Sean Leather (Feb 27 2018 at 06:51):

So, topics are not first-class. You can merge messages just by changing the name of the topic.

Sean Leather (Feb 27 2018 at 06:51):

That's also sneaky.

Sean Leather (Feb 27 2018 at 06:52):

I wonder why Zulip doesn't support deleting messages.

Sean Leather (Feb 27 2018 at 06:55):

So, I should not even be expecting a message board here. Topics are usually decided universally on a message board. But here, it's haphazard.

Simon Hudon (Feb 27 2018 at 06:56):

I guess if you want to delete a message, you can change its topic to "trash"

Mario Carneiro (Feb 27 2018 at 06:58):

The fact that it even formats it is better than nothing, I guess. But, yeah, nothing like LaTeX for doing a proper integral.

No, I mean I see the "quick mode" rendering of MathJax, as opposed to the "professional style" that it normally updates to after a few seconds on other sites

Sean Leather (Feb 27 2018 at 07:00):

No, I mean I see the "quick mode" rendering of MathJax, as opposed to the "professional style" that it normally updates to after a few seconds on other sites

Sorry, I don't know the difference.

Sean Leather (Feb 27 2018 at 07:01):

Oh, I think I see it at https://www.mathjax.org/#demo

Kevin Buzzard (Feb 27 2018 at 08:02):

FWIW the lack of threads on gitter didn't bother me as there was rarely more than one or two going on at once. What was really beginning to bite me on gitter was that the search was so poor -- I never even figured out how to search for e.g. "all comments from Johannes made between 1 and 3 months ago", which was something I really wanted to do a day or two ago. Also there was a scroll bug, and there was unread messages bugs etc (but these were more minor in the sense that I had figured out workarounds)

Sebastian Ullrich (Feb 27 2018 at 08:33):

I do like this view in the morningScreenshot-from-2018-02-27-09-30-37.png

Kevin Buzzard (Feb 27 2018 at 08:34):

I agree that it makes it very clear what has been going on.

Simon Hudon (Feb 27 2018 at 08:35):

Nice summary! That probably makes it easier to skip some conversations too

Sebastian Ullrich (Feb 27 2018 at 08:36):

Yeah, I can skip all this mathy stuff :laughing:

Sean Leather (Feb 27 2018 at 08:37):

I like the emoji tags on messages. More of it reduces the overall noise.

Simon Hudon (Feb 27 2018 at 08:37):

Actually, no offense @Kevin Buzzard but often I wake up to find you had a long conversation with Kenny and @Mario Carneiro about stuff I don't know much about. I'd love to be able to if there's anything I could take away from it

Mario Carneiro (Feb 27 2018 at 08:38):

yep, we all have our specializations

Simon Hudon (Feb 27 2018 at 08:38):

@Sean Leather All that's missing is tallying up those emoji's to see who has the highest score

Simon Hudon (Feb 27 2018 at 08:38):

@Mario Carneiro Is there any specialization that isn't yours?

Mario Carneiro (Feb 27 2018 at 08:40):

I'm okay, not great, at underwater basketweaving

Simon Hudon (Feb 27 2018 at 08:45):

You disappoint me

Mario Carneiro (Feb 27 2018 at 08:56):

It should now be possible to delete your own posts here.

Mario Carneiro (Feb 27 2018 at 08:57):

I can't seem to delete a stream though... just ignore #mathlib travis, the actual travis CI pushes to #travis

Patrick Massot (Feb 27 2018 at 08:58):

Maybe @Sebastian Ullrich has more admin rights and could do it?

Mario Carneiro (Feb 27 2018 at 08:58):

He adminified me, but I still can't. Zulip doesn't seem to like deletion in general

Mario Carneiro (Feb 27 2018 at 08:59):

I mean it makes sense, deleting a stream could potentially involve a huge loss of information

Mario Carneiro (Feb 27 2018 at 09:00):

I can kick everyone off the stream and make it private tho :)

Sebastian Ullrich (Feb 27 2018 at 09:09):

I deleted mathlib travis. I have a tab "Delete streams" in the organization settings.

Mario Carneiro (Feb 27 2018 at 09:17):

Ah, found it. I had to log out and in again

Sebastian Ullrich (Feb 27 2018 at 09:18):

Heh, I guess it's not completely mature yet in every regard

Scott Morrison (Feb 27 2018 at 09:31):

I really don't like Zulip. For me it is very slow and unresponsive, and I don't like having everything tucked away in different threads that I have to individually open and scan.

Patrick Massot (Feb 27 2018 at 09:32):

You can click "All messages" on the top left corner to get everything mixed as in gitter

Patrick Massot (Feb 27 2018 at 09:32):

And it's very responsive here

Patrick Massot (Feb 27 2018 at 09:32):

Maybe Australia is too far away :(

Sean Leather (Feb 27 2018 at 09:32):

For me it is very slow and unresponsive

That's interesting. I was just noticing how fast it is. And I'm rather used to slow sites, being in South Africa.

Scott Morrison (Feb 27 2018 at 09:34):

Whenever I click on something a pulsing blue circle appears, seeming to show that something is trying to load?

Patrick Massot (Feb 27 2018 at 09:34):

That circle indicates some tip is available

Andrew Ashworth (Feb 27 2018 at 09:34):

those are the new user tutorial popups

Sean Leather (Feb 27 2018 at 09:34):

Ah! I was confused about that, too, in the beginning.

Patrick Massot (Feb 27 2018 at 09:34):

Click on it to read the tip and it won't show up again

Sean Leather (Feb 27 2018 at 09:35):

I thought the same thing. It's a misleading animation.

Simon Hudon (Feb 27 2018 at 09:35):

I had no idea! Thanks guys!

Scott Morrison (Feb 27 2018 at 09:35):

Oops, thanks!

Scott Morrison (Feb 27 2018 at 09:36):

Ok. Seems fine to me now :-)

Kevin Buzzard (Feb 27 2018 at 22:02):

You can star stuff (presumably to favourite it). I _really_ like this because occasionally a guru says something when I'm scanning through old chat and I think "ooh that needs some more thought at some point". This happens fairly often to me in fact.

Simon Hudon (Feb 27 2018 at 22:06):

Nice! I'm going to try it out

Sebastian Ullrich (Mar 02 2018 at 10:19):

Soo... looks like we're staying here?

Kevin Buzzard (Mar 02 2018 at 10:19):

I prefer it to gitter

Kevin Buzzard (Mar 02 2018 at 10:19):

For me the starring of messages is a game changer

Patrick Massot (Mar 02 2018 at 10:19):

I'm worried that we are still missing Johannes.

Kevin Buzzard (Mar 02 2018 at 10:20):

Often people write things and I think "I should follow up on this later" and before I had to cut and paste some URL and add it to a text file

Patrick Massot (Mar 02 2018 at 10:20):

He was not very active on gitter but still there

Kevin Buzzard (Mar 02 2018 at 10:20):

now I just star

Sebastian Ullrich (Mar 02 2018 at 10:20):

It's really bad for my productivity. I'm much more inclined to participate here than on Gitter.

Kevin Buzzard (Mar 02 2018 at 10:20):

Oh :-(

Sebastian Ullrich (Mar 02 2018 at 10:21):

Kevin Buzzard (Mar 02 2018 at 10:21):

Just close the tab?

Patrick Massot (Mar 02 2018 at 10:21):

:smile:

Kevin Buzzard (Mar 02 2018 at 10:21):

I had the tab closed for 24 hours just now because I was busy

Sebastian Ullrich (Mar 02 2018 at 10:21):

@Patrick Massot Try pinging him on Gitter

Kevin Buzzard (Mar 02 2018 at 10:21):

and I just opened it again this morning and read through all the messages. I really liked that they were sorted into categories.

Sean Leather (Mar 02 2018 at 10:22):

It's really bad for my productivity. I'm much more inclined to participate here than on Gitter.

@Sebastian Ullrich: On the other hand, your participation is highly valued by the rest of us, so your productivity loss surely comes as a universal gain for everyone. :simple_smile:

Kevin Buzzard (Mar 02 2018 at 10:23):

And I also really liked that I didn't have to deal with "24 unread ^ up there" because gitter was confused about what I had read and what I hadn't read, and the silly bugs that are there (at least on Ubuntu with Chrome) where you look at old messages and then scroll down and there are some missing messages and then you're right back up to date except that you're not because it looks like someone just said something but actually they said it yesterday

Patrick Massot (Mar 02 2018 at 10:25):

We still need that Sebastian has some productivity. He needs to get that monad stuff merged before opening that [WIP] new parser PR

Sean Leather (Mar 02 2018 at 10:26):

We still need that Sebastian has some productivity. He needs to get that monad stuff merged before opening that [WIP] new parser PR

Oh, absolutely! I just wanted to point out that one person's trash (lost productivity) may still be multiple other people's treasure (enlightenment).

Johannes Hölzl (Mar 02 2018 at 11:16):

I'm here now. I like the topics, makes it easier to follow whats going on.

Patrick Massot (Mar 02 2018 at 11:50):

Great!

Patrick Massot (Mar 02 2018 at 11:51):

Go for the chain rule topic :wink:

Patrick Massot (Mar 02 2018 at 11:53):

@Patrick Massot Try pinging him on Gitter

@Sebastian Ullrich you were right, it worked

Patrick Massot (Mar 02 2018 at 22:06):

@Reid Barton did you make any progress about the syntax highlighting update?

Reid Barton (Mar 04 2018 at 16:23):

@Patrick Massot Thanks for the reminder. I filed a Zulip issue: https://github.com/zulip/zulip/issues/8574

Patrick Massot (Mar 26 2018 at 19:26):

It seems we never followed on this https://github.com/zulip/zulip/issues/8574

Patrick Massot (Mar 26 2018 at 19:27):

@Sebastian Ullrich Shouldn't we modify https://github.com/leanprover/leanprover.github.io/blob/master/documentation/index.md to mention Zulip instead of Gitter? I could make a PR if you want

Kevin Buzzard (Mar 29 2018 at 09:52):

Zulip eats my indentation and appends random newlines when I cut and paste from VS Code lean buffers, on Firefox/Ubuntu. Is there a fix for this?

Kevin Buzzard (Mar 29 2018 at 09:53):

theorem  ev_sum : ∀ {n m}, ev n → ev m → ev (n + m) :=

begin

intros n m Hn Hm,

induction Hm with d Hd Hnd,

{ assumption },

{ apply ev_SS,

assumption}

end

Kenny Lau (Mar 29 2018 at 09:53):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/idly.20trying.20software.20foundations/near/124295607

Kevin Buzzard (Mar 29 2018 at 09:53):

That was correctly indented with no blank lines in VS Code

Kevin Buzzard (Mar 29 2018 at 09:54):

Sure but now I'm noting this in the correct place.

Kevin Buzzard (Mar 29 2018 at 09:54):

PS spoiler alert ;-)

Kenny Lau (Mar 29 2018 at 14:47):

@Kevin Buzzard fix: paste your content in editpad.org and then re-copy-and-paste

Mario Carneiro (Mar 29 2018 at 18:21):

The problem is VSCode formatted copy, which is currently not disable-able, but you can work around it by pasting into notepad or a new plain text file in VSCode (to strip the colors), and then copying that text and pasting here