Julin S (Feb 01 2022 at 07:34): Julin S (Feb 01 2022 at 07:34):Is the workshop meant for just experienced coq users? Or can newbies join as well?
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.
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
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.
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.
Gaëtan Gilbert (Feb 01 2022 at 11:36):propose away
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
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.
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
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.
Karl Palmskog (Feb 01 2022 at 12:55):one might use codeowners stuff as a guide right?
Pierre Courtieu (Feb 01 2022 at 12:56):done adding my suggestion. Thanks!
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...
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
Emilio Jesús Gallego Arias (Feb 04 2022 at 13:41):that should be fixed
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
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"
Emilio Jesús Gallego Arias (Feb 04 2022 at 13:44):Seems shorter and more catchy, wdyt folks?
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
Emilio Jesús Gallego Arias (Feb 04 2022 at 13:50):Sounds good thanks!
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
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.
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.
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.
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
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...
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.
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.
Théo Zimmermann (Feb 11 2022 at 12:19):In any case, both Cyril and I are OK to have more (Zulip-wide) admins.
Karl Palmskog (Feb 11 2022 at 14:11):I think the timestamps with "h" suffix is a French or Spanish thing? As in: "09h"
Emilio Jesús Gallego Arias (Feb 11 2022 at 14:11):yes sorry, it is both
Emilio Jesús Gallego Arias (Feb 11 2022 at 14:11):9 hour
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?
Emilio Jesús Gallego Arias (Feb 11 2022 at 14:13):Sure please go ahead, I didn't realize
Emilio Jesús Gallego Arias (Feb 11 2022 at 14:13):maybe keep the 24hours format?
Emilio Jesús Gallego Arias (Feb 11 2022 at 14:13):I dunno
Emilio Jesús Gallego Arias (Feb 11 2022 at 14:14):not sure at all
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
Karl Palmskog (Feb 11 2022 at 14:19):I guess this is a question for the Coq team, what is our official time format?
Ali Caglayan (Feb 11 2022 at 14:20):I think 24 hour time is better in every way here
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
Ali Caglayan (Feb 11 2022 at 14:21):It is already confusing enough with time zones
Emilio Jesús Gallego Arias (Feb 11 2022 at 14:21):yes, 24h format is fine
Karl Palmskog (Feb 11 2022 at 14:22):don't forget to say "16 hundred hours"...
Karl Palmskog (Feb 11 2022 at 14:23):OK, all in 24 hour without the h now
Gaëtan Gilbert (Feb 11 2022 at 14:23):maybe the japan time one should be 23:00-26:00
Gaëtan Gilbert (Feb 14 2022 at 16:14):when's a good time for my ocamldebug demo?
Ali Caglayan (Feb 14 2022 at 16:16):Tuesday evening?
Gaëtan Gilbert (Feb 14 2022 at 18:14):that's not very specific
schedule masters please pick a specific time
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
Emilio Jesús Gallego Arias (Feb 14 2022 at 18:42):not tomorrow for sure
Ali Caglayan (Feb 14 2022 at 20:36):I've scheduled Gaëtan for Wednesday at 15:00 by the way.
Ana de Almeida Borges (Feb 14 2022 at 21:02):What does "Morning (CET/Paris time)" mean in practice?
Ali Caglayan (Feb 14 2022 at 21:14):10:00
Ali Caglayan (Feb 14 2022 at 21:14):I will make it more clear on the wiki
Emilio Jesús Gallego Arias (Feb 17 2022 at 08:29):Hi folks, and good morning/evening/afternoon; the BBB is open
Emilio Jesús Gallego Arias (Feb 17 2022 at 08:30):I will be away due to doctor until unknown time
Ali Caglayan (Feb 17 2022 at 08:50):I have made some breakout rooms which you are welcome to use
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
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)?
Emilio Jesús Gallego Arias (Mar 22 2022 at 18:19):That's an open question!
Emilio Jesús Gallego Arias (Mar 22 2022 at 18:20):we can check the wiki to see frequency in the past
Emilio Jesús Gallego Arias (Mar 22 2022 at 18:20):but we want to organize different now I hypothesize
Emilio Jesús Gallego Arias (Mar 22 2022 at 18:20):before we use to do coq working group
Emilio Jesús Gallego Arias (Mar 22 2022 at 18:20):now IMHO it makes more sense to do more thematic ones
Emilio Jesús Gallego Arias (Mar 22 2022 at 18:21):for example the first big summer one was in 2015
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
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...
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
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.
Théo Zimmermann (Mar 22 2022 at 18:26):I would avoid hybrid though. Hybrid is really hard to do right.
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
Théo Zimmermann (Mar 22 2022 at 18:27):In this sense, we are always hybrid when we use GitHub.
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
Emilio Jesús Gallego Arias (Mar 22 2022 at 18:29):or even a bit more often
Karl Palmskog (Mar 22 2022 at 18:31):the working groups were arguably semi-closed [to only Coq team]
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
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
Emilio Jesús Gallego Arias (Mar 22 2022 at 18:32):but indeed physical imposed many limitations
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
Emilio Jesús Gallego Arias (Mar 22 2022 at 18:33):summer event was for users and developers abroad
Emilio Jesús Gallego Arias (Mar 22 2022 at 18:33):of course now we have a very different scope due to online
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
Karl Palmskog (Mar 22 2022 at 18:34):most people were Coq devs, plugin devs, or researchers who used Coq
Emilio Jesús Gallego Arias (Mar 22 2022 at 18:34):Maybe it could not, but users were welcome too.
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
Emilio Jesús Gallego Arias (Mar 22 2022 at 18:35):due to our nice online presence
Emilio Jesús Gallego Arias (Mar 22 2022 at 18:35):2015 was very different but it is true we also did the workshop
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
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
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
Emilio Jesús Gallego Arias (Mar 22 2022 at 18:37):so this case is still very very relevant, even more, essential!
Emilio Jesús Gallego Arias (Mar 22 2022 at 18:37):In fact we are not doing very well in this sense
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
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.
Karl Palmskog (Mar 22 2022 at 18:44):@Emilio Jesús Gallego Arias here
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
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
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 )
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
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
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.
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.
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
Emilio Jesús Gallego Arias (Mar 22 2022 at 19:44):I don't thing they are incompatible
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.
Emilio Jesús Gallego Arias (Mar 22 2022 at 23:22):Maybe it is, but I'd find it surprising
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.
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.
Hanneli Tavante (Mar 22 2022 at 23:48):Thanks for all the clarifications!
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.
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: Dec 07 2023 at 14:02 UTC