Karl Palmskog (Dec 10 2022 at 12:11): Karl Palmskog (Dec 10 2022 at 12:11):It's been almost four years since there was an in-person Coq Users and Developers Workshop. Is there any planned for 2023?
Karl Palmskog (Dec 12 2022 at 11:10):as memento, our efforts on consolidation of Coq code into "the right library" (which may be Stdlib), is one obvious work item for a tentative CUDW: https://github.com/coq-community/manifesto/issues/143
Matthieu Sozeau (Jan 19 2023 at 16:43):@Yves Bertot brought up this discussion with me and I'd like to get some feedback on this subject. Indeed it would be good to have one. I'm not sure which format / content it should have however. Should it be about developing plugins and the like (as previous CUDWs) or more about contributing to a consolidated stdlib, and/or learning about tools like Ltac2, elpi, equations... or even slightly general purpose libraries like math-comp, iris, ... (this might be tricky to do right, I guess one needs a few days of dedicated lectures to get on with any of them)?
Matthieu Sozeau (Jan 19 2023 at 16:44):A quite essential question is if this could be done online or not
Karl Palmskog (Jan 19 2023 at 16:47):the last CUDW had some lecture stuff, but it wasn't really the point of the whole thing, I think the value for most people (me included) was (1) in-person access to Coq core devs to work on plugins/bugs/libraries, (2) meeting in-person other people who did the same, and in particular library experts (MathComp).
Matthieu Sozeau (Jan 19 2023 at 16:47):Personally, I would prefer an in-person event that's split between a developer/plugin developer side but generalizing "plugin" to encompass not only ML but also the other metalanguages.
Matthieu Sozeau (Jan 19 2023 at 16:47):Yes, I also understand the interest of meeting "foundational" library developers.
Karl Palmskog (Jan 19 2023 at 16:50):in a recent documentation discussion, I think there was some agreement that "plugin" nowadays is ambiguous and needs to be more qualified to ML plugin when that is what is meant, since a lot can be done with Elpi/MetaCoq/SerAPI/LSP
Matthieu Sozeau (Jan 19 2023 at 16:50):agreed
Karl Palmskog (Jan 19 2023 at 16:52):we also have some general "ecosystem questions", that are indirectly related to Coq. To give a recent example, CUDW might be a forum to figure out why Linux Snap for Coq Platform and VsCoq are having interaction issues, since one would have both the Snappers and VsCoq devs there.
Matthieu Sozeau (Jan 19 2023 at 16:53):I was just thinking it should maybe be the Coq Ecosystem Clinic :)
Michael Soegtrop (Jan 19 2023 at 17:08):I think the topics should not be too much carved in stone - it should also be an opportunity for Coq users to meet the Coq developers and learn from them - not necessarily regarding plugins / proof automation. There is also much to learn about how to write proofs nicely.
Karl Palmskog (Jan 19 2023 at 17:10):from what I remember about CUDW 2019, we didn't have many official topics for the whole event, but people had very specific personal goals (perhaps nearly carved in the proverbial stone). I think that still worked well.
Karl Palmskog (Jan 19 2023 at 17:13):the tradeoff is that if you just want to learn about Coq in general, a lot of the clusters of people are going to be working on and talking about super-specific stuff. But at least to me, that's the "D" side of CUDW, as opposed to "learning Coq [or Coq library]" schools.
Matthieu Sozeau (Jan 19 2023 at 17:17):It should definitely still be about development of Coq for a part. Indeed it can't be both that and a school about libraries.
Matthieu Sozeau (Jan 19 2023 at 17:18):But point taken, it should be relatively free form for a good part
Matthieu Sozeau (Jan 19 2023 at 17:18):This kind of makes it impossible to run online these kind of gatherings, IMHO.
Ana de Almeida Borges (Jan 19 2023 at 17:44):I have never been to an in-person such gathering, but FWIW I found the last two online users+developers workshops (or whatever they were called) extremely useful for learning how to implement the things I wanted to implement at the time.
Enrico Tassi (Jan 19 2023 at 19:45):I think the format of CUDW in the past worked well, but it does not prevent the organization of Coding Sprints events, which in general have fewer participants and a fixed topic (and with a restricted set of core devs). I think that sprints are a very good mean to make progress in open communities.
Said that, if there is enough interest for a CUDW I can help organizing it in Sophia-Antipolis as we did in the past.
Théo Zimmermann (Jan 19 2023 at 20:29):Ideally, if we have enough energy, we should keep doing both in-person and online CUDWs (not at the same time), because meeting face to face is invaluable but online CUDWs can reach out to people who wouldn't have had the opportunity to travel. That being said, I think we have missed in-person interactions, so it's a good objective to focus on an in-person CUDW first (keeping in mind that online stuff is also a nice thing to keep).
Matthieu Sozeau (Jan 20 2023 at 07:43):@Enrico Tassi Ok, so I guess we should organize one by June!
Matthieu Sozeau (Jan 25 2023 at 15:12):TYPES 2023 : https://types2023.webs.upv.es/ 12-17 june
Théo Zimmermann (Jan 25 2023 at 15:12):GDR GPL: 5-9 june 2023
Last updated: May 28 2023 at 13:30 UTC