tutorials

Stream: Lean for the curious mathematician 2020

[Jeremy Avigad]

On the second day, I am down for 3.5 hours of tutorials (based in MiL). I am thinking of something like the following format:

• I lecture and demo for about 20 minutes.
• We ask people to work on a (short) pre-prepared list of exercises for about 20 minutes, with weird Zoom silence while people play around with them. We can answer verbal questions and questions posed in the chat.
• I then call everyone back and we work through the exercises together.
• Repeat.
  I am anxious about this plan. It could work or it could be a real mess. Does anyone have any thoughts on the matter?

[Patrick Massot]

My vague idea was to emulate having this is a room full of computers with experienced Lean users walking from computers to computers to help people doing the exercises. But of course, besides technical issues, this depends a lot on the number of participants.

[Patrick Massot]

Right now it seems feasible, but I have no idea how many people will actually show up.

[Jeremy Avigad]

So people get to share their screens to ask questions? Or use breakout rooms? Or use the Zulip channel or the chat window?

Are we using Zoom? Zoom has breakout groups, so we can break participants into small groups (say, groups of five) and instructors can go from group to group.

[Rob Lewis]

My impression from watching a few days of IJCAR is: pre-recorded conference talks are unpleasant. Maybe nobody was planning to do this at LFTCM anyway. But I think we should try to avoid the "record a 30 minute talk and pretend it's live" style.

[Mario Carneiro]

My impression from the PLDI presentations was that they tend to be more rushed and dense

[Rob Lewis]

Exactly. I'm pretty certain I've seen a few where they sped them up to fit them in the time slot, it was horrible to listen to.

[Mario Carneiro]

which is good for student presentations that have received far too little time I guess, but is not too pleasant for the audience

[Rob Lewis]

For the metaprogramming tutorial I'm assigned at LFTCM, my plan was to record a series of short(ish) videos and just put them on YouTube. No pretense that they're live talks at conference time. They'll probably get many more views after the fact than "live" anyway, so it seems better to optimize for that.

[Jalex Stark]

I see, so you wouldn't have a scheduled time where people all watch the video

[Mario Carneiro]

are you going to play them during the time slot?

[Rob Lewis]

This doesn't work for the more intro-level talks where you expect questions in the middle.

[Rob Lewis]

Mario Carneiro said:

are you going to play them during the time slot?

No, I've already seen multiple issues today at IJCAR with trying to stream videos over Zoom. It seems dumb, just point people to the video links and let them stream themselves...

[Rob Lewis]

We can say, "everyone start watching these videos at 1pm" or whatever.

[Jeremy Avigad]

@Johan Commelin Is the plan to use Zoom? I am still thinking of a format where I give a short presentation, then we ask people to work on exercises (maybe posted as a gist where everyone can cut-and-paste them). If we have Zoom we can put people in breakout rooms and mathlib experts can go from room to room answering questions.

[Rob Lewis]

Some people involved had security/privacy/ethics concerns about Zoom, I don't remember where the discussion landed. Personally, I'm not so worried about that and wouldn't compromise on reliability and features just to avoid Zoom.

[Patrick Massot]

The main practical point is that nobody volunteered to actively investigate alternatives, especially if it involves setting up a server.

[Bhavik Mehta]

Zoom seems to do breakout rooms well, I've seen some people using jitsi with some success as well though. For one to one work I found Microsoft Teams the most convenient

[Bhavik Mehta]

There's also timeout.srcf.net, made by some students at Cambridge which has the same features as Zoom but without the security problems (essentially because they didn't like that the university wasn't helping enough with remote working) but unfortunately it seems that rooms can only be made by cambridge accounts

[Patrick Massot]

It seems the Cambridge thing is simply BigBlueButton rebranded.

[Jeremy Avigad]

I don't have any strong opinions, but it would be nice to have a decision, so I can try out the system. (Zoom is convenient because I already know how to use it.)

[Johan Commelin]

For zoom we would need some paid accounts to host it, I guess.

[Johan Commelin]

I don't have those

[Johan Commelin]

Would CMU be able to provide them?

[Johan Commelin]

I could ask my dept for BBB rooms

[Johan Commelin]

I'm pretty sure they would set up as many rooms as we want

[Johan Commelin]

@Jeremy Avigad Are you familiar with BBB (BigBlueButton) ?

[Johan Commelin]

Rob Lewis said:

For the metaprogramming tutorial I'm assigned at LFTCM, my plan was to record a series of short(ish) videos and just put them on YouTube. No pretense that they're live talks at conference time. They'll probably get many more views after the fact than "live" anyway, so it seems better to optimize for that.

I think that's a great decision.

[Johan Commelin]

It would be good if the material of this workshop would be available and helpful afterwards for people who want to learn stuff when it's December :wink:

[Mario Carneiro]

Am I on the hook for anything? I have been trying to avoid thinking about the workshop until I get back to PGH this weekend

[Johan Commelin]

@Mario Carneiro You're supposed to do 24/7 all-round support on Zulip (-; :wink: :grinning: :oops:

[Mario Carneiro]

oh is that all?

[Johan Commelin]

You're the only one that can do 5 all-nighters in one week

[Mario Carneiro]

lol

[Mario Carneiro]

:smile: :upside_down: :smile: :upside_down: :smile: :upside_down:

[Johan Commelin]

The idea is that there will be spontaneous breakouts and pair programming sessions

[Johan Commelin]

It would be great if you can help with those

[Johan Commelin]

(That's one reason I would like VScode Live Share to work 1 week from now)

[Jeremy Avigad]

Carnegie Mellon has a Zoom subscription, so everyone with a CMU account can hold a meeting with up to 300 people. I think I can start a meeting and then transfer or share the host role with anyone else. That will work for the afternoon sessions. But I don't want to get up at 4 am to start a Zoom meeting in the mornings.

[Jeremy Avigad]

We can even have different people using different systems. In any case, the question is how to share the links. Are people registering for the conference? Is there an email list that we can use?

[Mario Carneiro]

I think this stream is the coordination point for the conference

[Mario Carneiro]

so I guess the links should be posted in a topic here

[Mario Carneiro]

Registration is here

[Jeremy Avigad]

Oh, good. So, for my session, I can easily post a link here, and then promote any Lean experts around to co-host, so that they can go from room to room. I'll test that out ahead of time.

[Patrick Massot]

Mario, if you are disappointed that your name doesn't appear in the schedule, we can arrange that very easily.

[Patrick Massot]

For instance I have two slots, you can take one. The first one is intended to roughly cover Chapter 2 of MIL, although there is no way the participants will have time to do all exercises of course..

[Patrick Massot]

But in any case we hope we'll need a lot of people to help during the exercises sessions. Hopefully this is not only about answering questions on Zulip, we hope at least some participants will be able to share their screens to receive help.

[Patrick Massot]

About technical questions, we really need to try stuff soon.

[Rob Lewis]

Johan Commelin said:

For zoom we would need some paid accounts to host it, I guess.

The VU also has a subscription big enough to do large lectures, which I think will be more than enough for this. And I'm in a more convenient time zone than Jeremy to make sure things are working in the morning.

[Rob Lewis]

We also have a Google Meetings subscription so you can pick your poison. My impression is that people are settling on Zoom over Google in general.

[Rob Lewis]

I'm happy to configure/test Zoom or Google stuff. Used both enough while I was teaching that I know basically what I'm doing there. I don't have time the next few weeks to figure out where and how to self-host a Jitsi server though.

[Rob Lewis]

Jeremy Avigad said:

We can even have different people using different systems. In any case, the question is how to share the links. Are people registering for the conference? Is there an email list that we can use?

Using different systems seems like it's asking for trouble. We should really try to standardize on one platform as much as possible. I think "recorded talks are on YouTube, live stuff is on Zoom or whatever" is fine, everyone knows how to use YouTube and there's no interaction. But let's not make people switch from Twitch to Zoom to Jitsi and back.

[Rob Lewis]

At least with Zoom, you can have one meeting for the whole week. I've never tried but I'm pretty sure you can easily change host permissions so different people can create breakout rooms etc.

[Jeremy Avigad]

Yeah, when you create a meeting with Zoom, you can reserve the ID / link so that it is yours until it is released. But I think only the host can start. So e.g. if VU hosts for the week, Rob has to start the meeting every day. He can then designate co hosts, and if I understand correctly, the co hosts can designate co hosts.

Oh, and it looks like only the host can create breakout rooms. https://support.zoom.us/hc/en-us/articles/206330935-Enabling-and-adding-a-co-host

[Rob Lewis]

Ah, starting the meeting every day is easy enough (especially since I could delegate to anyone else at the VU). The breakout room restrictions are a little more annoying.

[Patrick Massot]

Can you delegate the breakout rooms creation?

[Patrick Massot]

We can't ask you to be there all day long for all week.

[Rob Lewis]

Not to any random person; possibly to people at the VU, it's unclear.

[Jeremy Avigad]

Actually, Rob, I think you can start the meeting, and then make anyone else the host. If you are awake and up for it, we can try it. Just start a Zoom meeting and email me the link.

[Jeremy Avigad]

Oh, it looks like Rob is gone now.

[Rob Lewis]

I'm back! One sec

[Rob Lewis]

@Jeremy Avigad I sent you an invite. But we should also test with someone who doesn't have a licensed Zoom account.

[Johan Commelin]

/me guinea pig?

[Jeremy Avigad]

Strange, I didn't get it...

[Jeremy Avigad]

Sorry, that was a response to Rob.

[Rob Lewis]

In a private message here!

[Rob Lewis]

Conclusion: we can transfer host privileges around as much as we want. So I could start a meeting, make Johan the host, and leave, and he can create and assign breakout rooms.

[Rob Lewis]

The downside is, it seems only the host can add people to breakout rooms. So if there are "experts" floating around multiple rooms they might need some assistance.

[Johan Commelin]

We didn't actually try what happens if you leave completely... but I guess it should work. You still had some superpowers that I didn't. Because you could reclaim being a host.

[Rob Lewis]

True. I'm sure I can leave at least temporarily because of internet outages. Worst case I could just start things up on my old laptop and leave it in a corner.

[Dan Stanescu]

@Rob Lewis Rob, AFAIK you can designate random co-hosts after the session starts, but you can designate people at VU as co-hosts ahead of time on the Zoom website.

[Rob Lewis]

Ah, maybe. There's a difference between "co-host" and "alternate host" in their documentation but I'm not sure how that's reflected on the site/in the program.

[Rob Lewis]

Yeah, I can set an "alternative host" when I schedule the meeting on the website, and the docs say it has to be someone licensed on the same account. That person can start the meeting.

[Rob Lewis]

And then "co-host" inside the meeting is less powerful than a full host, but you can assign whoever you want to be the full host, and any number of co-hosts.

[Dan Stanescu]

So this allows you to have someone at VU as "alternative host" just for backup, if anyone is available. They can start the meeting.

[Rob Lewis]

Yep, that's perfect.

[Dima Pasechnik]

Google Meet is a reasonable alternative to Zoom, with very similar options. It is essentially setup-free.

[Dan Stanescu]

How many people can get together with Google Meet now? I think this is what used to make it less interesting than Zoom.

[Dima Pasechnik]

up to 250, and you can also record meetings.

[Philip Vetter]

Hello, I don't see a video stream happening. Am I in the wrong place?

[Floris van Doorn]

Welcome! You are in the right place, but the Zoom meeting has not started yet. The install session is a bit different, since we don't expect anyone to stick around for the full 5 hours. For now you can start watching the Youtube playlist on how to install Lean and ask questions here: https://www.youtube.com/playlist?list=PLlF-CfQhukNnxF1S22cNGKyfOrd380NUv