Stream: Coq Hackathon and Working Group, Winter 2022

Topic: Organization questions


view this post on Zulip Julin S (Feb 01 2022 at 07:34):

Is the workshop meant for just experienced coq users? Or can newbies join as well?

view this post on Zulip Ali Caglayan (Feb 01 2022 at 09:23):

@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.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 01 2022 at 09:55):

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

view this post on Zulip Pierre Courtieu (Feb 01 2022 at 11:27):

Hi!
Is there some room for propositions of developments for the hackaton? I have a small one.

view this post on Zulip Pierre Courtieu (Feb 01 2022 at 11:30):

Hold on :-) precision: I am not proposing myself as a coq expert, but as an attendee. I am rusty, for the least.

view this post on Zulip Gaëtan Gilbert (Feb 01 2022 at 11:36):

propose away

view this post on Zulip Emilio Jesús Gallego Arias (Feb 01 2022 at 12:47):

Indeed @Pierre Courtieu plenty of room, see the wiki https://github.com/coq/coq/wiki/CoqWG-2022-02

view this post on Zulip Karl Palmskog (Feb 01 2022 at 12:49):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 01 2022 at 12:51):

@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

view this post on Zulip Karl Palmskog (Feb 01 2022 at 12:53):

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.

view this post on Zulip Karl Palmskog (Feb 01 2022 at 12:55):

one might use codeowners stuff as a guide right?

view this post on Zulip Pierre Courtieu (Feb 01 2022 at 12:56):

done adding my suggestion. Thanks!

view this post on Zulip Karl Palmskog (Feb 04 2022 at 13:30):

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...

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 13:41):

Time is not yet decided, let me see why you don't have permission tho

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 13:41):

that should be fixed

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 13:43):

I can't do it either, @Théo Zimmermann would you mind when you have a second

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 13:44):

Actually I'd suggest a name for the stream to be "Coq Winter Hackathon, Feb 15th-17th 2022"

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 13:44):

Seems shorter and more catchy, wdyt folks?

view this post on Zulip Karl Palmskog (Feb 04 2022 at 13:47):

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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 13:50):

Sounds good thanks!

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 13:50):

Feel free to improve the wiki, for Zulip we need an admin but I agree with you

view this post on Zulip Karl Palmskog (Feb 11 2022 at 11:17):

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.

view this post on Zulip Théo Zimmermann (Feb 11 2022 at 11:20):

There's no such concept, so all I can do is to make one of you an admin of the entire Zulip.

view this post on Zulip Théo Zimmermann (Feb 11 2022 at 11:21):

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.

view this post on Zulip Karl Palmskog (Feb 11 2022 at 11:22):

that's strange, it says when I try to edit:

Save failed: Must be an organization or stream administrator

view this post on Zulip Karl Palmskog (Feb 11 2022 at 11:22):

and also weird because I can edit stream descriptions for a bunch of other streams just fine...

view this post on Zulip Théo Zimmermann (Feb 11 2022 at 11:23):

Someone would have to look into the Zulip doc or bug tracking system to understand that, unfortunately I'm short on time today.

view this post on Zulip Karl Palmskog (Feb 11 2022 at 11:28):

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.

view this post on Zulip Théo Zimmermann (Feb 11 2022 at 12:19):

In any case, both Cyril and I are OK to have more (Zulip-wide) admins.

view this post on Zulip Karl Palmskog (Feb 11 2022 at 14:11):

I think the timestamps with "h" suffix is a French or Spanish thing? As in: "09h"

view this post on Zulip Emilio Jesús Gallego Arias (Feb 11 2022 at 14:11):

yes sorry, it is both

view this post on Zulip Emilio Jesús Gallego Arias (Feb 11 2022 at 14:11):

9 hour

view this post on Zulip Karl Palmskog (Feb 11 2022 at 14:12):

I personally don't like the am/pm thing, but it's kind of standard in English... should I change?

view this post on Zulip Emilio Jesús Gallego Arias (Feb 11 2022 at 14:13):

Sure please go ahead, I didn't realize

view this post on Zulip Emilio Jesús Gallego Arias (Feb 11 2022 at 14:13):

maybe keep the 24hours format?

view this post on Zulip Emilio Jesús Gallego Arias (Feb 11 2022 at 14:13):

I dunno

view this post on Zulip Emilio Jesús Gallego Arias (Feb 11 2022 at 14:14):

not sure at all

view this post on Zulip Karl Palmskog (Feb 11 2022 at 14:18):

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

view this post on Zulip Karl Palmskog (Feb 11 2022 at 14:19):

I guess this is a question for the Coq team, what is our official time format?

view this post on Zulip Ali Caglayan (Feb 11 2022 at 14:20):

I think 24 hour time is better in every way here

view this post on Zulip Emilio Jesús Gallego Arias (Feb 11 2022 at 14:21):

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

view this post on Zulip Ali Caglayan (Feb 11 2022 at 14:21):

It is already confusing enough with time zones

view this post on Zulip Emilio Jesús Gallego Arias (Feb 11 2022 at 14:21):

yes, 24h format is fine

view this post on Zulip Karl Palmskog (Feb 11 2022 at 14:22):

don't forget to say "16 hundred hours"...

view this post on Zulip Karl Palmskog (Feb 11 2022 at 14:23):

OK, all in 24 hour without the h now

view this post on Zulip Gaëtan Gilbert (Feb 11 2022 at 14:23):

maybe the japan time one should be 23:00-26:00

view this post on Zulip Gaëtan Gilbert (Feb 14 2022 at 16:14):

when's a good time for my ocamldebug demo?

view this post on Zulip Ali Caglayan (Feb 14 2022 at 16:16):

Tuesday evening?

view this post on Zulip Gaëtan Gilbert (Feb 14 2022 at 18:14):

that's not very specific
schedule masters please pick a specific time

view this post on Zulip Emilio Jesús Gallego Arias (Feb 14 2022 at 18:42):

@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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 14 2022 at 18:42):

not tomorrow for sure

view this post on Zulip Ali Caglayan (Feb 14 2022 at 20:36):

I've scheduled Gaëtan for Wednesday at 15:00 by the way.

view this post on Zulip Ana de Almeida Borges (Feb 14 2022 at 21:02):

What does "Morning (CET/Paris time)" mean in practice?

view this post on Zulip Ali Caglayan (Feb 14 2022 at 21:14):

10:00

view this post on Zulip Ali Caglayan (Feb 14 2022 at 21:14):

I will make it more clear on the wiki

view this post on Zulip Emilio Jesús Gallego Arias (Feb 17 2022 at 08:29):

Hi folks, and good morning/evening/afternoon; the BBB is open

view this post on Zulip Emilio Jesús Gallego Arias (Feb 17 2022 at 08:30):

I will be away due to doctor until unknown time

view this post on Zulip Ali Caglayan (Feb 17 2022 at 08:50):

I have made some breakout rooms which you are welcome to use

view this post on Zulip Ali Caglayan (Feb 17 2022 at 09:02):

Here is the link in case it was buried https://bbb.inria.fr/gal-afg-2va-fun

view this post on Zulip Hanneli Tavante (Mar 22 2022 at 18:19):

Related org-question: How often do these Hackathon/ workgroup sessions happen? Are they periodic (e.g. once every month)?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 22 2022 at 18:19):

That's an open question!

view this post on Zulip Emilio Jesús Gallego Arias (Mar 22 2022 at 18:20):

we can check the wiki to see frequency in the past

view this post on Zulip Emilio Jesús Gallego Arias (Mar 22 2022 at 18:20):

but we want to organize different now I hypothesize

view this post on Zulip Emilio Jesús Gallego Arias (Mar 22 2022 at 18:20):

before we use to do coq working group

view this post on Zulip Emilio Jesús Gallego Arias (Mar 22 2022 at 18:20):

now IMHO it makes more sense to do more thematic ones

view this post on Zulip Emilio Jesús Gallego Arias (Mar 22 2022 at 18:21):

for example the first big summer one was in 2015

view this post on Zulip Emilio Jesús Gallego Arias (Mar 22 2022 at 18:21):

so it is an evolving process as the development of Coq becomes more based in the community

view this post on Zulip Karl Palmskog (Mar 22 2022 at 18:23):

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...

view this post on Zulip Hanneli Tavante (Mar 22 2022 at 18:24):

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

view this post on Zulip Théo Zimmermann (Mar 22 2022 at 18:25):

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.

view this post on Zulip Théo Zimmermann (Mar 22 2022 at 18:26):

I would avoid hybrid though. Hybrid is really hard to do right.

view this post on Zulip Karl Palmskog (Mar 22 2022 at 18:26):

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

view this post on Zulip Théo Zimmermann (Mar 22 2022 at 18:27):

In this sense, we are always hybrid when we use GitHub.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 22 2022 at 18:29):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 22 2022 at 18:29):

or even a bit more often

view this post on Zulip Karl Palmskog (Mar 22 2022 at 18:31):

the working groups were arguably semi-closed [to only Coq team]

view this post on Zulip Emilio Jesús Gallego Arias (Mar 22 2022 at 18:31):

Karl Palmskog said:

the working groups were arguably semi-closed [to only Coq team]

Depends on the years you refer to

view this post on Zulip Emilio Jesús Gallego Arias (Mar 22 2022 at 18:32):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 22 2022 at 18:32):

but indeed physical imposed many limitations

view this post on Zulip Emilio Jesús Gallego Arias (Mar 22 2022 at 18:33):

Hanneli question was about the working groups, so it is fair to talk about the working groups

view this post on Zulip Emilio Jesús Gallego Arias (Mar 22 2022 at 18:33):

summer event was for users and developers abroad

view this post on Zulip Emilio Jesús Gallego Arias (Mar 22 2022 at 18:33):

of course now we have a very different scope due to online

view this post on Zulip Karl Palmskog (Mar 22 2022 at 18:33):

I was at the 2019 CUDW, and it could not really be described as being for users

view this post on Zulip Karl Palmskog (Mar 22 2022 at 18:34):

most people were Coq devs, plugin devs, or researchers who used Coq

view this post on Zulip Emilio Jesús Gallego Arias (Mar 22 2022 at 18:34):

Maybe it could not, but users were welcome too.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 22 2022 at 18:35):

There were a few users, but I guess already at 2019, there was little motivations for users to go to see coq devs

view this post on Zulip Emilio Jesús Gallego Arias (Mar 22 2022 at 18:35):

due to our nice online presence

view this post on Zulip Emilio Jesús Gallego Arias (Mar 22 2022 at 18:35):

2015 was very different but it is true we also did the workshop

view this post on Zulip Emilio Jesús Gallego Arias (Mar 22 2022 at 18:35):

moreover we have the workshop and coqpl that is another meeting point for users

view this post on Zulip Karl Palmskog (Mar 22 2022 at 18:36):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 22 2022 at 18:36):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 22 2022 at 18:37):

so this case is still very very relevant, even more, essential!

view this post on Zulip Emilio Jesús Gallego Arias (Mar 22 2022 at 18:37):

In fact we are not doing very well in this sense

view this post on Zulip Karl Palmskog (Mar 22 2022 at 18:37):

I don't think it's overly useful for core to talk directly to (inexperienced) end users

view this post on Zulip Emilio Jesús Gallego Arias (Mar 22 2022 at 18:39):

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.

view this post on Zulip Karl Palmskog (Mar 22 2022 at 18:44):

@Emilio Jesús Gallego Arias here

view this post on Zulip Karl Palmskog (Mar 22 2022 at 18:46):

my view: would be best if inexperienced users/plugin devs met library devs, existing plugin devs, researchers - with core in the background to consult

view this post on Zulip Emilio Jesús Gallego Arias (Mar 22 2022 at 18:46):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 22 2022 at 18:47):

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 )

view this post on Zulip Karl Palmskog (Mar 22 2022 at 18:48):

maybe a bad analogy, but you don't really let new drivers talk to car developers on how they should improve their car handling

view this post on Zulip Karl Palmskog (Mar 22 2022 at 18:50):

on the other hand, makes sense to let senior drivers of racecars consult with car developers on tuning

view this post on Zulip Emilio Jesús Gallego Arias (Mar 22 2022 at 18:51):

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.

view this post on Zulip Karl Palmskog (Mar 22 2022 at 18:59):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 22 2022 at 19:44):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 22 2022 at 19:44):

I don't thing they are incompatible

view this post on Zulip Karl Palmskog (Mar 22 2022 at 19:51):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 22 2022 at 23:22):

Maybe it is, but I'd find it surprising

view this post on Zulip Emilio Jesús Gallego Arias (Mar 22 2022 at 23:23):

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.

view this post on Zulip Hanneli Tavante (Mar 22 2022 at 23:45):

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.

view this post on Zulip Hanneli Tavante (Mar 22 2022 at 23:48):

Thanks for all the clarifications!

view this post on Zulip Karl Palmskog (Mar 23 2022 at 08:04):

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.

view this post on Zulip Théo Zimmermann (Mar 23 2022 at 08:22):

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: Jan 29 2023 at 14:02 UTC