Zulip Chat Archive
Stream: FoMM / Lean Together 2020
Topic: Zoom
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.
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!
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.
Jeremy Avigad (Jan 06 2020 at 14:31):
We can't zoom the camera, but at least we can see the room.
Floris van Doorn (Jan 06 2020 at 14:32):
Is it possible to screen share so that we can see the slides?
Kevin Buzzard (Jan 06 2020 at 14:34):
I think the general plan is to get it fixed. We haven't started yet
Floris van Doorn (Jan 06 2020 at 14:35):
Also, the audio is still off.
Rob Lewis (Jan 06 2020 at 14:36):
Is the audio back on?
Alex J. Best (Jan 06 2020 at 14:37):
No
Floris van Doorn (Jan 06 2020 at 14:37):
no, it's muted
Rob Lewis (Jan 06 2020 at 14:37):
There are still complications with the video. We're working on it.
Floris van Doorn (Jan 06 2020 at 14:38):
now it's on
Wojciech Nawrocki (Jan 06 2020 at 14:39):
Can you hear anything? It's unmuted for me also but with no sound output
Floris van Doorn (Jan 06 2020 at 14:39):
Yes, I can hear it well
Alex J. Best (Jan 06 2020 at 14:40):
I can also hear
Wojciech Nawrocki (Jan 06 2020 at 14:40):
It works now, thanks!
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.
Rob Lewis (Jan 06 2020 at 14:48):
Kevin just asked a question from the third row. Was that audible on the stream?
Rob Lewis (Jan 06 2020 at 14:49):
It looks like the whole room has mics, but I'm not sure which are active.
Alex J. Best (Jan 06 2020 at 14:50):
Yes I could hear it fine
Kenny Lau (Jan 06 2020 at 14:59):
(where) can we access the slides?
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
Manuel Eberl (Jan 06 2020 at 16:05):
Here's mine: https://www21.in.tum.de/~eberlm/pdfs/fomm2020.pdf
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.
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.
Kenny Lau (Jan 06 2020 at 16:41):
mic is suddenly not working (10 sec ago)
Floris van Doorn (Jan 06 2020 at 16:41):
the audio just got muted
Kenny Lau (Jan 06 2020 at 16:41):
after Kevin Buzzard remarked that the d_r is the lcm from 1 to r
Kenny Lau (Jan 06 2020 at 16:42):
indeed the audio was muted
Kenny Lau (Jan 06 2020 at 16:42):
it's unmuted now
Floris van Doorn (Jan 06 2020 at 16:42):
fixed again
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?
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
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.
Rob Lewis (Jan 06 2020 at 16:53):
Slides for Sebastien's talk, coming up next: http://robertylewis.com/files/fomm_gouezel.pdf
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.
Rob Lewis (Jan 06 2020 at 19:38):
We tried to bump up the mic volume again. Has the stream quality improved at all?
Ulrik Buchholtz (Jan 06 2020 at 19:57):
I've put my slides on my webpage.
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")
Floris van Doorn (Jan 06 2020 at 21:33):
the meeting got canceled because the host started another meeting.
Jeremy Avigad (Jan 06 2020 at 21:46):
Sorry. We don't know what happened, but we got it fixed pretty quickly.
Floris van Doorn (Jan 07 2020 at 14:33):
I get the message "the host has another meeting in progress" again.
Kevin Buzzard (Jan 07 2020 at 14:38):
Rob is on the case
Rob Lewis (Jan 07 2020 at 14:40):
Rob is putting Bruno on the case.
Rob Lewis (Jan 07 2020 at 14:41):
And Bruno has put Jeremy on the case.
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.
Rob Lewis (Jan 07 2020 at 14:44):
https://cmu.zoom.us/j/332471944
Jeremy Avigad (Jan 07 2020 at 14:46):
I fixed the link on the web page now.
Floris van Doorn (Jan 07 2020 at 14:49):
Thanks!
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
Jeremy Avigad (Jan 07 2020 at 17:37):
They are now also on the website.
Jason Rute (Jan 07 2020 at 20:30):
Are the slides for this talk or Markus's talk going to be online?
Chris Hughes (Jan 07 2020 at 20:33):
@Reid Barton Are your slides available somewhere?
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).
Jeremy Avigad (Jan 07 2020 at 20:59):
(I was responding to Jason, not Chris!)
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?
Jeremy Avigad (Jan 08 2020 at 14:48):
Alas, it seems that he cannot make them public. (Google rules, I guess.)
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!
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.
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
Etienne Laurin (Jan 08 2020 at 16:37):
The current meeting id seems to be 896-922-652
Bruno Bentzen (Jan 08 2020 at 16:37):
The current meeting id seems to be 896-922-652
Yes, this is the correct id.
Jeremy Avigad (Jan 08 2020 at 16:40):
Thanks for catching that! The web site is fixed now.
Jeremy Avigad (Jan 08 2020 at 17:24):
Let me know if I should ask Gabriel to readjust the microphone to make it louder.
Rob Lewis (Jan 09 2020 at 16:50):
If anyone is streaming right now: how is the volume?
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?
Rob Lewis (Jan 09 2020 at 16:56):
It's streaming, not being recorded.
Cyril Cohen (Jan 09 2020 at 16:56):
It's streaming, not being recorded.
oh,... right
Etienne Laurin (Jan 09 2020 at 16:57):
The volume is very good.
Agnishom Chattopadhyay (Jan 09 2020 at 16:59):
It's streaming, not being recorded.
unless someone is recording the stream...
Rob Lewis (Jan 09 2020 at 17:01):
Please don't :slight_smile:
Johan Commelin (Jan 09 2020 at 17:31):
So Lean 4 is classified material?
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.
Johan Commelin (Jan 09 2020 at 17:32):
aah, ok
Johan Commelin (Jan 09 2020 at 17:33):
I'm looking forward to the youtube versions!
Luis Berlioz (Jan 10 2020 at 17:08):
Hi, please find attached the slides for my presentation this afternoon.
TextMiningArXiv.pdf
Jeremy Avigad (Jan 10 2020 at 17:10):
I'll put them on the web page during the lunch break.
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
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
Johan Commelin (Jan 13 2020 at 11:44):
Is there an ETA for the youtube videos?
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.
Johan Commelin (Jan 15 2020 at 07:06):
Thanks! I can wait that long (-;
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.
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.
Rob Lewis (Jan 16 2020 at 02:16):
Yes, I think every talk was captured by at least one of you.
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: Dec 20 2023 at 11:08 UTC