Zulip Chat Archive

Stream: Lean Together 2021

Topic: social time


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.

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

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.

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!

Edward Ayers (Jan 04 2021 at 14:03):

How do we get links to the zoom?

Rob Lewis (Jan 04 2021 at 14:03):

See the "meeting links" topic in this stream

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

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 :)

Floris van Doorn (Jan 04 2021 at 16:20):

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

Stanislas Polu (Jan 04 2021 at 16:20):

Did we just break wonder?

Sebastian Ullrich (Jan 04 2021 at 16:20):

ditto

Patrick Massot (Jan 04 2021 at 16:21):

Ok, it's not only me then

Sebastian Ullrich (Jan 04 2021 at 16:21):

Is that the sign to get back to our seats?

Floris van Doorn (Jan 04 2021 at 16:21):

oh noes!

Rob Lewis (Jan 04 2021 at 16:21):

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

Adam Topaz (Jan 04 2021 at 16:22):

Did we reach some time limit?

Floris van Doorn (Jan 04 2021 at 16:22):

or participant limit?

Sebastian Ullrich (Jan 04 2021 at 16:22):

wonderful

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.

Rob Lewis (Jan 04 2021 at 16:24):

There are no relevant limits AFAIK

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.

Jakob von Raumer (Jan 04 2021 at 17:37):

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

Gabriel Ebner (Jan 04 2021 at 18:40):

Is wonder down again?

Kevin Buzzard (Jan 04 2021 at 18:40):

down for me

Gabriel Ebner (Jan 04 2021 at 18:40):

We did it guys! Great job everyone!

Ender Doe (Jan 04 2021 at 18:40):

Down for me

Patrick Massot (Jan 04 2021 at 18:41):

Who has a great backup plan?

Kevin Buzzard (Jan 04 2021 at 18:41):

let's go down the pub

Heather Macbeth (Jan 04 2021 at 18:41):

Zoom, randomly generated breakout rooms?

Johan Commelin (Jan 04 2021 at 18:42):

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

Johan Commelin (Jan 04 2021 at 18:42):

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

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.

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

Mario Carneiro (Jan 04 2021 at 20:54):

was the zoom supposed to go down?

Mario Carneiro (Jan 04 2021 at 20:54):

it seems the passing of the scepter didn't work

Jakob von Raumer (Jan 04 2021 at 20:55):

There was nobody accepting the burden of the scepter

Rob Lewis (Jan 04 2021 at 20:55):

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

Mario Carneiro (Jan 04 2021 at 20:55):

that's fine

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!

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...

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

Jannis Limperg (Jan 05 2021 at 10:53):

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

Rob Lewis (Jan 05 2021 at 10:53):

Same links

Jannis Limperg (Jan 05 2021 at 10:55):

Ah, found them. Sorry, bit slow today.

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

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

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.

Huỳnh Trần Khanh (Jan 05 2021 at 13:04):

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

Rob Lewis (Jan 05 2021 at 16:43):

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

Rob Lewis (Jan 05 2021 at 20:22):

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

Rob Lewis (Jan 05 2021 at 20:22):

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

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

Reid Barton (Jan 06 2021 at 17:02):

:bell:

Rob Lewis (Jan 06 2021 at 18:54):

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

Rob Lewis (Jan 07 2021 at 19:46):

They fixed Wonder now :upside_down:

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?

Jakob von Raumer (Jan 07 2021 at 20:16):

People are still on gather.town

Mohamed Al-Fahim (Jan 07 2021 at 20:17):

So should we move to Wonder?

Sebastian Ullrich (Jan 07 2021 at 20:17):

We're nowhere near the limit of Gather

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: Dec 20 2023 at 11:08 UTC