Pierre-Marie Pédrot (Nov 16 2020 at 18:07): 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?
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
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
Pierre-Marie Pédrot (Nov 16 2020 at 18:12):What do you call a random demo exactly?
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?
Pierre-Marie Pédrot (Nov 16 2020 at 18:16):Good idea!
Enrico Tassi (Nov 16 2020 at 18:16):you have 20 minutes for a teaser, a demo of you new cool feature
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
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
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 :)
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)
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.
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.
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.
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.
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?
Pierre-Marie Pédrot (Nov 30 2020 at 09:57):Hopefully as soon as possible, that is, we should schedule it ~ todayish.
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.
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
Pierre-Marie Pédrot (Nov 30 2020 at 09:58):We can dedicate a slot late in the day for that.
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?
Matthieu Sozeau (Nov 30 2020 at 10:00):I can do a MetaCoq demo / summary talk (around 20 mins) tomorrow morning.
Pierre-Marie Pédrot (Nov 30 2020 at 10:01):@Matthieu Sozeau what about the poor Americans?
Matthieu Sozeau (Nov 30 2020 at 10:01):Oh right. I can do it in the afternoon too
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
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
Pierre-Marie Pédrot (Nov 30 2020 at 10:21):in the Program section
Pierre-Marie Pédrot (Nov 30 2020 at 10:21):please register your talk there
Pierre-Marie Pédrot (Nov 30 2020 at 10:22):@Karl Palmskog @Emilio Jesús Gallego Arias @Clément Pit-Claudel @Matthieu Sozeau
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.
Pierre-Marie Pédrot (Nov 30 2020 at 10:42):Go ahead!
Michael Soegtrop (Nov 30 2020 at 11:23):@Pierre-Marie Pédrot : what time would you suggest?
Karl Palmskog (Nov 30 2020 at 11:24):just fill up chronologically on Wednesday
Théo Zimmermann (Nov 30 2020 at 12:38):@Michael Soegtrop Jim was interested to attend so the later the better.
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.
Karl Palmskog (Nov 30 2020 at 14:02):@Michael Soegtrop https://github.com/coq/coq/wiki/Coq-Users-and-Developers-Workshop-2020#program
Pierre-Marie Pédrot (Nov 30 2020 at 14:25):REMINDER: Next Plenary Session in 5 (FIVE) minutes
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.
Gaëtan Gilbert (Nov 30 2020 at 15:16):there may be a "join audio" button at the bottom below emilio
Pierre-Marie Pédrot (Nov 30 2020 at 15:16):You're indeed showed as "not listening"
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.
Pierre-Marie Pédrot (Nov 30 2020 at 15:31):Jason's defense will be available at https://mit.zoom.us/j/96295220004
Pierre-Marie Pédrot (Nov 30 2020 at 15:33):The password is the name of your favourite tactic language, in lowercase
Pierre-Marie Pédrot (Nov 30 2020 at 15:34):For a good notion of favourite.
Cyril Cohen (Nov 30 2020 at 15:36):coq-elpi ?
Pierre-Marie Pédrot (Nov 30 2020 at 15:37):Well tried, but no.
Enrico Tassi (Nov 30 2020 at 15:42):which version?
Pierre-Marie Pédrot (Nov 30 2020 at 15:43):4-letter pasword, no version number
Gaëtan Gilbert (Nov 30 2020 at 15:45):caml?
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.
Emilio Jesús Gallego Arias (Nov 30 2020 at 15:54):make?
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:
Pierre-Marie Pédrot (Nov 30 2020 at 16:37):Works for me©
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?
Matthieu Sozeau (Dec 01 2020 at 13:10):@Karl Palmskog sure
Théo Zimmermann (Dec 01 2020 at 14:34):@all Plenary starting now!
Cody Roux (Dec 01 2020 at 14:39):Can't find the link!
Matthieu Sozeau (Dec 01 2020 at 14:39):See Topic
Cody Roux (Dec 01 2020 at 14:39):Oh I see.
Jim Fehrle (Dec 01 2020 at 14:51):How do I join the call?
Jim Fehrle (Dec 01 2020 at 14:53):How do I join the call?
Enrico Tassi (Dec 01 2020 at 14:53):https://bbb-front.math.univ-paris-diderot.fr/recherche/the-sev-dee-jmp
Enrico Tassi (Dec 01 2020 at 14:53):(It's in the stream title)
Jim Fehrle (Dec 01 2020 at 14:54):Which room?
Cody Roux (Dec 01 2020 at 14:56):The "main" room, AKA none of the breakout rooms.
Enrico Tassi (Dec 01 2020 at 14:57):if it asks you to join a breakout room, hit "cancel"
Jim Fehrle (Dec 01 2020 at 14:59):Somehow it started working after several tries. Strange.
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
Théo Zimmermann (Dec 01 2020 at 15:51):Thanks to Yves!
Matthieu Sozeau (Dec 01 2020 at 16:00):Cool !
Matthieu Sozeau (Dec 01 2020 at 16:00):demo effect included :)
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.
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.
Matthieu Sozeau (Dec 01 2020 at 16:13):@Lasse I'd like to see a talk on tactician.
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
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.
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).
Gaëtan Gilbert (Dec 01 2020 at 20:50):nothing on friday?
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)
Clément Pit-Claudel (Dec 01 2020 at 20:55):Oh, Friday is even better for me if it's available
Pierre-Marie Pédrot (Dec 01 2020 at 20:58):There is no official talk on Friday, so be my / our guest.
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)
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?
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 )
Pierre-Marie Pédrot (Dec 01 2020 at 21:00):And also "HALP We n33dz rele4se manag3rs for 8.14!1!l0l"
Enrico Tassi (Dec 01 2020 at 21:01):FTR, feedback on that PR is very welcome
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)
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.
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
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...
Lasse Blaauwbroek (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.
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
Théo Zimmermann (Dec 02 2020 at 14:12):Sure.
Karl Palmskog (Dec 02 2020 at 14:28):@Théo Zimmermann so, maybe you could ping everyone for the plenary as per usual?
Théo Zimmermann (Dec 02 2020 at 14:28):Right!
Théo Zimmermann (Dec 02 2020 at 14:29):@all The plenary session with Karl and Enrico's talks is about to start!
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?
Gaëtan Gilbert (Dec 02 2020 at 14:45):there is a button below the presentation to "join audio" or some such thing
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.
Guillaume Melquiond (Dec 02 2020 at 14:46):This is expected. You need to click on the "phone" icon to enable the audio.
Maxime Dénès (Dec 02 2020 at 14:46):The tooltip is "join audio", but the icon is mute...
Arthur Charguéraud (Dec 02 2020 at 14:46):ah ok, not intuitive, thanks. i didn't need to do that before...
Maxime Dénès (Dec 02 2020 at 14:46):Yeah. Gaetan unlocked me last time ;)
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.
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
Lasse Blaauwbroek (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?
Lasse Blaauwbroek (Dec 03 2020 at 10:38):@Théo Zimmermann Could you maybe take a look at my questions above?
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.
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...
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.
Théo Zimmermann (Dec 03 2020 at 14:13):Sure.
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.
Pierre-Marie Pédrot (Dec 03 2020 at 14:30):Plenary session about to start!
Théo Zimmermann (Dec 03 2020 at 14:30):@all : Plenary session about to start, with two talks, by Karl and Lasse.
Clément Pit-Claudel (Dec 04 2020 at 05:01):Done! Is 15:30 on Friday a good time?
Karl Palmskog (Dec 04 2020 at 05:23):yes, this is a good time for a plenary
Karl Palmskog (Dec 04 2020 at 05:24):@Clément Pit-Claudel please assure you have some time for questions :wink:
Pierre-Marie Pédrot (Dec 04 2020 at 14:29):Plenary Session About To Start!
Théo Zimmermann (Dec 04 2020 at 14:30):@all Clément Pit-Claudel's talk now!
Clément Pit-Claudel (Dec 04 2020 at 14:30):Which room should I join for that?
Pierre-Marie Pédrot (Dec 04 2020 at 14:30):the main one
Pierre-Marie Pédrot (Dec 04 2020 at 14:30):just exit
Last updated: Jun 11 2023 at 00:30 UTC