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
is this a new name for CUDW?
No, it is a new event, CUDW will hopefully happen in the summer
You could think of it as a more coding-focused CUDW
the idea is very similar tho
so the audience of the hackathon is mostly core devs then? Or maintainers and community as well?
obvious followup question: is it going to be fully physical, fully remote, or hybrid?
The idea is hybrid
Let me setup the wiki page of course :embarrassed:
sounds good, you can already write the FAQ...
@Karl Palmskog preliminary page setup, see edited msg
don't forget the second h in hackathon
Thanks we spaniards always have problems with this
by the way anyone interested in helping with the organization: just add yourself to the list with the "organizer" moniker"
I will take care of the local stuff, but the rest can be done by AoW
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
but I guess the "Coq Internals" seminar could also broaden things a bit by talking about how to contribute to Coq code side?
Indeed, that's implicit in the "Hackathon" tag, maybe you can edit the page a bit?
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"
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?
But we have CoqPL already just a few weeks before
yeah, I think it suffices to broaden by saying plugin devs are welcome, since they will likely benefit from hearing about Coq internals
Yes, I will also broaden the audience to include people that has never hacked Coq
but they would like to learn more
cc: @Ali Caglayan by the way
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
do you want me to move it now?
@Ali Caglayan maybe we should do a small TODO list to organize?
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
Should we do maybe a poll?
Yeah let's do a poll for the date, an announce it on discuss etc....
The Feb date works for me
I can start a todo list tomorrow to scope out what we want
Great @Ali Caglayan , we use the wiki page right?
I'll add a few items myself
I think that would be best
sounds good, do you think we should open a poll for the date tho?
with 3 options I guess, 14th 21st and 28th of Feb
at least we should poll the core people IMHO
by core I mean the regular contributors
Sounds good
:thumbs_up:
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
Should a link be added to https://github.com/coq/coq/wiki/CoqImplementorsWorkshop?
Emilio said he doesn't consider this a CUDW above
A "more coding-focused CUDW" looks very much like a CUDW to me.
I think the Users part is largely absent, i.e., the focus is almost wholly on Coq devs + plugin devs
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.
But OK, maybe the difference here is that the focus will be less on onboarding and more on meeting with current devs?
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.
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.)
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 :-)
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.
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
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...
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.
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.
indeed, "PR design" or "PR architecture" is a black art in large projects. And getting it wrong upfront can be frustrating to all involved
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.
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
Karl Palmskog said:
OK, let me give one example I had in mind: introducing
Body
as a synonym to theProof
keyword.
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.
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)
Ok folks, as discussed yesterday here is the draft of the announcement mail that I'd like to send to coq-club / discourse
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
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)
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).
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?
LGTM
I will sign instead of Emilio and Ali "the coq team"
as many people have contributed to this discussion
still the wiki list us as the people to get in touch with for questions
"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!
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
Anywhere you like. But I can also just make you a moderator and you'll have these permissions if you want.
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
@Emilio Jesús Gallego Arias Should we make a Zulip stream?
Yes!
That's a great idea if you wanna add it to the reminder already
@Emilio Jesús Gallego Arias done.
Last updated: Dec 07 2023 at 17:01 UTC