Zulip Chat Archive

Stream: FoMM / Lean Together 2020

Topic: Zoom


view this post on Zulip Jeremy Avigad (Jan 02 2020 at 02:45):

We've got 90 people registered! It should be a great meeting. The weather forecast looks o.k. -- comfortably above freezing, no winter storms on the horizon.

I set up Zoom meetings for the sessions for the first day, and posted the links at the bottom of the page here:

http://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/schedule.html

We should be able to start the "meeting" before the session begins, so you can click the link early and watch people file into the room. It might help to pre-install the Zoom app ahead of time, but if you don't, your browser should prompt you to do it when you click the link. It only takes a few seconds.

view this post on Zulip Floris van Doorn (Jan 06 2020 at 14:20):

I've been sick in bed for the last week. I'm recovering now, but I think it's still good for me to stay home today. So even for locals, the Zoom sessions are very welcome!

view this post on Zulip Jeremy Avigad (Jan 06 2020 at 14:22):

We are having some technical difficulties, but the AV guys are here. Hopefully, it will be up soon.

view this post on Zulip Jeremy Avigad (Jan 06 2020 at 14:31):

We can't zoom the camera, but at least we can see the room.

view this post on Zulip Floris van Doorn (Jan 06 2020 at 14:32):

Is it possible to screen share so that we can see the slides?

view this post on Zulip Kevin Buzzard (Jan 06 2020 at 14:34):

I think the general plan is to get it fixed. We haven't started yet

view this post on Zulip Floris van Doorn (Jan 06 2020 at 14:35):

Also, the audio is still off.

view this post on Zulip Rob Lewis (Jan 06 2020 at 14:36):

Is the audio back on?

view this post on Zulip Alex J. Best (Jan 06 2020 at 14:37):

No

view this post on Zulip Floris van Doorn (Jan 06 2020 at 14:37):

no, it's muted

view this post on Zulip Rob Lewis (Jan 06 2020 at 14:37):

There are still complications with the video. We're working on it.

view this post on Zulip Floris van Doorn (Jan 06 2020 at 14:38):

now it's on

view this post on Zulip Wojciech Nawrocki (Jan 06 2020 at 14:39):

Can you hear anything? It's unmuted for me also but with no sound output

view this post on Zulip Floris van Doorn (Jan 06 2020 at 14:39):

Yes, I can hear it well

view this post on Zulip Alex J. Best (Jan 06 2020 at 14:40):

I can also hear

view this post on Zulip Wojciech Nawrocki (Jan 06 2020 at 14:40):

It works now, thanks!

view this post on Zulip Jeremy Avigad (Jan 06 2020 at 14:44):

We can only screen share from the lectern, which is clunky. Is the sound o.k.?
AV will come back at 11 to get it fixed.

view this post on Zulip Rob Lewis (Jan 06 2020 at 14:48):

Kevin just asked a question from the third row. Was that audible on the stream?

view this post on Zulip Rob Lewis (Jan 06 2020 at 14:49):

It looks like the whole room has mics, but I'm not sure which are active.

view this post on Zulip Alex J. Best (Jan 06 2020 at 14:50):

Yes I could hear it fine

view this post on Zulip Kenny Lau (Jan 06 2020 at 14:59):

(where) can we access the slides?

view this post on Zulip Rob Lewis (Jan 06 2020 at 15:01):

We don't have Reid's yet. We do have Cyril's for the next talk: http://cyrilcohen.fr/fomm2020.pdf

view this post on Zulip Manuel Eberl (Jan 06 2020 at 16:05):

Here's mine: https://www21.in.tum.de/~eberlm/pdfs/fomm2020.pdf

view this post on Zulip Floris van Doorn (Jan 06 2020 at 16:13):

The audio quality is pretty low, making it sometimes hard to hear. I don't know whether that is a microphone issue or a Zoom issue.

view this post on Zulip Jeremy Avigad (Jan 06 2020 at 16:24):

The AV guys could not get the zoom working. They will try again during the lunch break, but I am afraid the camera will still be zoomed out for the next session.

view this post on Zulip Kenny Lau (Jan 06 2020 at 16:41):

mic is suddenly not working (10 sec ago)

view this post on Zulip Floris van Doorn (Jan 06 2020 at 16:41):

the audio just got muted

view this post on Zulip Kenny Lau (Jan 06 2020 at 16:41):

after Kevin Buzzard remarked that the d_r is the lcm from 1 to r

view this post on Zulip Kenny Lau (Jan 06 2020 at 16:42):

indeed the audio was muted

view this post on Zulip Kenny Lau (Jan 06 2020 at 16:42):

it's unmuted now

view this post on Zulip Floris van Doorn (Jan 06 2020 at 16:42):

fixed again

view this post on Zulip Rob Lewis (Jan 06 2020 at 16:43):

I tried to turn the volume up before Manuel started, but I'm not sure if it worked. Is the quality any better?

view this post on Zulip Floris van Doorn (Jan 06 2020 at 16:44):

the audio quality is still pretty bad, but I can hear the words that are spoken

view this post on Zulip Rob Lewis (Jan 06 2020 at 16:51):

We'll investigate at lunch. There are lots of weird noises here and I don't know where any of it is coming from.

view this post on Zulip Rob Lewis (Jan 06 2020 at 16:53):

Slides for Sebastien's talk, coming up next: http://robertylewis.com/files/fomm_gouezel.pdf

view this post on Zulip Jeremy Avigad (Jan 06 2020 at 18:38):

I am sorry that the streaming is not working as well as planned. This web page has links to the first two talks after lunch: http://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/schedule.html. (Rob has been posting them on his site; the link addresses are formulaic.) We'll try to get Ulrik's slides up before his talk.

view this post on Zulip Rob Lewis (Jan 06 2020 at 19:38):

We tried to bump up the mic volume again. Has the stream quality improved at all?

view this post on Zulip Ulrik Buchholtz (Jan 06 2020 at 19:57):

I've put my slides on my webpage.

view this post on Zulip Wojciech Nawrocki (Jan 06 2020 at 21:33):

The session 4 (659-260-510) stream just died for me ("waiting for the host to start this meeting")

view this post on Zulip Floris van Doorn (Jan 06 2020 at 21:33):

the meeting got canceled because the host started another meeting.

view this post on Zulip Jeremy Avigad (Jan 06 2020 at 21:46):

Sorry. We don't know what happened, but we got it fixed pretty quickly.

view this post on Zulip Floris van Doorn (Jan 07 2020 at 14:33):

I get the message "the host has another meeting in progress" again.

view this post on Zulip Kevin Buzzard (Jan 07 2020 at 14:38):

Rob is on the case

view this post on Zulip Rob Lewis (Jan 07 2020 at 14:40):

Rob is putting Bruno on the case.

view this post on Zulip Rob Lewis (Jan 07 2020 at 14:41):

And Bruno has put Jeremy on the case.

view this post on Zulip Jeremy Avigad (Jan 07 2020 at 14:43):

Damn, I started the wrong meeting. The meeting ID is 332-471-944. If you change the number in the link (without the hyphens) it should work.

view this post on Zulip Rob Lewis (Jan 07 2020 at 14:44):

https://cmu.zoom.us/j/332471944

view this post on Zulip Jeremy Avigad (Jan 07 2020 at 14:46):

I fixed the link on the web page now.

view this post on Zulip Floris van Doorn (Jan 07 2020 at 14:49):

Thanks!

view this post on Zulip Rob Lewis (Jan 07 2020 at 16:56):

The next talk is Patrick's. I don't think his slides made it to the website yet. For now they're here: http://robertylewis.com/files/fomm_massot.pdf

view this post on Zulip Jeremy Avigad (Jan 07 2020 at 17:37):

They are now also on the website.

view this post on Zulip Jason Rute (Jan 07 2020 at 20:30):

Are the slides for this talk or Markus's talk going to be online?

view this post on Zulip Chris Hughes (Jan 07 2020 at 20:33):

@Reid Barton Are your slides available somewhere?

view this post on Zulip Jeremy Avigad (Jan 07 2020 at 20:58):

We prompted the speakers for slides a few times. He hasn't sent his slides yet, but hopefully we can post them later (together with a recording of his talk).

view this post on Zulip Jeremy Avigad (Jan 07 2020 at 20:59):

(I was responding to Jason, not Chris!)

view this post on Zulip Johan Commelin (Jan 08 2020 at 07:16):

@Markus Rabe I would love to see the slides for your talk. Would you mind sharing them?

view this post on Zulip Jeremy Avigad (Jan 08 2020 at 14:48):

Alas, it seems that he cannot make them public. (Google rules, I guess.)

view this post on Zulip Kevin Buzzard (Jan 08 2020 at 15:29):

Google doesn't want the world to know that they're trying to write an AI which can translate ArXiv into dependent type theory!

view this post on Zulip Johan Commelin (Jan 08 2020 at 15:54):

They do want the world to know, but they don't want the world to know how they do it.

view this post on Zulip Etienne Laurin (Jan 08 2020 at 16:30):

The website reverted to listing yesterday's streams: http://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/schedule.html

view this post on Zulip Etienne Laurin (Jan 08 2020 at 16:37):

The current meeting id seems to be 896-922-652

view this post on Zulip Bruno Bentzen (Jan 08 2020 at 16:37):

The current meeting id seems to be 896-922-652

Yes, this is the correct id.

view this post on Zulip Jeremy Avigad (Jan 08 2020 at 16:40):

Thanks for catching that! The web site is fixed now.

view this post on Zulip Jeremy Avigad (Jan 08 2020 at 17:24):

Let me know if I should ask Gabriel to readjust the microphone to make it louder.

view this post on Zulip Rob Lewis (Jan 09 2020 at 16:50):

If anyone is streaming right now: how is the volume?

view this post on Zulip Cyril Cohen (Jan 09 2020 at 16:56):

If anyone is streaming right now: how is the volume?

Weren't we explicitly told this was not recorded?

view this post on Zulip Rob Lewis (Jan 09 2020 at 16:56):

It's streaming, not being recorded.

view this post on Zulip Cyril Cohen (Jan 09 2020 at 16:56):

It's streaming, not being recorded.

oh,... right

view this post on Zulip Etienne Laurin (Jan 09 2020 at 16:57):

The volume is very good.

view this post on Zulip Agnishom Chattopadhyay (Jan 09 2020 at 16:59):

It's streaming, not being recorded.

unless someone is recording the stream...

view this post on Zulip Rob Lewis (Jan 09 2020 at 17:01):

Please don't :slight_smile:

view this post on Zulip Johan Commelin (Jan 09 2020 at 17:31):

So Lean 4 is classified material?

view this post on Zulip Rob Lewis (Jan 09 2020 at 17:32):

Sorry. To clarify, the talks are being recorded, the informal discussions are not. Sebastian's talk will be put on YouTube afaik.

view this post on Zulip Johan Commelin (Jan 09 2020 at 17:32):

aah, ok

view this post on Zulip Johan Commelin (Jan 09 2020 at 17:33):

I'm looking forward to the youtube versions!

view this post on Zulip Luis Berlioz (Jan 10 2020 at 17:08):

Hi, please find attached the slides for my presentation this afternoon.
TextMiningArXiv.pdf

view this post on Zulip Jeremy Avigad (Jan 10 2020 at 17:10):

I'll put them on the web page during the lunch break.

view this post on Zulip Reid Barton (Jan 10 2020 at 19:26):

Reid Barton Are your slides available somewhere?

There's now available at http://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/slides/fomm_barton.pdf

view this post on Zulip Jeremy Avigad (Jan 10 2020 at 19:49):

Floris doesn't have slides for his talk, but he will use this file for the demo. I'll put it on the web page later. demo_filled.lean

view this post on Zulip Johan Commelin (Jan 13 2020 at 11:44):

Is there an ETA for the youtube videos?

view this post on Zulip Rob Lewis (Jan 14 2020 at 19:01):

I have a long bus ride tomorrow and I'm planning to cut up the recordings then. They'll reach YouTube once I have a stable internet connection.

view this post on Zulip Johan Commelin (Jan 15 2020 at 07:06):

Thanks! I can wait that long (-;

view this post on Zulip Rob Lewis (Jan 15 2020 at 23:11):

The bus ride was productive, videos are cut up into individual talks. Still haven't reached the stable internet connection though. Hopefully tomorrow.

view this post on Zulip Jeremy Avigad (Jan 16 2020 at 00:43):

Were they all there? Bruno and I were worried that we might have lost one or two.

view this post on Zulip Rob Lewis (Jan 16 2020 at 02:16):

Yes, I think every talk was captured by at least one of you.

view this post on Zulip Rob Lewis (Jan 16 2020 at 15:45):

We're missing the very beginning of Ulrik's talk. Otherwise I think we got everything. Here's a playlist: https://www.youtube.com/playlist?list=PLlF-CfQhukNkWwZt45vkNfWfuO-tBBqPN


Last updated: May 18 2021 at 11:11 UTC