Emilio Jesús Gallego Arias (Nov 19 2021 at 13:24): Emilio Jesús Gallego Arias (Nov 19 2021 at 13:24):Hi all, this is the thread for the organization of the Coq hackaton and Working Group in (hopefully) Feb. 2022 ; ITP deadline is Feb 8th, so it seems January is out of the question [given all other workshops]
Wiki page https://github.com/coq/coq/wiki/CoqWG-2022-02
Karl Palmskog (Nov 19 2021 at 13:38):is this a new name for CUDW?
Emilio Jesús Gallego Arias (Nov 19 2021 at 13:46):No, it is a new event, CUDW will hopefully happen in the summer
Emilio Jesús Gallego Arias (Nov 19 2021 at 13:46):You could think of it as a more coding-focused CUDW
Emilio Jesús Gallego Arias (Nov 19 2021 at 13:46):the idea is very similar tho
Karl Palmskog (Nov 19 2021 at 13:50):so the audience of the hackathon is mostly core devs then? Or maintainers and community as well?
Karl Palmskog (Nov 19 2021 at 14:11):obvious followup question: is it going to be fully physical, fully remote, or hybrid?
Emilio Jesús Gallego Arias (Nov 19 2021 at 14:15):The idea is hybrid
Emilio Jesús Gallego Arias (Nov 19 2021 at 14:15):Let me setup the wiki page of course :embarrassed:
Karl Palmskog (Nov 19 2021 at 14:19):sounds good, you can already write the FAQ...
Emilio Jesús Gallego Arias (Nov 19 2021 at 15:45):@Karl Palmskog preliminary page setup, see edited msg
Karl Palmskog (Nov 19 2021 at 15:46):don't forget the second h in hackathon
Emilio Jesús Gallego Arias (Nov 19 2021 at 15:47):Thanks we spaniards always have problems with this
Emilio Jesús Gallego Arias (Nov 19 2021 at 15:47):by the way anyone interested in helping with the organization: just add yourself to the list with the "organizer" moniker"
Emilio Jesús Gallego Arias (Nov 19 2021 at 15:47):I will take care of the local stuff, but the rest can be done by AoW
Karl Palmskog (Nov 19 2021 at 15:50):it looks like the audience is mainly Coq devs (core and maintainers), and focus is on code rather than documentation, maybe you want to flag this up explicitly
Karl Palmskog (Nov 19 2021 at 15:51):but I guess the "Coq Internals" seminar could also broaden things a bit by talking about how to contribute to Coq code side?
Emilio Jesús Gallego Arias (Nov 19 2021 at 15:51):Indeed, that's implicit in the "Hackathon" tag, maybe you can edit the page a bit?
Emilio Jesús Gallego Arias (Nov 19 2021 at 15:52):Karl Palmskog said:
but I guess the "Coq Internals" seminar could also broaden things a bit by talking about how to contribute to Coq code side?
I think that's the idea, maybe I should have a better name for it, it will be more a "guide to hack Coq"
Emilio Jesús Gallego Arias (Nov 19 2021 at 15:52):But yes, the idea of the meeting is for people interested in hacking Coq itself, maybe it would be a good idea to do an user meeting?
Emilio Jesús Gallego Arias (Nov 19 2021 at 15:53):But we have CoqPL already just a few weeks before
Karl Palmskog (Nov 19 2021 at 15:54):yeah, I think it suffices to broaden by saying plugin devs are welcome, since they will likely benefit from hearing about Coq internals
Emilio Jesús Gallego Arias (Nov 19 2021 at 15:54):Yes, I will also broaden the audience to include people that has never hacked Coq
Emilio Jesús Gallego Arias (Nov 19 2021 at 15:55):but they would like to learn more
Emilio Jesús Gallego Arias (Nov 19 2021 at 15:55):cc: @Ali Caglayan by the way
Emilio Jesús Gallego Arias (Dec 16 2021 at 19:40):Ok folks, so maybe we should move this thread to Coq Users at some point, the idea as discussed is to try the week of 14-18th of Feb 2022
Karl Palmskog (Dec 16 2021 at 19:40):do you want me to move it now?
Emilio Jesús Gallego Arias (Dec 16 2021 at 19:40):@Ali Caglayan maybe we should do a small TODO list to organize?
Emilio Jesús Gallego Arias (Dec 16 2021 at 19:41):Karl Palmskog said:
do you want me to move it now?
Now that I think of it maybe we should just open a new one? I dunno, let's see what Ali says
Emilio Jesús Gallego Arias (Dec 16 2021 at 19:41):Should we do maybe a poll?
Emilio Jesús Gallego Arias (Dec 16 2021 at 19:42):Yeah let's do a poll for the date, an announce it on discuss etc....
Ali Caglayan (Dec 16 2021 at 19:43):The Feb date works for me
Ali Caglayan (Dec 16 2021 at 19:44):I can start a todo list tomorrow to scope out what we want
Emilio Jesús Gallego Arias (Dec 16 2021 at 19:44):Great @Ali Caglayan , we use the wiki page right?
Emilio Jesús Gallego Arias (Dec 16 2021 at 19:44):I'll add a few items myself
Ali Caglayan (Dec 16 2021 at 19:44):I think that would be best
Emilio Jesús Gallego Arias (Dec 16 2021 at 19:45):sounds good, do you think we should open a poll for the date tho?
Emilio Jesús Gallego Arias (Dec 16 2021 at 19:45):with 3 options I guess, 14th 21st and 28th of Feb
Emilio Jesús Gallego Arias (Dec 16 2021 at 19:45):at least we should poll the core people IMHO
Emilio Jesús Gallego Arias (Dec 16 2021 at 19:45):by core I mean the regular contributors
Ali Caglayan (Dec 16 2021 at 19:45):Sounds good
Emilio Jesús Gallego Arias (Dec 16 2021 at 19:45)::thumbs_up:
Emilio Jesús Gallego Arias (Dec 16 2021 at 19:46):Ok, I suggest we keep two threads for now, this one in the dev stream more for internal discussion, and we open a new one on the users channel for discussion about the event proper
Théo Zimmermann (Dec 16 2021 at 20:57):Should a link be added to https://github.com/coq/coq/wiki/CoqImplementorsWorkshop?
Karl Palmskog (Dec 17 2021 at 08:40):Emilio said he doesn't consider this a CUDW above
Théo Zimmermann (Dec 17 2021 at 10:22):A "more coding-focused CUDW" looks very much like a CUDW to me.
Karl Palmskog (Dec 17 2021 at 10:23):I think the Users part is largely absent, i.e., the focus is almost wholly on Coq devs + plugin devs
Théo Zimmermann (Dec 17 2021 at 10:38):What CUDW have always been about is as a place for users to become developers. Recall that the name of CUDW changed several times: the first one was called "Coq coding sprint", the next three ones were called "Coq Implementors Workshop" (hence the wiki page name). Only the last two ones were named CUDW. And I wonder if it wasn't under the impulse of Emilio that this last renaming happened.
Théo Zimmermann (Dec 17 2021 at 10:38):But OK, maybe the difference here is that the focus will be less on onboarding and more on meeting with current devs?
Ali Caglayan (Dec 17 2021 at 10:48):Our original intent with Emilio was to gather everybody up and spend some time organising and squashing bugs. I don't think we really had a workshop style thing in mind.
Karl Palmskog (Dec 17 2021 at 12:37):in my view, one basic element of CUDW is that some Coq devs have to dedicate a lot of their time to advising other people, but per Ali the dev attention here may go mostly to fixing long-standing bugs (and listening to presentations, etc.)
Théo Zimmermann (Dec 17 2021 at 12:41):OK, I see the difference, thanks! But then, I wonder if the "Coq Internals Seminar" and "Diversity session" are actually relevant for this event. But well, do as you wish folks :-)
Karl Palmskog (Dec 17 2021 at 12:42):I think the Coq internals seminar is a good fit since as a plugin dev, I struggle with that a lot. This is probably more efficient than one-on-one tutoring.
Karl Palmskog (Dec 17 2021 at 12:45):one thing that would be nice is if devs could say that they will devote time to guide and merge Coq PRs with horizon of a few days during the hackathon. For example, I have some ideas for improving tools, but it's not feasible if it's going to take several weeks of discussion and refactoring and so on in a PR to get it merged.
Here, one could agree up front on an approximate PR time horizon
Théo Zimmermann (Dec 17 2021 at 13:11):That could make sense, but it really depends on how finished the PR will end up being during the hackathon. Note that the usual time for a PR to get merged is generally pretty reasonable. But the bigger a PR gets, the longer it can take...
Karl Palmskog (Dec 17 2021 at 20:53):OK, let me give one example I had in mind: introducing Body as a synonym to the Proof keyword.
Ideally one would agree up front that this would be acceptable with the right people to even begin work on grammar, coqdoc, documentation, etc. But the whole thing could likely be done during the hackathon.
Also good to get "impossible" PR ideas (either for technical or other reasons) shot down early.
Théo Zimmermann (Dec 19 2021 at 13:36):Good example! Yes, we can agree in advance that we want this. And the good thing about it is that not every related changes need to be implemented in the same PR and merged at the same time.
Karl Palmskog (Dec 19 2021 at 13:52):indeed, "PR design" or "PR architecture" is a black art in large projects. And getting it wrong upfront can be frustrating to all involved
Théo Zimmermann (Dec 19 2021 at 15:07):That's why our contributing guide tries to demystify the process as much as possible and be as clear as possible on the expectations to have and how to behave when they are not met. It also contains advice on the size of PR:
You are always welcome to open a PR for a change of any size. However, you should be aware that the larger the change, the higher the chances it will take very long to review, and possibly never get merged.
So it is recommended that before spending a lot of time coding, you seek feedback from maintainers to see if your change would be supported, and if they have recommendations about its implementation. You can do this informally by opening an issue, or more formally by producing a design document as a Coq Enhancement Proposal.
Another recommendation is that you do not put several unrelated changes in the same PR (even if you produced them together). In particular, make sure you split bug fixes into separate PRs when this is possible. More generally, smaller-sized PRs, or PRs changing fewer components, are more likely to be reviewed and merged promptly.
This observation on larger PRs taking longer to review is a general one across projects that has often been reported in the SE literature BTW.
Karl Palmskog (Dec 19 2021 at 15:10):there is a difference between "large PR due to lots of stuff" and "large PR due to small change with lots of unintended/unexpected consequences", so the general/generic advice can only go so far
Hugo Herbelin (Dec 20 2021 at 09:49):Karl Palmskog said:
OK, let me give one example I had in mind: introducing
Bodyas a synonym to theProofkeyword.
For the history, Body existed in early versions of Coq, with syntax Body term, in parallel with Proof term. It disappeared between versions 5.6 (1995) and 5.10 (1996) at the time a cosmetic noop Proof. was introduced. I agree it would be natural to have it available.
Karl Palmskog (Dec 20 2021 at 09:52):good to know. The main motivation is that users nowadays do not necessarily consider the body of constant defined using Definition a "proof" (i.e., they do not necessarily buy into Curry-Howard, or care about whether something is a proof, regardless of whether it's defined by tactics)
Emilio Jesús Gallego Arias (Jan 13 2022 at 16:44):Ok folks, as discussed yesterday here is the draft of the announcement mail that I'd like to send to coq-club / discourse
Emilio Jesús Gallego Arias (Jan 13 2022 at 16:58):Dear all,
we are happy to announce a virtual Coq Hackaton and Working Group in
Feb 15th-17th 2022; we were hoping to make this event a hybrid one,
but due to the current circumstances it will be online-only.
The event is targeted at people that is interested in Coq itself, and
would like to learn more about how Coq works and possibly contribute
to it. We hope that the event will be accessible and fun for people
with all levels of expertise.
The format and program of the event is open, we hope that there will
be 1 or 2 talks / tutorials per day, with the rest of the time people
assembling in working teams.
Some preliminary activities are already written down in the wiki,
please feel free to both _propose_ and _request_ a topic; yes, you can
request a talk or hacking session and we will try to find a person
interested in driving it.
See https://github.com/coq/coq/wiki/CoqWG-2022-02 for more information
and registration instructions.
Emilio and Ali
cc @Ali Caglayan
Pierre Roux (Jan 13 2022 at 17:35):Looks great! (I personally understand "people that is interested" as considering "people" as objects and would rewrite "people that is [...] would like" as "people interested in Coq itself and wanting" but I may be wrong, native English speakers here would certainly know better)
Pierre-Marie Pédrot (Jan 13 2022 at 17:38):Not a native speaker but I've never seen that form. Given the author, I suspect a calque from la gente which is indeed singular (but whose use can be funnily plural).
Karl Palmskog (Jan 13 2022 at 17:44):Here is a pass:
Dear all,
We are happy to announce a virtual Coq Hackathon and Working Group on
Feb 15th-17th 2022. We were hoping to make this event a hybrid one,
but due to the current circumstances it will be online only.
The event is targeted at people who are interested in the implementation
of Coq, and would like to learn more about how Coq works and possibly
contribute to its development. We hope that the event will be accessible
and fun for people at all levels of expertise.
The exact format and program of the event is currently open. We hope that there will
be 1-2 talks or tutorials per day, with people self-organizing into working groups
at other times.
Some preliminary activities are already written down in the wiki.
Please feel free to both _propose_ and _request_ topics. Yes, you can
request a talk or hacking session and we will try to find a person
interested in driving it.
See https://github.com/coq/coq/wiki/CoqWG-2022-02 for more information
and registration instructions.
Thanks @Karl Palmskog ! @Ali Caglayan any comment?
Ali Caglayan (Jan 14 2022 at 15:15):LGTM
Emilio Jesús Gallego Arias (Jan 14 2022 at 15:33):I will sign instead of Emilio and Ali "the coq team"
Emilio Jesús Gallego Arias (Jan 14 2022 at 15:34):as many people have contributed to this discussion
Emilio Jesús Gallego Arias (Jan 14 2022 at 15:34):still the wiki list us as the people to get in touch with for questions
Emilio Jesús Gallego Arias (Jan 31 2022 at 10:36):"all" hi coq devs and contributors, please don't forget to add your name and topics to https://github.com/coq/coq/wiki/CoqWG-2022-02 , thanks!
Emilio Jesús Gallego Arias (Jan 31 2022 at 10:36):Umm, "you don't have permissions to use all in this stream" @Théo Zimmermann the permissions on Zulip have been a constant source of pain, what's the right place to discuss it
Théo Zimmermann (Jan 31 2022 at 11:28):Anywhere you like. But I can also just make you a moderator and you'll have these permissions if you want.
Emilio Jesús Gallego Arias (Jan 31 2022 at 12:07):I put it in the call, thanks; if you wanna make a moderator that's fine; or else maybe you can just do the @all yourself
Ali Caglayan (Jan 31 2022 at 12:29):@Emilio Jesús Gallego Arias Should we make a Zulip stream?
Emilio Jesús Gallego Arias (Jan 31 2022 at 12:44):Yes!
Emilio Jesús Gallego Arias (Jan 31 2022 at 12:44):That's a great idea if you wanna add it to the reminder already
Théo Zimmermann (Jan 31 2022 at 13:11):@Emilio Jesús Gallego Arias done.
Last updated: Dec 07 2023 at 17:01 UTC