social time

Stream: Lean Together 2021

[Rob Lewis]

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]

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

[Rob Lewis]

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]

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]

How do we get links to the zoom?

[Rob Lewis]

See the "meeting links" topic in this stream

[Alena Gusakov]

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]

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]

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

[Stanislas Polu]

Did we just break wonder?

[Sebastian Ullrich]

ditto

[Patrick Massot]

Ok, it's not only me then

[Sebastian Ullrich]

Is that the sign to get back to our seats?

[Floris van Doorn]

oh noes!

[Rob Lewis]

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

[Adam Topaz]

Did we reach some time limit?

[Floris van Doorn]

or participant limit?

[Sebastian Ullrich]

wonderful

[Patrick Massot]

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

[Rob Lewis]

There are no relevant limits AFAIK

[Rob Lewis]

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

[Jakob von Raumer]

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

[Gabriel Ebner]

Is wonder down again?

[Kevin Buzzard]

down for me

[Gabriel Ebner]

We did it guys! Great job everyone!

[Ender Doe]

Down for me

[Patrick Massot]

Who has a great backup plan?

[Kevin Buzzard]

let's go down the pub

[Heather Macbeth]

Zoom, randomly generated breakout rooms?

[Johan Commelin]

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

[Johan Commelin]

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

[Rob Lewis]

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]

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

[Mario Carneiro]

was the zoom supposed to go down?

[Mario Carneiro]

it seems the passing of the scepter didn't work

[Jakob von Raumer]

There was nobody accepting the burden of the scepter

[Rob Lewis]

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

[Mario Carneiro]

that's fine

[Rob Lewis]

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]

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

[Rob Lewis]

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]

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

[Rob Lewis]

Same links

[Jannis Limperg]

Ah, found them. Sorry, bit slow today.

[Rob Lewis]

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

[Rob Lewis]

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]

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]

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

[Rob Lewis]

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

[Rob Lewis]

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

[Rob Lewis]

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

[Rob Lewis]

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

[Reid Barton]

:bell:

[Rob Lewis]

We will resume at 2021-01-06T20:10:00+01:00 , 10 minutes later than the schedule says!

[Rob Lewis]

They fixed Wonder now :upside_down:

[Mohamed Al-Fahim]

Rob Lewis said:

They fixed Wonder now :upside_down:

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

[Jakob von Raumer]

People are still on gather.town

[Mohamed Al-Fahim]

So should we move to Wonder?

[Sebastian Ullrich]

We're nowhere near the limit of Gather

[Mohamed Al-Fahim]

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