It's been almost four years since there was an in-person Coq Users and Developers Workshop. Is there any planned for 2023?
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
@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)?
A quite essential question is if this could be done online or not
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).
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.
Yes, I also understand the interest of meeting "foundational" library developers.
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
agreed
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.
I was just thinking it should maybe be the Coq Ecosystem Clinic :)
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.
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.
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.
It should definitely still be about development of Coq for a part. Indeed it can't be both that and a school about libraries.
But point taken, it should be relatively free form for a good part
This kind of makes it impossible to run online these kind of gatherings, IMHO.
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.
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.
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).
@Enrico Tassi Ok, so I guess we should organize one by June!
TYPES 2023 : https://types2023.webs.upv.es/ 12-17 june
GDR GPL: 5-9 june 2023
Last updated: Nov 29 2023 at 04:01 UTC