landing post for newcomers

Stream: Zulip meta

[Arthur Paulino]

Do you guys think it would be nice to have new users being directed to a post talking about rules and suggestions for communication via Zulip? For example, I feel like we have to ask for #mwe and talk about #backticks too many times

Going a bit further, what if people were requested to check such a post as seen/read before being able to interact? Is such bureaucracy desired? It's rather common in many communities

[Kevin Buzzard]

I think there is a case for this. It's absolutely true that for many users, their first post is met with someone saying #mwe or #backticks . On my Discord server people are shown a bunch of ground rules and have to click through before they can get going.

[Mario Carneiro]

I think we need to coordinate with zulip to do this, e.g. as part of the welcome bot's PM to new users

[Mario Carneiro]

we could have a bot of our own do welcome posts but that's kind of weird for the user

[Joachim Breitner]

There is value for a new enthusiastic but possibly clueless person to be greeted by a friendly human message, as opposed to some bot asking for click-through bureaucracy. Is the situation so bad that we can't afford humans pointing to #mwe when needed?

[Mario Carneiro]

no, but it might also be preferable for users to not have to be chided in their first human interaction

[Mario Carneiro]

I think plenty of users are trying to do their best and we have a definite lack of capability in automated messaging to new users

[Arthur Paulino]

I was thinking about the possibility of newcomers landing directly on some kind of pinned post rather than us having a bot to send DMs automatically

[Mario Carneiro]

in particular, it's a lot easier to be friendly and say a bunch of useful information with lots of links in a bot message compared to an expert who has to correct yet another clueless newcomer; in the latter case you will usually get just a bare "#backticks" message and it would be a big ask to improve on that

[Mario Carneiro]

pinned posts aren't really a thing in zulip

[Mario Carneiro]

there is the top banner, but I don't think it has a lot of visibility (and it's also stream-specific)

[Arthur Paulino]

I've never noticed the top banner on the mobile app. I think the user has to click on the "i"

[Arthur Paulino]

How would a bot work? Where would it be hosted? Does Zulip provide an endpoint with the information needed?

[Mario Carneiro]

Zulip already has a welcome bot that messages every new user (perhaps you forgot the message you received when you joined). It would be great if we could insert some organization specific text in that message

[Mario Carneiro]

https://leanprover.zulipchat.com/#narrow/is/private/sender/100007-welcome-bot

[Mario Carneiro]

We also have several bots of our own that post on this zulip: https://leanprover.zulipchat.com/#organization/bot-list-admin . As far as I know there is nothing stopping us from having bots PM new users

[Arthur Paulino]

May I kick off a first version of the welcoming message then?

[Mario Carneiro]

sure, if you want to write it be my guest, but we don't have the infrastructure for delivery yet

[Damiano Testa]

Even having #welcome direct to a page with information on #backticks and #mwe might be better: receiving a "welcome" from a human probably feels better than being told off for not using backticks or providing imports.

[Mario Carneiro]

true, but that might be too much of a coded message. If you just posted your first question and it doesn't use backticks, saying #welcome generically does not indicate that there is something wrong with the message just posted that we would like you to fix

[Mario Carneiro]

in particular, I think most users will not realize that they did not provide a MWE and will gloss over that part if not directed specifically to it

[Matthew Ballard]

What about a bot that can be summoned via keyword(s) with canned scripts? People tend to blow past a landing page.

[Arthur Paulino]

The landing page/post idea was dropped in favor of an idea of a bot that sends the message to new members automatically

[Matthew Ballard]

DM? Do you think people will pay more attention to that?

[Mario Carneiro]

I think Matthew is suggesting something different, more like the reddit bot that follows up immediately to a command by a user

[Alya Abbott]

There is a related Zulip issue from a while back: zulip/zulip#3917

I'd love to brainstorm with you guys what a good solution is, and we could take a PR if it requires a new feature (i.e. probably anything other than a bot).

[Arthur Paulino]

Mario Carneiro said:

I think Matthew is suggesting something different, more like the reddit bot that follows up immediately to a command by a user

Got it. But I think it can be a bit noisy for other users unless only the newcomer sees the message

[Arthur Paulino]

Effectively, I believe that the best solution is something along the lines of what Kevin said: having the user confirming that the message was read. This is not only about tips like #mwe and #backticks, but also about the rules of the community and making sure the message is read is quite important

[Mario Carneiro]

@Alya Abbott I think a good Zulip feature which is simple to spec and would help here is the ability for organizations to edit the welcome message sent by the welcome bot to all new users.

[Arthur Paulino]

First prototype:

Welcome to the Lean Community!

This is a place where we talk and ask questions about Lean and projects involving Lean.
You can find more information on about the community [here](https://leanprover-community.github.io/meet.html)

Please make sure to follow the [community guidelines](https://leanprover-community.github.io/meet.html#community-guidelines).

In order to optimize the communication, we
* Use #backticks to format messages that contain Lean code. This makes it easier for everyone to read them
* Provide an #mwe when asking a question, so those willing to help can copy/paste our code to their Lean environment
* Avoid quote-replying long messages to keep the chat less cluttered

Note: Zulip automatically makes some strings like #backticks and #mwe clickable (try clicking on them)

Have a nice stay!

[Patrick Massot]

I would also insist on the fact that the first two items in the list contains http links. It's amazing to see how many people can read #mwe and #backticks without realizing those are links that they are meant to click.

[Arthur Paulino]

Alright, message edited :+1:

[Julian Berman]

deleted -- it's in the note

[Mario Carneiro]

If this replaces the welcome bot message, it will have to be edited to also incorporate stuff from the zulip message, which is still important (it includes stuff like key commands and an encouragement to reply to the bot, although I don't think you can have a conversation with the welcome bot)

[Mario Carneiro]

On the other hand, if zulip wants to make modifications of their own to this message (for example, if the keys change) then they will have difficulty updating the message if it is customized by organizations

[Arthur Paulino]

It can be a second message, sent right after Zulip's current message

[Mario Carneiro]

Here's the message I got (others should speak up if the message has changed since I joined):

Hello, and welcome to Zulip!

This is a private message from me, Welcome Bot. Here are some tips to get you started:
* Download our [Desktop and mobile apps](/apps)
* Customize your account and notifications on your [Settings page](#settings)
* Type `?` to check out Zulip's keyboard shortcuts

The most important shortcut is `r` to reply.

Practice sending a few messages by replying to this conversation. If you're not into keyboards, that's okay too; clicking anywhere on this message will also do the trick!

[Mario Carneiro]

I find it kind of funny that it says the most important shortcut is r to reply because I'm pretty sure I've never used it (enter works as well)

[Alya Abbott]

The message has since been updated:

Hello, and welcome to Zulip!:wave: This is a private message from me, Welcome Bot.

If you are new to Zulip, check out our Getting started guide!

I can also help you get set up! Just click anywhere on this message or press r to reply.

Here are a few messages I understand: apps, profile, theme, streams, topics, message formatting, keyboard shortcuts, help.

[Mario Carneiro]

aha, so you can actually have a conversation with the bot

[Alya Abbott]

Yep. Even if you got the old message, you can still test out what happens when you type in the commands.

[Mario Carneiro]

it seems more natural to have the prompts and suggestion to reply be the last part of the message, so having the organization message come second seems not good either. Maybe it should just be a separate bot, although that is also kind of weird :/

[Mario Carneiro]

I think just replacing the zulip message entirely and incorporating its contents into the message is the best way to go

[Arthur Paulino]

Which one comes first?

[Alya Abbott]

I could see it being:

Hello, and welcome to Zulip!:wave: This is a private message from me, Welcome Bot.

If you are new to Zulip, check out our Getting started guide!

[custom message]

I can also help you get set up! Just click anywhere on this message or press r to reply.

Here are a few messages I understand: apps, profile, theme, streams, topics, message formatting, keyboard shortcuts, help.

[Mario Carneiro]

I would chop the top and bottom off of Arthur's message to make it fit there, but I think we could work with that

[Alya Abbott]

I started a discussion thread in a web-public stream in the Zulip development community. Please feel free to drop by. :)

[Eric Wieser]

To what extent could we solve this problem just by changing the link at https://leanprover-community.github.io/ to not go straight to zulip, but to go via a landing page?

[Arthur Paulino]

Eric Wieser said:

To what extent could we solve this problem just by changing the link at https://leanprover-community.github.io/ to not go straight to zulip, but to go via a landing page?

It depends on how many of the new Zulip members come here via that link

[Arthur Paulino]

IIRC, I found the Zulip link here