Stream: CUDW 2020

Topic: Plenary sessions


view this post on Zulip Pierre-Marie Pédrot (Nov 16 2020 at 18:07):

In the previous CUDWs we used to have some core devs presenting the nitty-gritty details of the Coq source code, and similar other short technical talks about the implementation. Anybody up for the task this year?

view this post on Zulip Pierre-Marie Pédrot (Nov 16 2020 at 18:09):

I don't have a way to ping core devs, so let's do that haphazardly from the top of my head @Enrico Tassi @Emilio Jesús Gallego Arias @Maxime Dénès @Hugo Herbelin @Matthieu Sozeau @Gaëtan Gilbert @Théo Zimmermann and whomever I forgot about

view this post on Zulip Enrico Tassi (Nov 16 2020 at 18:11):

Mah, do we want it? if all topics were about ML plugins, why not... but if it is not the case, maybe better random demos

view this post on Zulip Pierre-Marie Pédrot (Nov 16 2020 at 18:12):

What do you call a random demo exactly?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 16 2020 at 18:13):

I've been planning to do a youtube streaming with my dev setup for quite a while, so indeed that could work?

view this post on Zulip Pierre-Marie Pédrot (Nov 16 2020 at 18:16):

Good idea!

view this post on Zulip Enrico Tassi (Nov 16 2020 at 18:16):

you have 20 minutes for a teaser, a demo of you new cool feature

view this post on Zulip Enrico Tassi (Nov 16 2020 at 18:18):

IIRC last CUDW in Nice some non-dev gave talks. I liked that, but they were full talk, while I propose smaller slots

view this post on Zulip Karl Palmskog (Nov 17 2020 at 10:19):

assuming there is enough interest, I could present an overview 15-20 min of "Coq batch incremental checking" (amalgamation of 4-5 papers in ASE, ISSTA, TACAS., from last 3 years), and ideas for better support in Coq going forward

view this post on Zulip Matthieu Sozeau (Nov 17 2020 at 10:23):

Karl Palmskog said:

assuming there is enough interest, I could present an overview 15-20 min of "Coq batch incremental checking" (amalgamation of 4-5 papers in ASE, ISSTA, TACAS., from last 3 years), and ideas for better support in Coq going forward

That interrests me :)

view this post on Zulip Karl Palmskog (Nov 17 2020 at 13:22):

maybe @Emilio Jesús Gallego Arias could give a summary/demo of his current work on document/proof management in Coq itself, which is partly related but much more focused on interactive incremental checking (in my book)

view this post on Zulip Pierre-Marie Pédrot (Nov 18 2020 at 22:37):

I forgot to mention that @Jason Gross is defending his PhD on the 30th at 17:00 CET. It's right after the official schedule of the CUDW, be it could be worth advertising as a highly related event.

view this post on Zulip Jason Gross (Nov 18 2020 at 23:25):

Pierre-Marie Pédrot said:

I forgot to mention that Jason Gross is defending his PhD on the 30th at 17:00 CET. It's right after the official schedule of the CUDW, be it could be worth advertising as a highly related event.

Indeed! Anyone who wants to come needs to get the zoom room and password from me or someone I've given it to (the MIT admins are concerned about zoombombing), but I'd be happy to have it advertised (and to hand out the link to anyone interested, or to delegate that to someone else). I can also offer a blurb if you want one.

view this post on Zulip Karl Palmskog (Nov 23 2020 at 01:31):

also perhaps plenary-worthy: I can give a 10 minute demo of our lemma naming suggestion tool, which can be used in VSCode thanks to a new extension on top of VSCoq: https://github.com/EngineeringSoftware/roosterize

Currently, we only have a MathComp dataset for training. To extend to other styles/projects, we need collaborators to help us curate enough high-quality code for the deep learning process to work well.

view this post on Zulip Théo Zimmermann (Nov 25 2020 at 13:42):

@Clément Pit-Claudel I would like to hear your talk about using Alectryon for Coq's refman.

view this post on Zulip Assia Mahboubi (Nov 30 2020 at 09:56):

@Pierre-Marie Pédrot @Théo Zimmermann how/when will will know the time slots and speakers for the plenary sessions of the days to come?

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 09:57):

Hopefully as soon as possible, that is, we should schedule it ~ todayish.

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 09:58):

@Clément Pit-Claudel is likely to present his work on Alectryon, but due to his timezone we have to wait a bit to hear from him.

view this post on Zulip Karl Palmskog (Nov 30 2020 at 09:58):

I can do my incremental-Coq-CI talk ideally on Wednesday (15 min), then perhaps a quick name suggestion tool demo (10 min) on Thursday

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 09:58):

We can dedicate a slot late in the day for that.

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 09:59):

What about 15:30-16:30, so that the last half an hour can be use to summarize the day?

view this post on Zulip Matthieu Sozeau (Nov 30 2020 at 10:00):

I can do a MetaCoq demo / summary talk (around 20 mins) tomorrow morning.

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 10:01):

@Matthieu Sozeau what about the poor Americans?

view this post on Zulip Matthieu Sozeau (Nov 30 2020 at 10:01):

Oh right. I can do it in the afternoon too

view this post on Zulip Karl Palmskog (Nov 30 2020 at 10:01):

Pierre-Marie Pédrot said:

What about 15:30-16:30, so that the last half an hour can be use to summarize the day?

those slots work fine for me, Wed or Thu

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 10:21):

I have added info on the wiki page https://github.com/coq/coq/wiki/Coq-Users-and-Developers-Workshop-2020

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 10:21):

in the Program section

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 10:21):

please register your talk there

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 10:22):

@Karl Palmskog @Emilio Jesús Gallego Arias @Clément Pit-Claudel @Matthieu Sozeau

view this post on Zulip Michael Soegtrop (Nov 30 2020 at 10:37):

As mentioned on the Wiki I would be happy to present and discuss the Coq platform project in a plenary session - preferably tomorrow so that we can incorporate feedback we get - today is a bit tight cause of the Ph.D. defense of Jason.

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 10:42):

Go ahead!

view this post on Zulip Michael Soegtrop (Nov 30 2020 at 11:23):

@Pierre-Marie Pédrot : what time would you suggest?

view this post on Zulip Karl Palmskog (Nov 30 2020 at 11:24):

just fill up chronologically on Wednesday

view this post on Zulip Théo Zimmermann (Nov 30 2020 at 12:38):

@Michael Soegtrop Jim was interested to attend so the later the better.

view this post on Zulip Michael Soegtrop (Nov 30 2020 at 14:02):

@Karl Palmskog is there a list with times somewhere - I thought it should be on the Wiki but couldn't find it there.

view this post on Zulip Karl Palmskog (Nov 30 2020 at 14:02):

@Michael Soegtrop https://github.com/coq/coq/wiki/Coq-Users-and-Developers-Workshop-2020#program

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 14:25):

REMINDER: Next Plenary Session in 5 (FIVE) minutes

view this post on Zulip Maxime Dénès (Nov 30 2020 at 15:12):

@Pierre-Marie Pédrot how to join? When I reach the main room I see Emilio but hear nothing.

view this post on Zulip Gaëtan Gilbert (Nov 30 2020 at 15:16):

there may be a "join audio" button at the bottom below emilio

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 15:16):

You're indeed showed as "not listening"

view this post on Zulip Maxime Dénès (Nov 30 2020 at 15:18):

Thanks @Gaëtan Gilbert I hadn't imagined that the crossed mic icon meant to activate speakers.

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 15:31):

Jason's defense will be available at https://mit.zoom.us/j/96295220004

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 15:33):

The password is the name of your favourite tactic language, in lowercase

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 15:34):

For a good notion of favourite.

view this post on Zulip Cyril Cohen (Nov 30 2020 at 15:36):

coq-elpi ?

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 15:37):

Well tried, but no.

view this post on Zulip Enrico Tassi (Nov 30 2020 at 15:42):

which version?

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 15:43):

4-letter pasword, no version number

view this post on Zulip Gaëtan Gilbert (Nov 30 2020 at 15:45):

caml?

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 15:46):

Pardon my French, but y a des coups de pied au cul qui se perdent.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 30 2020 at 15:54):

make?

view this post on Zulip Gaëtan Gilbert (Nov 30 2020 at 16:35):

zoom mutes itself every few minutes so I have to rejoin
what a piece of :poop:

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 16:37):

Works for me©

view this post on Zulip Karl Palmskog (Dec 01 2020 at 12:53):

@Matthieu Sozeau any chance of a few words today about the status of CertiCoq during the plenary?

view this post on Zulip Matthieu Sozeau (Dec 01 2020 at 13:10):

@Karl Palmskog sure

view this post on Zulip Théo Zimmermann (Dec 01 2020 at 14:34):

@all Plenary starting now!

view this post on Zulip Cody Roux (Dec 01 2020 at 14:39):

Can't find the link!

view this post on Zulip Matthieu Sozeau (Dec 01 2020 at 14:39):

See Topic

view this post on Zulip Cody Roux (Dec 01 2020 at 14:39):

Oh I see.

view this post on Zulip Jim Fehrle (Dec 01 2020 at 14:51):

How do I join the call?

view this post on Zulip Jim Fehrle (Dec 01 2020 at 14:53):

How do I join the call?

view this post on Zulip Enrico Tassi (Dec 01 2020 at 14:53):

https://bbb-front.math.univ-paris-diderot.fr/recherche/the-sev-dee-jmp

view this post on Zulip Enrico Tassi (Dec 01 2020 at 14:53):

(It's in the stream title)

view this post on Zulip Jim Fehrle (Dec 01 2020 at 14:54):

Which room?

view this post on Zulip Cody Roux (Dec 01 2020 at 14:56):

The "main" room, AKA none of the breakout rooms.

view this post on Zulip Enrico Tassi (Dec 01 2020 at 14:57):

if it asks you to join a breakout room, hit "cancel"

view this post on Zulip Jim Fehrle (Dec 01 2020 at 14:59):

Somehow it started working after several tries. Strange.

view this post on Zulip Théo Zimmermann (Dec 01 2020 at 15:51):

Matthieu's talk available at http://www-sop.inria.fr/members/Yves.Bertot/videos/Matthieu-metacoq.mp4

view this post on Zulip Théo Zimmermann (Dec 01 2020 at 15:51):

Thanks to Yves!

view this post on Zulip Matthieu Sozeau (Dec 01 2020 at 16:00):

Cool !

view this post on Zulip Matthieu Sozeau (Dec 01 2020 at 16:00):

demo effect included :)

view this post on Zulip Enrico Tassi (Dec 01 2020 at 16:11):

@Pierre-Marie Pédrot you were asking for more talk... I can pitch Coq-Elpi for 20' on Thursday if you think it fits the schedule.

view this post on Zulip Pierre-Marie Pédrot (Dec 01 2020 at 16:12):

Let's hear from @Clément Pit-Claudel who first previously mentioned a talk, but a priori there is no problem.

view this post on Zulip Matthieu Sozeau (Dec 01 2020 at 16:13):

@Lasse I'd like to see a talk on tactician.

view this post on Zulip Yves Bertot (Dec 01 2020 at 18:28):

Michael's talk is available at http://www-sop.inria.fr/members/Yves.Bertot/videos/Michael-Coq-Platform.mp4

view this post on Zulip Clément Pit-Claudel (Dec 01 2020 at 20:37):

Sorry folks, I'm drowning in faculty applications; I'm still happy to do a 15 minutes demo about Alectryon and the refman, maybe on Thursday? I have stuff almost all day Wednesday.

view this post on Zulip Enrico Tassi (Dec 01 2020 at 20:40):

OK then. I'll give @Lasse precedence on Wednesday (tomorrow) if he likes. I'll pick any slot left (if none, no problem).

view this post on Zulip Gaëtan Gilbert (Dec 01 2020 at 20:50):

nothing on friday?

view this post on Zulip Karl Palmskog (Dec 01 2020 at 20:52):

for Friday, I vote for Enrico & Maxime giving us a quick tour of what's to come in 8.13 (highlights, gotchas)

view this post on Zulip Clément Pit-Claudel (Dec 01 2020 at 20:55):

Oh, Friday is even better for me if it's available

view this post on Zulip Pierre-Marie Pédrot (Dec 01 2020 at 20:58):

There is no official talk on Friday, so be my / our guest.

view this post on Zulip Enrico Tassi (Dec 01 2020 at 20:59):

@Karl Palmskog this is the best I could tell you about 8.13 : https://github.com/coq/coq/pull/13527 (not sure it is worth a talk)

view this post on Zulip Pierre-Marie Pédrot (Dec 01 2020 at 21:00):

Maybe @Maxime Dénès can give the evergreen "release plan" for the 8.14 then?

view this post on Zulip Enrico Tassi (Dec 01 2020 at 21:00):

(unroll the diff on doc/sphinx/changes.rst, or look at the rendering https://coq.gitlab.io/-/coq/-/jobs/883787225/artifacts/_install_ci/share/doc/coq/sphinx/html/changes.html#version-8-13 )

view this post on Zulip Pierre-Marie Pédrot (Dec 01 2020 at 21:00):

And also "HALP We n33dz rele4se manag3rs for 8.14!1!l0l"

view this post on Zulip Enrico Tassi (Dec 01 2020 at 21:01):

FTR, feedback on that PR is very welcome

view this post on Zulip Enrico Tassi (Dec 01 2020 at 21:05):

To me the gotcha for 8.3 (where early feedback can really help) is this one:

Changed: Redeclaring a notation also reactivates its printing rule; in particular a second Import of the same module reactivates the printing rules declared in this module. In theory, this leads to changes in behavior for printing. However, this is mitigated in general by the adoption in #12986 of a priority given to notations which match a larger part of the term to print (#12984, fixes #7443 and #10824, by Hugo Herbelin).
Changed: Use of notations for printing now gives preference to notations which match a larger part of the term to abbreviate (#12986, by Hugo Herbelin).

(Since out resting infrastructure is weak on this kind of things, that is how goals are printed)

view this post on Zulip Enrico Tassi (Dec 01 2020 at 21:14):

These new rules came of discussion and testing with power users of the notation system, but it's hard to know in advance if it causes problems to the rest of the user base.

view this post on Zulip Pierre-Marie Pédrot (Dec 02 2020 at 09:18):

@Clément Pit-Claudel please register your talk on the wiki page https://github.com/coq/coq/wiki/Coq-Users-and-Developers-Workshop-2020#program

view this post on Zulip Pierre-Marie Pédrot (Dec 02 2020 at 09:21):

Officially the time slots are any connected subcomponent of the range 15:30-16:30 UTC+1, but @Yves Bertot mentioned he would not be available starting from 16:00 and would prefer a bit sooner if possible (~15:00). It's a bit early for you so...

view this post on Zulip Lasse (Dec 02 2020 at 10:01):

I've added my talk between 15:40 and 15:55 tomorrow. I can also give a longer talk, but I understand that quick demo-style talks are preferred.

view this post on Zulip Karl Palmskog (Dec 02 2020 at 14:12):

@Théo Zimmermann can you help me with trying out the plenary system? I finished my slides so I could potentially upload them somewhere

view this post on Zulip Théo Zimmermann (Dec 02 2020 at 14:12):

Sure.

view this post on Zulip Karl Palmskog (Dec 02 2020 at 14:28):

@Théo Zimmermann so, maybe you could ping everyone for the plenary as per usual?

view this post on Zulip Théo Zimmermann (Dec 02 2020 at 14:28):

Right!

view this post on Zulip Théo Zimmermann (Dec 02 2020 at 14:29):

@all The plenary session with Karl and Enrico's talks is about to start!

view this post on Zulip Arthur Charguéraud (Dec 02 2020 at 14:44):

I have an issue, when I log into the bbb using any of the links that I know of, it redirects me immediately to the pannel showing the choices for breakout rooms, without asking me for mic/listenonly. If I close that panel, then I don't have sound. If I enter a breakout room, however, it works. I get that on all my navigators. Any idea why this may happen?

view this post on Zulip Gaëtan Gilbert (Dec 02 2020 at 14:45):

there is a button below the presentation to "join audio" or some such thing

view this post on Zulip Maxime Dénès (Dec 02 2020 at 14:45):

Dunno, but sometimes clicking on the "mute" icon show me the menu for mic/listen only.

view this post on Zulip Guillaume Melquiond (Dec 02 2020 at 14:46):

This is expected. You need to click on the "phone" icon to enable the audio.

view this post on Zulip Maxime Dénès (Dec 02 2020 at 14:46):

The tooltip is "join audio", but the icon is mute...

view this post on Zulip Arthur Charguéraud (Dec 02 2020 at 14:46):

ah ok, not intuitive, thanks. i didn't need to do that before...

view this post on Zulip Maxime Dénès (Dec 02 2020 at 14:46):

Yeah. Gaetan unlocked me last time ;)

view this post on Zulip Maxime Dénès (Dec 02 2020 at 14:47):

Having to click on a crossed mic to turn your speakers on is not a very impressive UX approach.

view this post on Zulip Yves Bertot (Dec 02 2020 at 16:08):

Videos of the talks are available here http://www-sop.inria.fr/members/Yves.Bertot/videos/Karl-Incremental-Proofs.mp4
http://www-sop.inria.fr/members/Yves.Bertot/videos/Enrico-Coq-Elpi.mp4

view this post on Zulip Lasse (Dec 03 2020 at 09:12):

Is there any wisdom to be given to prevent video stuttering during a talk? Also, could somebody with merge rights on the Opam repo look at my PR so that people can try my software after the presentation?

view this post on Zulip Lasse (Dec 03 2020 at 10:38):

@Théo Zimmermann Could you maybe take a look at my questions above?

view this post on Zulip Théo Zimmermann (Dec 03 2020 at 10:42):

cc @Karl Palmskog or @Matthieu Sozeau or @Enrico Tassi for the PR to the opam repo.

view this post on Zulip Théo Zimmermann (Dec 03 2020 at 10:43):

I don't know what to say about avoiding video stuttering except that: if you use slides, you will have less bandwidth problems if you upload your slides to BBB instead of sharing your screen; if you need to share your screen, e.g. for a demo, then shutting off your webcam will improve the bandwidth and thus reduce video stuttering...

view this post on Zulip Karl Palmskog (Dec 03 2020 at 14:12):

@Théo Zimmermann could you help me set up some slides again for BBB plenary? I decided to do 3 slides as intro and then switch to screen sharing.

view this post on Zulip Théo Zimmermann (Dec 03 2020 at 14:13):

Sure.

view this post on Zulip Théo Zimmermann (Dec 03 2020 at 14:13):

I won't enable my mic though because I'm currently following a PhD defense at the same time.

view this post on Zulip Pierre-Marie Pédrot (Dec 03 2020 at 14:30):

Plenary session about to start!

view this post on Zulip Théo Zimmermann (Dec 03 2020 at 14:30):

@all : Plenary session about to start, with two talks, by Karl and Lasse.

view this post on Zulip Clément Pit-Claudel (Dec 04 2020 at 05:01):

Done! Is 15:30 on Friday a good time?

view this post on Zulip Karl Palmskog (Dec 04 2020 at 05:23):

yes, this is a good time for a plenary

view this post on Zulip Karl Palmskog (Dec 04 2020 at 05:24):

@Clément Pit-Claudel please assure you have some time for questions :wink:

view this post on Zulip Pierre-Marie Pédrot (Dec 04 2020 at 14:29):

Plenary Session About To Start!

view this post on Zulip Théo Zimmermann (Dec 04 2020 at 14:30):

@all Clément Pit-Claudel's talk now!

view this post on Zulip Clément Pit-Claudel (Dec 04 2020 at 14:30):

Which room should I join for that?

view this post on Zulip Pierre-Marie Pédrot (Dec 04 2020 at 14:30):

the main one

view this post on Zulip Pierre-Marie Pédrot (Dec 04 2020 at 14:30):

just exit


Last updated: Oct 16 2021 at 07:02 UTC