Zulip Chat Archive

Stream: Lean Together 2021

Topic: social time


view this post on Zulip Rob Lewis (Jan 04 2021 at 12:29):

We're trying out wonder.io for the social time for this workshop, since Zoom isn't a great venue for mingling. This is a bit of an experiment, so let's hope it goes smoothly! The Wonder interface is a little funny -- clicking on the map makes your avatar run around, and it's easy to accidentally lock your "circle" so nobody else can join. But when we tested it out a few weeks ago it made sense quickly enough.

view this post on Zulip Rob Lewis (Jan 04 2021 at 12:29):

The link to the room is here: https://www.wonder.me/r?id=f3cc3041-0c16-42df-a556-ae77b316c113

view this post on Zulip Rob Lewis (Jan 04 2021 at 12:30):

This is technically always open, you can log in any time. We have official social time after each day's events and I'll try to hang out there a bit before as well.

view this post on Zulip Rob Lewis (Jan 04 2021 at 12:31):

Tonight's "conference dinner" is nothing special, just an extra-emphasized social hour. These things are better if more people attend, so if you have to pick one, try for that one!

view this post on Zulip Edward Ayers (Jan 04 2021 at 14:03):

How do we get links to the zoom?

view this post on Zulip Rob Lewis (Jan 04 2021 at 14:03):

See the "meeting links" topic in this stream

view this post on Zulip Alena Gusakov (Jan 04 2021 at 15:59):

Hey so I feel like it's worth mentioning - I wanted to attend the social hour for today but something serious has come up

view this post on Zulip Rob Lewis (Jan 04 2021 at 16:07):

Alena Gusakov said:

Hey so I feel like it's worth mentioning - I wanted to attend the social hour for today but something serious has come up

Hope everything is okay! Maybe we'll catch you another day :)

view this post on Zulip Floris van Doorn (Jan 04 2021 at 16:20):

Am I the only one that doesn't hear / see others right now?

view this post on Zulip Stanislas Polu (Jan 04 2021 at 16:20):

Did we just break wonder?

view this post on Zulip Sebastian Ullrich (Jan 04 2021 at 16:20):

ditto

view this post on Zulip Patrick Massot (Jan 04 2021 at 16:21):

Ok, it's not only me then

view this post on Zulip Sebastian Ullrich (Jan 04 2021 at 16:21):

Is that the sign to get back to our seats?

view this post on Zulip Floris van Doorn (Jan 04 2021 at 16:21):

oh noes!

view this post on Zulip Rob Lewis (Jan 04 2021 at 16:21):

This is not intentional, at least not done by me -- no idea what's going on

view this post on Zulip Adam Topaz (Jan 04 2021 at 16:22):

Did we reach some time limit?

view this post on Zulip Floris van Doorn (Jan 04 2021 at 16:22):

or participant limit?

view this post on Zulip Sebastian Ullrich (Jan 04 2021 at 16:22):

wonderful

view this post on Zulip Patrick Massot (Jan 04 2021 at 16:23):

I thought about having a nice way to call everybody back to work but this is a bit early.

view this post on Zulip Rob Lewis (Jan 04 2021 at 16:24):

There are no relevant limits AFAIK

view this post on Zulip Rob Lewis (Jan 04 2021 at 16:24):

Let's see if it's fixed after the next talk. If not I'll create a new room.

view this post on Zulip Jakob von Raumer (Jan 04 2021 at 17:37):

Slack is experiencing an outage as well, maybe that's somehow related...

view this post on Zulip Gabriel Ebner (Jan 04 2021 at 18:40):

Is wonder down again?

view this post on Zulip Kevin Buzzard (Jan 04 2021 at 18:40):

down for me

view this post on Zulip Gabriel Ebner (Jan 04 2021 at 18:40):

We did it guys! Great job everyone!

view this post on Zulip Ender Doe (Jan 04 2021 at 18:40):

Down for me

view this post on Zulip Patrick Massot (Jan 04 2021 at 18:41):

Who has a great backup plan?

view this post on Zulip Kevin Buzzard (Jan 04 2021 at 18:41):

let's go down the pub

view this post on Zulip Heather Macbeth (Jan 04 2021 at 18:41):

Zoom, randomly generated breakout rooms?

view this post on Zulip Johan Commelin (Jan 04 2021 at 18:42):

I wouldn't mind doing a porting discussion on Zoom now

view this post on Zulip Johan Commelin (Jan 04 2021 at 18:42):

maybe people can distribute themselves over 3 ad hoc gather.town instances?

view this post on Zulip Rob Lewis (Jan 04 2021 at 18:49):

Here's the deal: we're back in Zoom. The main room is discussing porting mathlib to Lean 4. The breakout rooms are for casual chat.

view this post on Zulip Rob Lewis (Jan 04 2021 at 18:50):

Ping me if you want to move to a new breakout room. You can always go back to the main stream

view this post on Zulip Mario Carneiro (Jan 04 2021 at 20:54):

was the zoom supposed to go down?

view this post on Zulip Mario Carneiro (Jan 04 2021 at 20:54):

it seems the passing of the scepter didn't work

view this post on Zulip Jakob von Raumer (Jan 04 2021 at 20:55):

There was nobody accepting the burden of the scepter

view this post on Zulip Rob Lewis (Jan 04 2021 at 20:55):

Yeah, I thought we were done, most of the faces disappeared

view this post on Zulip Mario Carneiro (Jan 04 2021 at 20:55):

that's fine

view this post on Zulip Rob Lewis (Jan 04 2021 at 20:57):

I'm going to try to reach Wonder support. In the meantime, https://comingle.csail.mit.edu/ was suggested as an alternative. I won't have time to test it out before tomorrow's session starts, but if anyone wants to investigate, please let me know!

view this post on Zulip Jakob von Raumer (Jan 04 2021 at 21:00):

It's a bit strange that they seem to have no social media presence and no status page...

view this post on Zulip Rob Lewis (Jan 05 2021 at 10:11):

No response from the Wonder people yet. The backup plan, if we don't hear from them, will be distributing over a couple Gather instances. Not ideal but better than Zoom breakout rooms

view this post on Zulip Jannis Limperg (Jan 05 2021 at 10:53):

Do we have Zoom links for today already? I'm failing to find them.

view this post on Zulip Rob Lewis (Jan 05 2021 at 10:53):

Same links

view this post on Zulip Jannis Limperg (Jan 05 2021 at 10:55):

Ah, found them. Sorry, bit slow today.

view this post on Zulip Rob Lewis (Jan 05 2021 at 12:29):

Let's try Gather for this coffee break: https://gather.town/app/U60XhAzwwDUlWbzD/lean-together-2021-1

view this post on Zulip Rob Lewis (Jan 05 2021 at 12:37):

Let me know if you get denied entry or anything. It looks like we haven't hit the 25 person cap yet

view this post on Zulip Huỳnh Trần Khanh (Jan 05 2021 at 13:04):

Gather is awesome :heart_eyes: I can walk around the room and listen to other people talking. I know zip about this stuff so I couldn't join the conversations LOL. But it feels so awesome and the conversations are really interesting.

view this post on Zulip Huỳnh Trần Khanh (Jan 05 2021 at 13:04):

I guess I'm the only teenager in the room, haha.

view this post on Zulip Rob Lewis (Jan 05 2021 at 16:43):

I see we have 25 people now. Has anyone been rejected trying to join?

view this post on Zulip Rob Lewis (Jan 05 2021 at 20:22):

I take it there was no trouble with Gather after I left?

view this post on Zulip Rob Lewis (Jan 05 2021 at 20:22):

If not, this is now the official social room for the workshop.

view this post on Zulip Rob Lewis (Jan 06 2021 at 16:34):

The social time (coffee break starting soon) will be on Gather again: https://gather.town/app/U60XhAzwwDUlWbzD/lean-together-2021-1

view this post on Zulip Reid Barton (Jan 06 2021 at 17:02):

:bell:

view this post on Zulip Rob Lewis (Jan 06 2021 at 18:54):

We will resume at , 10 minutes later than the schedule says!

view this post on Zulip Rob Lewis (Jan 07 2021 at 19:46):

They fixed Wonder now :upside_down:

view this post on Zulip Mohamed Al-Fahim (Jan 07 2021 at 20:16):

Rob Lewis said:

They fixed Wonder now :upside_down:

Are we going to use the same Wonder link from before?

view this post on Zulip Jakob von Raumer (Jan 07 2021 at 20:16):

People are still on gather.town

view this post on Zulip Mohamed Al-Fahim (Jan 07 2021 at 20:17):

So should we move to Wonder?

view this post on Zulip Sebastian Ullrich (Jan 07 2021 at 20:17):

We're nowhere near the limit of Gather

view this post on Zulip Mohamed Al-Fahim (Jan 07 2021 at 20:18):

I see. For a second, I thought Rob wanted us to move to Wonder since it got fixed.


Last updated: May 08 2021 at 21:09 UTC