Is the workshop meant for just experienced coq users? Or can newbies join as well?
@Julin S The workshop is meant for everyone regardless of expertise level. If you are interested in how Coq works under the hood and want to tinker around, this workshop is for you.
Indeed, at least myself (and I'm sure other devs) will be very happy to spend time with people which is not familiar with Coq's implementation at all
Hi!
Is there some room for propositions of developments for the hackaton? I have a small one.
Hold on :-) precision: I am not proposing myself as a coq expert, but as an attendee. I am rusty, for the least.
propose away
Indeed @Pierre Courtieu plenty of room, see the wiki https://github.com/coq/coq/wiki/CoqWG-2022-02
we usually have a nice atmosphere were people jump in to help with questions. But nevertheless, it would be nice if experts could flag up somehow what their specialties are, and what they are willing to possibly help out with.
@Karl Palmskog feel free to update the wiki to reflect this, or to add yourself as an organizer and add informartion to the coq-club / discuss post
I'm not expert on much on much in Coq dev. I guess I can add some things like "using Dune for Coq plugins", and I know a bit about coqdoc and coq_makefile.
one might use codeowners stuff as a guide right?
done adding my suggestion. Thanks!
can you guys please put the main dates/time and the wiki link in the stream description? I don't have rights to do it...
Time is not yet decided, let me see why you don't have permission tho
that should be fixed
I can't do it either, @Théo Zimmermann would you mind when you have a second
Actually I'd suggest a name for the stream to be "Coq Winter Hackathon, Feb 15th-17th 2022"
Seems shorter and more catchy, wdyt folks?
fine by me in abstract, but then the whole "working group" stuff is inherited, right? So maybe you would clarify in its longer description that the Hackathon is indeed part of a series of Coq Working Groups
Sounds good thanks!
Feel free to improve the wiki, for Zulip we need an admin but I agree with you
ping @Théo Zimmermann can you please give me and Emilio admin privileges for this stream so we can edit stream description and so on.
There's no such concept, so all I can do is to make one of you an admin of the entire Zulip.
Note that I didn't see the previous ping because I was not subscribed to this stream. Normally when you try to ping someone who is not subscribed, Zulip should tell you.
that's strange, it says when I try to edit:
Save failed: Must be an organization or stream administrator
and also weird because I can edit stream descriptions for a bunch of other streams just fine...
Someone would have to look into the Zulip doc or bug tracking system to understand that, unfortunately I'm short on time today.
OK, then I think we will simply have to ask you or Cyril to change the stream description for us next week. It's not urgent right now I guess.
In any case, both Cyril and I are OK to have more (Zulip-wide) admins.
I think the timestamps with "h" suffix is a French or Spanish thing? As in: "09h"
yes sorry, it is both
9 hour
I personally don't like the am/pm thing, but it's kind of standard in English... should I change?
Sure please go ahead, I didn't realize
maybe keep the 24hours format?
I dunno
not sure at all
I changed now to am/pm, but we can do 15:00
or 16:30
etc., without h
, which I believe is some ISO standard
I guess this is a question for the Coq team, what is our official time format?
I think 24 hour time is better in every way here
Karl Palmskog said:
I guess this is a question for the Coq team, what is our official time format?
I'd bet that was never discussed and I'd vote for it to be never discussed XD
It is already confusing enough with time zones
yes, 24h format is fine
don't forget to say "16 hundred hours"...
OK, all in 24 hour without the h
now
maybe the japan time one should be 23:00-26:00
when's a good time for my ocamldebug demo?
Tuesday evening?
that's not very specific
schedule masters please pick a specific time
@Gaëtan Gilbert do we know who's interested? I'm gonna send the mail now to remind everyone to add their name, then depending on the timezone we schedule
not tomorrow for sure
I've scheduled Gaëtan for Wednesday at 15:00 by the way.
What does "Morning (CET/Paris time)" mean in practice?
10:00
I will make it more clear on the wiki
Hi folks, and good morning/evening/afternoon; the BBB is open
I will be away due to doctor until unknown time
I have made some breakout rooms which you are welcome to use
Here is the link in case it was buried https://bbb.inria.fr/gal-afg-2va-fun
Related org-question: How often do these Hackathon/ workgroup sessions happen? Are they periodic (e.g. once every month)?
That's an open question!
we can check the wiki to see frequency in the past
but we want to organize different now I hypothesize
before we use to do coq working group
now IMHO it makes more sense to do more thematic ones
for example the first big summer one was in 2015
so it is an evolving process as the development of Coq becomes more based in the community
used to be about once a year physically in France. In my opinion, purely virtual hackathons should be replaced by hybrid or fully physical ones as soon as this is possible...
Right, it also makes sense to consider virtual components, distributed timezones, etc.
My question was motivated by the idea that maybe some periodic (esp. virtual/hybrid) sessions could be helpful for people trying to get involved
IMHO we should try to do physical meetings again but keep the virtual ones too because they have the potential to help newcomers who wouldn't have come to the physical meetings.
I would avoid hybrid though. Hybrid is really hard to do right.
I meant hybrid in the sense that: two people might be hacking on something together in the same room, while collaborating with someone remote at intervals
In this sense, we are always hybrid when we use GitHub.
Karl Palmskog said:
used to be about once a year physically in France. In my opinion, purely virtual hackathons should be replaced by hybrid or fully physical ones as soon as this is possible...
That was the big event, the working groups used to be every two months, at Paris, physically
or even a bit more often
the working groups were arguably semi-closed [to only Coq team]
Karl Palmskog said:
the working groups were arguably semi-closed [to only Coq team]
Depends on the years you refer to
They became more open as the development became more open, at least since I've been involved with Coq they were not closed as such
but indeed physical imposed many limitations
Hanneli question was about the working groups, so it is fair to talk about the working groups
summer event was for users and developers abroad
of course now we have a very different scope due to online
I was at the 2019 CUDW, and it could not really be described as being for users
most people were Coq devs, plugin devs, or researchers who used Coq
Maybe it could not, but users were welcome too.
There were a few users, but I guess already at 2019, there was little motivations for users to go to see coq devs
due to our nice online presence
2015 was very different but it is true we also did the workshop
moreover we have the workshop and coqpl that is another meeting point for users
the main payoff for me was talking to Coq devs about development stuff. Most users arguably do not need to talk to devs, but need general help from experienced users/researchers
Karl Palmskog said:
the main payoff for me was talking to Coq devs about development stuff. Most users arguably do not need to talk to devs, but need general help from experienced users/researchers
most users may not need to talk to coq devs, but certainly a very important set of advanced users have had and provided a lot of feedback to devs
so this case is still very very relevant, even more, essential!
In fact we are not doing very well in this sense
I don't think it's overly useful for core to talk directly to (inexperienced) end users
Karl Palmskog said:
I don't think it's overly useful for core to talk directly to (inexperienced) end users
I don't know, for me it has been very revealing and useful.
@Emilio Jesús Gallego Arias here
my view: would be best if inexperienced users/plugin devs met library devs, existing plugin devs, researchers - with core in the background to consult
Emilio Jesús Gallego Arias said:
Karl Palmskog said:
I don't think it's overly useful for core to talk directly to (inexperienced) end users
I don't know, for me it has been very revealing and useful.
In particular I got a lot of hints about why people find math-comp hard and what kind of documentation we need to write, from teaching it to mathematicians with 0 Coq experience
Karl Palmskog said:
my view: would be best if inexperienced users/plugin devs met library devs, existing plugin devs, researchers - with core in the background to consult
I think that was the idea for the CUDW from the start, but I may let other weight in (cc @Maxime Dénès )
maybe a bad analogy, but you don't really let new drivers talk to car developers on how they should improve their car handling
on the other hand, makes sense to let senior drivers of racecars consult with car developers on tuning
Indeed not sure the analogy is the best. Depends how you define "inexperience user" . Is a top level mathematician that has never done Coq "inexperienced". For me, the spirit of the working groups and the larger events is to bring everyone together, and moreover, to focus on the newcomers.
OK, I think our views diverge a lot here: Coq core consulting time is extremely valuable to me, and the people who can best use it are senior Coq users and plugin devs.
This doesn't rule out core participating in initiatives that bring improvements to newcomers. But for example, it would be better to have senior plugin devs teach plugin dev than core helping someone with Coq API basics.
Indeed a big part of my professional goals are to make proof assistants accesible and usable by everyone. But i do agree that the kind of organization you propose makes a lot of sense too
I don't thing they are incompatible
I would personally find it more valuable to suddenly have 5-10 more Coq-related projects with the visibility and impact of CompCert, than a large influx of new users, to be honest. Support to experienced Coq users at least has a chance of making new CompCerts happen, but many new users mean the existing community support volunteers might be overwhelmed, with no clear and immediate benefit.
So I think in some sense targeting "everyone" is partly in conflict with other desirable goals.
Maybe it is, but I'd find it surprising
I don't see why having a larger and better prepared user base wouldn't come too, once these users become more experienced, with new and exciting projects.
Sorry, it looks like my original question started a long discussion.
Based on what you said, it looks like there is no pre-established, periodic coding sessions that can accommodate beginners / users without exp in Coq development.
Maybe an idea for the future: having something like that could bring in more Coq users.
Thanks for all the clarifications!
Based on what you said, it looks like there is no pre-established, periodic coding sessions that can accommodate beginners / users without exp in Coq development.
Right, this role has been traditionally covered by summer schools and the CUDW, but few were complete beginners at CUDW.
Indeed, this was precisely the idea of CUDW. Depending on the sessions, it has had a larger or smaller audience. Some have been very successful.
Last updated: Jun 10 2023 at 23:01 UTC