Enrico Tassi (May 13 2020 at 14:01): Enrico Tassi (May 13 2020 at 14:01):I'm getting: En raison d'une forte demande, le service demandé est actuellement indisponible, merci d'essayer ultérieurement. Si le problème persiste, merci de contacter le support via notre portail https://assistance.renater.fr
Emilio Jesús Gallego Arias (May 13 2020 at 14:01):Yes, the server is down :S
Théo Zimmermann (May 13 2020 at 14:01):I get the same. I suggest using BBB instead.
Pierre-Marie Pédrot (May 13 2020 at 14:01):Great :/
Emilio Jesús Gallego Arias (May 13 2020 at 14:01):Should we move to visio.inria?
Théo Zimmermann (May 13 2020 at 14:02):I'll create a room.
Théo Zimmermann (May 13 2020 at 14:02):(visio.inria is discouraged right now for non-confidential meetings)
Enrico Tassi (May 13 2020 at 14:02):waiting for the link
Théo Zimmermann (May 13 2020 at 14:02):https://bbb2.math.univ-paris-diderot.fr/b/the-ume-p6v
Enrico Tassi (May 13 2020 at 14:03):should I put this link on the wiki?
Enrico Tassi (May 13 2020 at 14:03):you are blazing fast
Théo Zimmermann (May 13 2020 at 14:03):I did it already
Théo Zimmermann (May 13 2020 at 14:04):Indeed, I'm not respecting the wish of the IRIF IT staff by doing this but I'll delete the room after the meeting to avoid any trouble.
Janno (May 13 2020 at 14:09):Hm, I am not getting any sound output. I suppose it hasn't been total silence for the last 5 minutes, has it? I guess it's best we postpone the topic I added to another time
Pierre-Marie Pédrot (May 13 2020 at 14:10):We're talking.
Théo Zimmermann (May 13 2020 at 14:10):In principle, you should have sound testing when you join
Janno (May 13 2020 at 14:11):Yes, I decided to skip that after several unsuccessful tests. It never managed to detect an output device (the "test speakers" button worked, however). Not blaming BBB for this (not yet, anyway).
Théo Zimmermann (May 13 2020 at 14:12):You can try to rejoin in headphone only...
Gaëtan Gilbert (May 13 2020 at 14:12):Isn't the test about the mic?
Théo Zimmermann (May 13 2020 at 14:13):Yeah but since you're supposed to have echo you can can also hear sound.
Janno (May 13 2020 at 14:14):Listen only also doesn't work. The browser is using the right device and everything, BBB just isn't sending it any sound. Anyway, I don't want to waste anybody's time with this!
Janno (May 13 2020 at 14:23):Chromium to the rescue!
Pierre-Marie Pédrot (May 20 2020 at 13:56):Is the link is supposed to be posted here?
Enrico Tassi (May 20 2020 at 13:57):I hope so
Pierre-Marie Pédrot (May 20 2020 at 13:57):Or are we reusing the same room as last time?
Enrico Tassi (May 20 2020 at 13:57):Last time it did not work and we moved to BBB no?
Enrico Tassi (May 20 2020 at 13:58):@Théo Zimmermann can we use BBB this time as well?
Théo Zimmermann (May 20 2020 at 13:58):Yes, let me create the room.
Théo Zimmermann (May 20 2020 at 13:59):https://bbb2.math.univ-paris-diderot.fr/b/the-mt4-7q4
Théo Zimmermann (May 21 2020 at 20:29):The recording of Emilio's presentation at the last Coq Call is now available at the above link.
Emilio Jesús Gallego Arias (May 21 2020 at 22:17):I hope it is not like super terrible, I was an impromptu thing; I will push a few notes to the wiki once the WE is over, I've better answered some questions and added a few more comments in these notes; I'll ping here when they are ready.
Théo Zimmermann (May 22 2020 at 07:16):We can remove the recording whenever you want. In any case, if nobody saves it like the WG, the recording will be gone over the summer.
Emilio Jesús Gallego Arias (May 22 2020 at 10:49):OK for me if someone was to save, just saying that was not a proper "talk" but a quite improvised discussion :)
Hugo Herbelin (May 27 2020 at 13:40):No call today, right?
Théo Zimmermann (May 27 2020 at 13:42):Indeed, no topics, no call.
Maxime Dénès (Jun 03 2020 at 13:58):@Théo Zimmermann do we have a link for today's call?
Théo Zimmermann (Jun 03 2020 at 13:58):We can reuse the same as last time: https://bbb2.math.univ-paris-diderot.fr/b/the-mt4-7q4
Maxime Dénès (Jun 10 2020 at 11:40):No Coq call today?
Matthieu Sozeau (Jun 10 2020 at 12:49):Indeed, there were no topics added.
Hugo Herbelin (Jun 10 2020 at 13:55):@maximedenes had a topic though...
Théo Zimmermann (Jun 10 2020 at 14:20):Maxime had a topic or you did? The Coq Call page was not created. If people have topics to discuss they should create the page, otherwise how do we know?
Hugo Herbelin (Jun 10 2020 at 14:40):We know from here. But I'm ok to not discuss about it if there is a satisfaction with the current status of #12429. (My primary concern is that #12429 does not stall and that everyone is happy with it.)
Théo Zimmermann (Jun 10 2020 at 15:32):Ah well, in "I suggest" and "let's do that", there's clearly a lack of action from both sides to update the schedule for the next call. I suggest that, in order to avoid further delaying the discussion, you put it now on the schedule of next week's call.
Hugo Herbelin (Jun 10 2020 at 15:44):you put it now on the schedule of next week's call.
Ok, @Maxime Dénès, would you mind doing it the way you want it to be?
Maxime Dénès (Jun 10 2020 at 16:02):FTR, it is usually the PR author who adds the patch to be discussed as a topic on the agenda, since he/she's expected to lead the discussion.
Maxime Dénès (Jun 10 2020 at 16:03):I can add an item if you like, but it should be the way you want.
Maxime Dénès (Jun 10 2020 at 16:04):I'm reading the last message in the PR.
Maxime Dénès (Jun 10 2020 at 16:17):Ok, after rereading, I tried to post a summary of my position. @Hugo Herbelin if more discussion is needed, please add a topic for the next call.
Hugo Herbelin (Jun 10 2020 at 16:29):@maximedenes: To be honest, I'm lost on what to do. Personally, I feel that all has been said (regarding the PR) and I don't see what more I could say. But, of course, I'm ready to lead a discussion if there is an explicit need to. In any case, I'd really prefer that you do decide if you think that more discussion is needed and if yes that you take the responsability of scheduling the discussion!
Théo Zimmermann (Jun 10 2020 at 16:39):@Hugo Herbelin If you keep asking other people to do tasks that you want to happen, you're not going to be happy, because it's never going to happen the way you'd like. Why do you insist on Maxime being the one to schedule and lead the discussion? He told you already what the right fix should be in his opinion. Now, if your view differ, there must be a discussion indeed, but there is no reason why you should depend on him to schedule it...
Hugo Herbelin (Jun 10 2020 at 16:53):@Théo Zimmermann: I don't know to resolve the question. If @Maxime Dénès wants another fix, he can propose one. I explained in my last comment that I tried first to do as he suggested (i.e. to always output the inlined constants) and it dit not work as nicely as expected. So, I moved to a more conservative approach which is to strictly fix the bug a minima.
Why do you insist on Maxime being the one to schedule and lead the discussion?
I'm not really willing to spend more time than needed on this PR and I feel that all what is reasonable to say has been said. If @maximedenes wants to take over and propose another fix (which outputs inlined constants in addition to the inlining properly speaking), that's perfectly fine to me. I already spent time on that. It did not work out of the nose and I'm moreover not strictly convinced that it is really worth, so I don't know what I can do more as of now.
Hugo Herbelin (Jun 10 2020 at 16:58):I see that @Jason Gross and @Maxime Dénès are continuing discussing. That'll be good if something good comes out of the discussion, but, as far I'm concerned, I'm unfortunately missing time in the short term and I have to prioritarize. As a result, I cannot afford monitoring this PR longer, and I'd be happy to hand over!
Théo Zimmermann (Jun 10 2020 at 16:59):What you say makes sense to me: you've done what you could, you don't expect to be able to do more. That's a reasonable position.
Théo Zimmermann (Jun 10 2020 at 17:01):I also hope that something good comes out of the discussion and that someone is ready to take over the PR, but I feel obligated to say that it doesn't have to be Maxime, despite his blocking the PR in the current state. Still, it would be great if he does volunteer.
Maxime Dénès (Jun 10 2020 at 19:36):Sure, once I process the items on my current todo-list (document manager, unifall, other Consortium support issues and stdlib2), I'll be glad to have a look at this one. I hope somebody else finds the time before that, though.
Enrico Tassi (Jun 11 2020 at 07:27):Recently I followed the development of Dedukti and, long story short, I discovered a parsing engine (they plan to use) that looks like how I would implement the engine of camlp5 today. Here it is https://github.com/craff/pacomb . I'm thinking that it may be worth looking at that, but it would be even simpler to ask it's author(s?) to present it in a call. What do you think?
Maxime Dénès (Jun 11 2020 at 09:11):Sure, it sounds interesting!
Maxime Dénès (Jun 17 2020 at 10:09):@Enrico Tassi I see that this topic was not added to today's call. Is it on purpose?
Enrico Tassi (Jun 17 2020 at 10:23):Because I failed to get in touch with them, also I did not get many answers here
Pierre-Marie Pédrot (Jun 17 2020 at 13:57):Are we reusing the same link as the last time?
Emilio Jesús Gallego Arias (Jun 17 2020 at 13:59):Pierre-Marie Pédrot said:
Are we reusing the same link as the last time?
Sounds good, but @Théo Zimmermann needs to open the room
Janno (Jun 17 2020 at 14:00):What is the room? (I'll be there in a few minutes)
Pierre-Marie Pédrot (Jun 17 2020 at 14:03):https://bbb2.math.univ-paris-diderot.fr/b/the-mt4-7q4
Pierre-Marie Pédrot (Jun 17 2020 at 14:03):doesn't seem to have been activated though
Enrico Tassi (Jun 17 2020 at 14:03):It seems no yet open
Pierre-Marie Pédrot (Jun 17 2020 at 14:04):and now that I think about it, @Théo Zimmermann told me he wouldn't be able to assist today
Pierre-Marie Pédrot (Jun 17 2020 at 14:04):so he won't be able to open the room
Maxime Dénès (Jun 17 2020 at 14:04):lol
Matthieu Sozeau (Jun 17 2020 at 14:04):Indeed I just saw his message tooo
Pierre-Marie Pédrot (Jun 17 2020 at 14:04):we need a fallback
Enrico Tassi (Jun 17 2020 at 14:04):hum, he is the owner ;-)
shall we try visio.inria.fr or renater?
Pierre-Marie Pédrot (Jun 17 2020 at 14:04):why not
Matthieu Sozeau (Jun 17 2020 at 14:04):Let's try renater?
Enrico Tassi (Jun 17 2020 at 14:05):@Matthieu Sozeau pelase create a link and post it here
Matthieu Sozeau (Jun 17 2020 at 14:05):https://rdv2.rendez-vous.renater.fr/coq-call
Théo Zimmermann (Jun 17 2020 at 15:52):Sorry about this folks! :confounded:
Matthieu Sozeau (Jun 17 2020 at 18:25):No problem, we managed !
Enrico Tassi (Jun 24 2020 at 13:51):Shall we use BBB this time?
Théo Zimmermann (Jun 24 2020 at 13:57):We can: I'm here. But it would contradict what the wiki page says, so it should be updated ASAP if that's the case.
Emilio Jesús Gallego Arias (Jun 24 2020 at 13:59):I guess we could just go back to adding a link to the preferred room of choice
Théo Zimmermann (Jun 24 2020 at 14:00):People are already connected, so let's stick to Renater for now?
Matthieu Sozeau (Jun 24 2020 at 14:00):Let's do BBB again next time
Emilio Jesús Gallego Arias (Jun 24 2020 at 14:04):Yup info is a mess, still the inria link is there
Gaëtan Gilbert (Jul 01 2020 at 09:58):Are people available for today's call considering fscd?
Emilio Jesús Gallego Arias (Jul 01 2020 at 10:09):That's a good point @Gaëtan Gilbert , maybe we should delay?
Matthieu Sozeau (Jul 01 2020 at 13:00):Hmm, I wouldn't mind, it's a busy time indeed. I feel a bit bad about delaying still Jim's PR, what do you think?
Matthieu Sozeau (Jul 01 2020 at 13:05):Also, it's a bit late to delay for people on different time zones... let's see at 4pm if there's enough people around. We can do a quick one maybe, postponing points that are not urgent
Cyril Cohen (Jul 01 2020 at 13:13):It does seem reasonable to postpone it
Matthieu Sozeau (Jul 01 2020 at 14:03):@Jim Fehrle @Jason Gross you had two points raised for this week's call, but it seems many people are away, so they'll be postponed to next week
Jason Gross (Jul 01 2020 at 14:04):Ah, okay
Jason Gross (Jul 01 2020 at 14:04):I guess that means I can go back to sleep :-)
Matthieu Sozeau (Jul 01 2020 at 14:04):Sorry for the late notice !
Jason Gross (Jul 01 2020 at 14:06):No worries, I only woke up 5 minutes ago, so I wouldn't have seen any earlier notice until now (unless you made the decision more than 9 hours ago)
Jim Fehrle (Jul 01 2020 at 15:06):I had intended to be on the call. I set 6:45 AM on my alarm but forgot to turn it on :-(. Where has the text for the items that were on today's agenda gone? Can they be added to the July 8 list or will we need to redraft those items?
Matthieu Sozeau (Jul 01 2020 at 15:09):I moved them to July 8th already !
Jim Fehrle (Jul 01 2020 at 15:36):Ah, but the link was still pointing to the now-empty July 1 page. I fixed this.
Matthieu Sozeau (Jul 07 2020 at 18:48):I'll be on vacations this week and until the 16th, so do not wait for me to have the call. @Maxime Dénès or @Pierre-Marie Pédrot or @Emilio Jesús Gallego Arias can any of you (or anyone voluntary) "lead" them?
Emilio Jesús Gallego Arias (Jul 07 2020 at 18:57):Sure, NP @Matthieu Sozeau , have fun!
Maxime Dénès (Jul 07 2020 at 19:41):I'll be in vacations too.
Emilio Jesús Gallego Arias (Jul 07 2020 at 20:29):Then likely we will postpone, let's see what happens
Pierre-Marie Pédrot (Jul 07 2020 at 22:06):FTR, I am in vacations this week as well.
Emilio Jesús Gallego Arias (Jul 07 2020 at 22:19):Well, I think it makes sense to postpone then; I will update the wiki tomorrow
Emilio Jesús Gallego Arias (Jul 08 2020 at 10:04):In view of the availability of developers, I've postponed the call to next week.
Gaëtan Gilbert (Jul 09 2020 at 09:41):Will anyone be unavailable next week?
Emilio Jesús Gallego Arias (Jul 09 2020 at 12:32):I will be available
Théo Zimmermann (Jul 09 2020 at 12:44):Yeah, me too.
Enrico Tassi (Jul 09 2020 at 15:04):I won't be available, I'll be probably travelling
Jim Fehrle (Jul 10 2020 at 15:39):I will be available. I'd like to cover my twice-postponed item.
Jim Fehrle (Jul 10 2020 at 16:13):I suggest we try to decide whether calls will be postponed at least 12 hours in advance. I have to get up a couple hours early (6:45 AM) to participate. Messages about postponing at 3 AM my time are not helpful; @Emilio Jesús Gallego Arias's "I think it makes sense to postpone then" is reasonable though it could have been more definite. I don't expect to participate in most calls, though.
Jim Fehrle (Jul 14 2020 at 21:27):Is the meeting on for Wednesday?
Jason Gross (Jul 15 2020 at 04:36):I plan on showing up, though I might be around 5 minutes late (or possibly 10, if I'm very tired)
Jason Gross (Jul 15 2020 at 04:38):(and I'd like to request @Hugo Herbelin 's presence to chat about "the various kinds of syntax for global references and what to call them", since I put this bullet point on mainly because I don't have the answers, and I think Hugo was (one of) the primary other participant(s) in the GitHub discussions)
Emilio Jesús Gallego Arias (Jul 15 2020 at 09:02):Monday and Tuesday were holidays in France so not a lot of feedback on this one folks
Emilio Jesús Gallego Arias (Jul 15 2020 at 09:02):But my guess is that quite a few people will be back, so we can try to have the call
Hugo Herbelin (Jul 15 2020 at 09:23):Jason Gross said:
I plan on showing up, though I might be around 5 minutes late (or possibly 10, if I'm very tired)
I would not mind a meeting later in the day. Or, say, to have such discussion, around the end of the call, close to 5PM CEST. (I might actually be late myself.)
Théo Zimmermann (Jul 15 2020 at 14:05):Where is everybody?
Théo Zimmermann (Jul 15 2020 at 14:05):We are just two right now.
Jim Fehrle (Jul 15 2020 at 14:06):I don't see you.
Jim Fehrle (Jul 15 2020 at 14:06):Or hear you.
Théo Zimmermann (Jul 15 2020 at 14:07):Did you use this link to join? https://rdv2.rendez-vous.renater.fr/coq-call
Jim Fehrle (Jul 15 2020 at 14:14):I was using the link on the web page. Should that one be added to it?
Emilio Jesús Gallego Arias (Jul 15 2020 at 14:21):https://github.com/coq/coq/pull/12259
Emilio Jesús Gallego Arias (Jul 15 2020 at 14:34):https://x80.org/coq-coverage/vernac/g_vernac.ml.html
Théo Zimmermann (Jul 15 2020 at 15:56):Please check the notes I took: https://github.com/coq/coq/wiki/Coq-Call-2020-07-15
Jim Fehrle (Jul 15 2020 at 20:54):On the notes: A fair bit of the discussion was about whether the code coverage tool would be a good substitute for my PR. We touched on completeness, maintainability and how often the parsing stats would be used, but we didn't discuss the pros and cons of putting the PR into a branch--it was more like "Could you put this in a branch?" and "Well, it's not my first choice". I'll put my thoughts on that topic in the PR. Probably we should have started by picking someone to really review the PR, which it has not gotten. Perhaps Hugo is willing?
Théo Zimmermann (Jul 16 2020 at 08:26):Feel free to expand the notes. I didn't want to make them too long and it was hard to decide what to select.
Théo Zimmermann (Jul 16 2020 at 08:26):Yes, Hugo seemed to be willing. This is good news because indeed, the main blocker so far has been the lack of a motivated reviewer.
Emilio Jesús Gallego Arias (Jul 20 2020 at 16:27):Hi all, I've added a link https://framadate.org/CHqXytAJQYGWZhRE to schedule the calls this summer; please add your informaiton. Find the link in the wiki too.
Emilio Jesús Gallego Arias (Jul 21 2020 at 14:01):Seems we have quorum for tomorrow
Jason Gross (Jul 22 2020 at 14:39):I seem to have been dropped from the call due to connection issues, and rejoining does not seem to be working
Emilio Jesús Gallego Arias (Jul 22 2020 at 14:40):@Jason Gross we are here
Emilio Jesús Gallego Arias (Jul 22 2020 at 14:40):waiting for you
Théo Zimmermann (Jul 22 2020 at 14:40):We were just about to discuss your point.
Emilio Jesús Gallego Arias (Aug 25 2020 at 12:56):A page has been added for tomorrow; however it wasn't added to the main wiki page?
Emilio Jesús Gallego Arias (Aug 25 2020 at 12:57):Actually that's on conflict with the break stated there
Hugo Herbelin (Aug 25 2020 at 18:02):Actually that's on conflict with the break stated there
OK, so let's move it to next Wednesday.
Emilio Jesús Gallego Arias (Sep 02 2020 at 14:18):We were supposed to hold a call today right?
Gaëtan Gilbert (Sep 02 2020 at 14:22):apparently
Karl Palmskog (Sep 02 2020 at 14:23):if there is one, may I join?
Emilio Jesús Gallego Arias (Sep 02 2020 at 14:23):I was waiting for a ping here :)
Emilio Jesús Gallego Arias (Sep 02 2020 at 14:23):but indeed it was already started
Théo Zimmermann (Sep 08 2020 at 12:36):Hello @Enrico Tassi, I am not sure I will be able to attend tomorrow's call (depends on when a previous meeting ends). I didn't realize SSR was severely broken in 8.12. I assume coq/coq#12857 is the PR that fixes this? It is backported now FWIW. As for when 8.12.1 is released, I was hoping that could wait for October given how busy I am until then but if it's urgent we can certainly do a release sooner.
Enrico Tassi (Sep 08 2020 at 12:59):The problem is that as soon as you have a case/elim in your line, the error message is bogus. So developing new scripts is very painful, while existing scripts just work fine (because they are correct, hence the bug was spot so late). Indeed that is the PR that fixes the issue.
I'm willing to help to get the release out, so if you want me to do some work just ask.
Enrico Tassi (Sep 08 2020 at 13:01):There is also a minor issue with search, since I get the warning (even if I'm using the new syntax). It seems that if you load ssr then you get a warning at every search, dunno if it was expected, but is surely perfectible (but not blocking either).
Karl Palmskog (Sep 08 2020 at 13:03):maybe this isn't the place, to ask, but will the "notation-incompatible-format" warning continue to be a thing in all SSR-based Coq projects on 8.12? Or will we have to wait until 8.13?
Enrico Tassi (Sep 08 2020 at 13:08):I don't recall the details, but if there is a fix/issue you want to be in the point release please set the milestone accordingly.
Enrico Tassi (Sep 08 2020 at 13:08):(I don't recall if we fixed it in MC, or worked around it in MC, or fixed in Coq...)
Théo Zimmermann (Sep 08 2020 at 13:43):Enrico Tassi said:
I don't recall the details, but if there is a fix/issue you want to be in the point release please set the milestone accordingly.
If it's a PR that's already merged, do not just modify the milestone but additionally ping me and Emilio.
Théo Zimmermann (Sep 08 2020 at 13:44):Enrico Tassi said:
There is also a minor issue with search, since I get the warning (even if I'm using the new syntax). It seems that if you load ssr then you get a warning at every search, dunno if it was expected, but is surely perfectible (but not blocking either).
Yes, sorry about that. I think this is expected but could be improved indeed.
Paolo Giarrusso (Sep 08 2020 at 20:52):The problem is that as soon as you have a case/elim in your line, the error message is bogus.
Wait, https://github.com/coq/coq/issues/12837 just says "error reporting on name reuse", which affects ~0% of users. What you describe affects ~100% of ssreflect users.
Paolo Giarrusso (Sep 08 2020 at 20:54):(I naively promised today to @Janno that upgrading to 8.12 would be easy, luckily he's not as easily fooled as me)
Enrico Tassi (Sep 09 2020 at 05:22):I've updated the title. Any error causes the problem.
Théo Zimmermann (Sep 09 2020 at 07:01):@Enrico Tassi Given how serious the problem is, I think the fix should be better highlighted by getting a changelog entry. Would you mind opening a PR adding one?
Enrico Tassi (Sep 09 2020 at 07:12):ok
Paolo Giarrusso (Sep 09 2020 at 08:46):Thanks to you both.
Emilio Jesús Gallego Arias (Sep 09 2020 at 14:01):I guess the call is starting now
Gaëtan Gilbert (Sep 23 2020 at 13:58):starting soon?
Jason Gross (Sep 23 2020 at 14:00):I'm running a couple minutes late, sorry
Théo Zimmermann (Sep 23 2020 at 15:23):Oops, I forgot about it :frown:
Enrico Tassi (Sep 23 2020 at 15:40):me too
Enrico Tassi (Sep 23 2020 at 15:40):but it's not on renater
Matthieu Sozeau (Sep 30 2020 at 08:14):There are no points on the Coq Call page for today, so there will be no call this afternoon.
Gaëtan Gilbert (Oct 07 2020 at 13:56):call today?
Théo Zimmermann (Oct 07 2020 at 14:04):@Karl Palmskog Did you see my e-mail suggesting to join the call today?
Karl Palmskog (Oct 07 2020 at 14:08):@Théo Zimmermann ah, is the call now? I can join now
Théo Zimmermann (Oct 07 2020 at 14:08):Yes :smile:
Théo Zimmermann (Oct 07 2020 at 14:53):Thanks for your participation! This was really useful.
Matthieu Sozeau (Oct 20 2020 at 14:09):I'm on vacations for the next two weeks, so won't be able to attend the calls.
Gaëtan Gilbert (Nov 04 2020 at 14:33):call in 30min
Théo Zimmermann (Nov 04 2020 at 15:02):Why am I alone in the meeting?
Pierre-Marie Pédrot (Nov 04 2020 at 15:03):same here?
Matthieu Sozeau (Nov 04 2020 at 15:03):Why am I too? :)
Emilio Jesús Gallego Arias (Nov 04 2020 at 15:03):I am too
Théo Zimmermann (Nov 10 2020 at 09:21):We have a Coq Call marked as planned tomorrow (@Erik Martin-Dorel added a point to discuss) but it is a national holiday in France (and possibly elsewhere too). What should we do? We could postpone to Thursday or next week (but then this would be after the 8.13 branching point).
Matthieu Sozeau (Nov 10 2020 at 09:23):I think we should postpone to Thursday
Matthieu Sozeau (Nov 10 2020 at 09:23):@Erik Martin-Dorel would that be ok with you?
Erik Martin-Dorel (Nov 10 2020 at 10:32):Hi @Matthieu Sozeau @Théo Zimmermann, Indeed I understand that the Coq call could not take place on tomorrow Wednesday. Regarding Thursday I'll be very busy so I will only have a slot at the end of the day → only at 17:30 or 18:00 Paris time I guess… Would it be feasible for you?
Théo Zimmermann (Nov 10 2020 at 10:33):No, that would be too late for me. What about Friday?
Erik Martin-Dorel (Nov 10 2020 at 10:35):so Friday only in the afternoon: I have a video-call at 14:00 (which should last ~1h I guess) then a lecture from 16:00 to 18:00.
So would you be available before 14:00 or around 15:00 ?
Théo Zimmermann (Nov 10 2020 at 10:38):Friday 15.00 would work for me. Let's see what the others' availability are.
Erik Martin-Dorel (Nov 10 2020 at 10:40):@Théo Zimmermann can one ping the stream by Cc "@all" ?
Théo Zimmermann (Nov 10 2020 at 10:41):There are lots of people subscribed to the stream (252). Let's just ping the usual suspects.
Théo Zimmermann (Nov 10 2020 at 10:43):@Enrico Tassi @Emilio Jesús Gallego Arias @Hugo Herbelin @Gaëtan Gilbert @Pierre-Marie Pédrot @Maxime Dénès @Matthieu Sozeau : would moving the Coq Call to Friday 15.00 work for you?
Enrico Tassi (Nov 10 2020 at 11:01):ok
Karl Palmskog (Nov 10 2020 at 11:06):hopefully I can join as well, I at least have some opinions from general package side (bottom line, I would prefer native is handled compiler-wise per-opam-switch as flambda is)
Erik Martin-Dorel (Nov 13 2020 at 14:01):Sorry I'll have 5' delay for the Coq call... but I'll be available till 16:00
Enrico Tassi (Nov 13 2020 at 14:01):ok
Gaëtan Gilbert (Nov 13 2020 at 14:05):for those who didn't notice: the call is starting now, not in 1h
Théo Zimmermann (Dec 09 2020 at 16:00):Sorry, I had to leave to attend a talk.
Théo Zimmermann (Dec 09 2020 at 17:21):@Matthieu Sozeau Is this really intended that the next Coq Call will be on the 18th (Friday) and not the 16th (Wednesday)? BTW, there is no link from the main Coq Calls page.
Matthieu Sozeau (Dec 09 2020 at 17:34):Thanks, my mistake
Théo Zimmermann (Jan 05 2021 at 16:08):The only two items on the program of tomorrow's Coq Call were added by @Jim Fehrle. Given that I'm not sure myself that I will be able to attend this call and given that there is the Lean Together workshop that starts at the same time, I am wondering how many Coq devs plan to attend this call and whether it should be postponed. Note that @Jim Fehrle needs to know about this today and not tomorrow when he wakes up at 6.30am PST.
Enrico Tassi (Jan 05 2021 at 17:43):I won't be able to attend, I'm afraid.
Matthieu Sozeau (Jan 05 2021 at 19:47):I can attend but given that the discussion is UI-related it's probably better to wait a week for Enrico and you, if that's ok with you @Jim Fehrle
Jim Fehrle (Jan 05 2021 at 19:53):Postponing to next week would be fine. I will update the web page.
Matthieu Sozeau (Jan 13 2021 at 15:02):Call is starting now
Matthieu Sozeau (Jan 20 2021 at 13:20):There will be no call today, I updated the wiki page.
Gaëtan Gilbert (Feb 03 2021 at 11:45):looks like nothing this week
Gaëtan Gilbert (Feb 03 2021 at 11:46):Didn't something get postponed last week though?
Matthieu Sozeau (Feb 03 2021 at 14:02):Théo had a point about locality attributes that was not adressed IIRC. @Théo Zimmermann are you available to talk about it?
Théo Zimmermann (Feb 03 2021 at 14:08):Yes, I'm available.
Théo Zimmermann (Feb 03 2021 at 14:08):And there was a second point by @Enrico Tassi which was not discussed about the minimal OCaml version to require for 8.14.
Matthieu Sozeau (Feb 03 2021 at 14:09):Ok, let's move them both to today's page
Matthieu Sozeau (Feb 03 2021 at 15:02):@Enrico Tassi will you join us today?
Enrico Tassi (Feb 03 2021 at 15:02):Sure, 1 minute
Gaëtan Gilbert (Feb 04 2021 at 10:02):I checked and ocamldebug is still dead slow on 4.11.1 btw
Enrico Tassi (Feb 04 2021 at 11:01):It has never been fast enough for me, so I don't really care. But if other use it, I guess this is a show stopper for 8.11
Matthieu Sozeau (Feb 17 2021 at 13:53):Hi guys, I'm on vacations this week so I won't be able to follow the Coq Call, but I'd be interested in notes about the topics this week, if anyone can volunteer!
Enrico Tassi (Feb 17 2021 at 14:00):I can take notes
Matthieu Sozeau (Feb 17 2021 at 14:08):Thanks !
Enrico Tassi (Feb 24 2021 at 08:35):I see no page but we have the dune update to discuss, right?
Enrico Tassi (Feb 24 2021 at 08:35):Cc @Emilio Jesús Gallego Arias
Matthieu Sozeau (Feb 24 2021 at 14:01):I'm still on vacations, so don't wait for me :)
Emilio Jesús Gallego Arias (Feb 24 2021 at 14:54):Oh I thought we had updated the page, indeed it would be good if we could chat a bit about the build system
Enrico Tassi (Mar 04 2021 at 07:23):Did anyone take notes yesterday?
Théo Zimmermann (Mar 04 2021 at 08:30):@Emilio Jesús Gallego Arias said he would.
Emilio Jesús Gallego Arias (Mar 04 2021 at 14:11):I took notes for the first part that was on the agenda, the rest of the discussion maybe someone else is better to summarize?
Emilio Jesús Gallego Arias (Mar 04 2021 at 14:12):@Enrico Tassi I ping you as indeed the discussion needs a bit more feedback
Emilio Jesús Gallego Arias (Mar 04 2021 at 14:12):once the notes are in the wiki I mean
Emilio Jesús Gallego Arias (Mar 12 2021 at 09:38):@Enrico Tassi here they are https://github.com/coq/coq/wiki/Coq-Call-2021-03-03
Emilio Jesús Gallego Arias (Mar 12 2021 at 09:38):not sure what more can I add to the notes, please review and let me know what you think
Enrico Tassi (Mar 12 2021 at 13:20):Hum, I see. having roadmaps is a good objective, but I think @Maxime Dénès tried keeping them (for the whole dev team) and it did not work
Théo Zimmermann (Mar 12 2021 at 13:29):This is not the same kind of roadmap AFAIU. This is not about saying what will be in the next release (something we don't know how to do) but about making people that work on the same topics coordinate and share info.
Emilio Jesús Gallego Arias (Mar 12 2021 at 14:22):Yeah, I mean roadmap here in the sense of avoiding duplicate work and generally being in sync, we have a few examples already, like the Pp.t printer Shachar developed, or code in vscoq-lsp that was already solved in sername by Karl, or the base coq-lsp for example on which that project started.
Enrico Tassi (Mar 12 2021 at 14:38):code in vscoq-lsp that was already solved in sername by Karl
can you elaborate?
Emilio Jesús Gallego Arias (Mar 12 2021 at 14:42):can you elaborate?
Emilio Jesús Gallego Arias (Mar 12 2021 at 14:42):I don't recall the details, was some parsing / tokenization stuff, that Maxime was doing then by chance was already done by Karl
Emilio Jesús Gallego Arias (Mar 12 2021 at 14:43):so indeed these kind of common requirements for the platform can be better identified
Emilio Jesús Gallego Arias (Mar 12 2021 at 14:44):This is the thread https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs.20.26.20plugin.20devs/topic/Parsing.20interface/near/199297523
Gaëtan Gilbert (Mar 31 2021 at 11:26):bit late to schedule a call @Pierre-Marie Pédrot
Pierre-Marie Pédrot (Mar 31 2021 at 11:27):that's fine if we don't discuss this today
Pierre-Marie Pédrot (Mar 31 2021 at 11:28):it's long term stuff for which I am seeking wise advice
Emilio Jesús Gallego Arias (Mar 31 2021 at 12:16):I have many woes with libobject too , so indeed even if it is just some chat about options would be very helpful
Matthieu Sozeau (Mar 31 2021 at 12:33):Let's have it then
Théo Zimmermann (Apr 07 2021 at 07:38):@Arthur Charguéraud It's a bit late to add that many topics to the Coq Call, don't you think?
Théo Zimmermann (Apr 07 2021 at 07:39):@Arthur Charguéraud And I'm also annoyed by your pushing the only point that was on the agenda to the end and the comment you added.
Théo Zimmermann (Apr 07 2021 at 07:40):E.g., did you ask someone about doing a "Quick report on the current development status of custom entry." ?
If not, then it seems pretty much inappropriate to ask this by adding it to today Call's topics.
Arthur Charguéraud (Apr 07 2021 at 07:56):Hi, maybe I have a different perspective than you on what are the purpose of Coq Calls. My understanding is: discuss things that can take 10 minutes in a live chat whereas would take weeks of non-converging discussions in async chat. But please share with me the definition of the Coq Calls as you see them, and I would be happy to follow whatever it is.
Arthur Charguéraud (Apr 07 2021 at 07:58):sorry if my comment on coq name was inappropriate, i'm probably lacking context here
Théo Zimmermann (Apr 07 2021 at 08:04):I wasn't the one who added the naming question to the Call, @Matthieu Sozeau did, but given the role I have ended up taking in structuring the Coq-Club discussion (did you follow that?), I cannot miss this discussion. Hopefully, it won't take too long but I'm not sure about that. But most importantly, I think you are completely underestimating the time it will take to discuss each of your own points. The Coq Call is not supposed to last longer than one hour and I personally cannot go overtime because of teaching duties.
Matthieu Sozeau (Apr 07 2021 at 08:10):Indeed, I did. I think the points of Arthur can still be discussed, and we'll move some to next week if we can't talk about all of them in the 1hour time-slot. But yeah, if you want Hugo to talk about custom entries, then it might be good to give him a heads up :)
Arthur Charguéraud (Apr 07 2021 at 08:29):Let me suggest the following regarding custom entry: I'll try to catch Hugo privately to ask him the questions I have in mind, and, if revelant, I'll post a summary of our discussion and/or schedule discussion for a follow-up call. thanks. Regarding the other points, if there is no time to discuss, what I'd like to do is simply to figure out "who is able/interested to discuss that topic with me, in the aim of coming up with very concrete proposals at a follow-up coq call". I purposely don't want to start the discussion on hints on zulip/discuss/github/younameit, because in my experience it does not converge well.
Jason Gross (Apr 14 2021 at 00:21):I've created a page and added a topic that I'd like to discuss to it: I'd like to discuss the future of coq_makefile customization (https://github.com/coq/coq/pull/12411), in particular variable overriding and use of variables. cc @Emilio Jesús Gallego Arias and @Enrico Tassi @Gaëtan Gilbert . Apologies if this is too late to add things to coq-call; if so I'm happy to defer to next week.
Pierre-Marie Pédrot (Apr 14 2021 at 11:19):@Jason Gross there is the HoTT EPIT going on this week, so at least @Matthieu Sozeau and myself won't be around. Since you're the only one to have proposed something on the wiki so far, and I've already recommended to some other people to postpone topics next week, it'd probably be better to postpone yours as well.
Jason Gross (Apr 14 2021 at 12:07):Ah, okay, I'll postpone to next week
Théo Zimmermann (Apr 14 2021 at 12:39):Updated on the wiki
Emilio Jesús Gallego Arias (Apr 14 2021 at 13:35):@Jason Gross , I had a look to the issue you point out, IMHO if you worry about tracking the coq used to build files I'd go the way Dune works [dune will correctly track coqc and rebuild if coqc changes], which would be to add this dependency to the core makefile rules. For that to work on make you'd need to have a rule that generates coqc.hash , but that is fine AFAICT.
Matthieu Sozeau (May 10 2021 at 07:29):I'm on vacations and won't be available for the Coq Call this week.
Jason Gross (May 12 2021 at 13:12):Is the call happening? I get that the call hasn't started yet
Pierre-Marie Pédrot (May 12 2021 at 13:24):Tomorrow (Thursday) stats a long week-end for most French people, so it's likely that there are not many people around.
Pierre-Marie Pédrot (May 12 2021 at 13:25):(I'd myself prefer postponing the call, but I can attend if we maintain it.)
Enrico Tassi (May 12 2021 at 13:30):There is a topic by Jim
Enrico Tassi (May 12 2021 at 13:30):I'd also like some advice for the opaque-def-no-body patch
Pierre-Marie Pédrot (May 12 2021 at 13:30):hm, for this kind of stuff I prefer having a one-to-one conversation
Enrico Tassi (May 12 2021 at 13:30):isn't the call in 30' ?
Pierre-Marie Pédrot (May 12 2021 at 13:31):yup
Enrico Tassi (May 12 2021 at 13:31):I get that the call hasn't started yet
Jason Gross (May 12 2021 at 13:38):Oops, I was off by an hour
Théo Zimmermann (May 12 2021 at 13:56):The current topic was added by Jim on the previous call and was postponed to this week by Matthieu. I don't know if Jim plans on attending.
Théo Zimmermann (May 12 2021 at 13:57):Jim just committed, so he obviously plans on attending.
Théo Zimmermann (May 12 2021 at 13:58):Postponing now would not be nice given that he has woken up early for this.
Pierre-Marie Pédrot (May 12 2021 at 14:00):ok
Théo Zimmermann (May 12 2021 at 14:04):@Emilio Jesús Gallego Arias are you joining as well?
Matthieu Sozeau (May 19 2021 at 13:34):There is one point to discuss on today's Coq Call: https://github.com/coq/coq/wiki/Coq-Call-2021-05-19
Matthieu Sozeau (May 19 2021 at 13:35):I updated the main page
Emilio Jesús Gallego Arias (May 20 2021 at 08:51):Sorry I was on the road and couldn't login to signal my abscence
Gaëtan Gilbert (May 26 2021 at 13:57):the call approaches
Théo Zimmermann (May 26 2021 at 14:00):So it seems that rendez-vous is down?
Gaëtan Gilbert (May 26 2021 at 14:01):is it?
Théo Zimmermann (May 26 2021 at 14:01):I get:
Un incident est en cours sur la majeure partie des services numériques du GIP RENATER. Les équipes techniques sont mobilisées pour rétablir l'accès aux services au plus vite.
when trying to log in.
Matthieu Sozeau (May 26 2021 at 14:01):I'll share a Zoom link
Matthieu Sozeau (May 26 2021 at 14:02):https://univ-nantes-fr.zoom.us/j/3070423803
Gaëtan Gilbert (May 26 2021 at 14:03):no zoom please
Gaëtan Gilbert (May 26 2021 at 14:03):it regularly bugs for me
Théo Zimmermann (May 26 2021 at 14:03):Ahem
Matthieu Sozeau (May 26 2021 at 14:04):Let's do https://whereby.com/mattam82
Emilio Jesús Gallego Arias (Jun 02 2021 at 14:02):Hi folks, I see no call today, right?
Matthieu Sozeau (Jun 02 2021 at 14:02):Yep, no call today
Matthieu Sozeau (Jun 09 2021 at 13:25):No call today either, I guess everyone is busy finishing his/her PRs ;)
Emilio Jesús Gallego Arias (Jun 15 2021 at 15:30):Related to tomorrow's call https://www.theregister.com/2021/06/15/coq_programming_language_change/
Emilio Jesús Gallego Arias (Jun 15 2021 at 15:30):only 106 comments XD
Théo Zimmermann (Jun 15 2021 at 15:45):Thanks for the pointer.
Emilio Jesús Gallego Arias (Jun 15 2021 at 18:05):Théo Zimmermann said:
Thanks for the pointer.
I assume Théo they didn't contact you, right?
Emilio Jesús Gallego Arias (Jun 15 2021 at 18:05):As the reporter writes "according to Théo" XD
Théo Zimmermann (Jun 15 2021 at 21:07):They didn't. They cite what I wrote in the wiki.
Matthieu Sozeau (Jun 16 2021 at 08:59):The article is a nice summary!
Théo Zimmermann (Jul 06 2021 at 08:16):@Hugo Herbelin @Emilio Jesús Gallego Arias When creating a Coq Call page, don't forget to add it to the main index. This is the place where I look to know whether there will be a Coq Call. If there is no link, I can miss that the page exists.
Hugo Herbelin (Jul 06 2021 at 08:31):I forgot, sorry.
Gaëtan Gilbert (Jul 08 2021 at 15:27):Is next call really July 14th? cc @Emilio Jesús Gallego Arias
Gaëtan Gilbert (Jul 08 2021 at 15:27):(who made the page)
Théo Zimmermann (Jul 08 2021 at 15:49):Probably a silly mistake. Let's move it to the week after.
Matthieu Sozeau (Jul 08 2021 at 15:55):We said we wanted to move it the 13th.
Matthieu Sozeau (Jul 08 2021 at 15:55):After that I'll be on vacations, and I expect I'm not the only one :)
Théo Zimmermann (Jul 08 2021 at 17:18):Ah OK.
Stéphane Desarzens (Jul 08 2021 at 20:32):Last week, I somehow couldn't get the audio working. Some technical problem, no idea. This week's call, I missed. Maybe I'll be able to listen in next week.
Emilio Jesús Gallego Arias (Jul 08 2021 at 22:57):Yup, we said we'd do the 13th, sorry we didn't move the page
Ali Caglayan (Jul 11 2021 at 14:16):By the way I added CEP #50 to the coq call so we can discuss it if that's alright.
Matthieu Sozeau (Jul 12 2021 at 08:53):@Théo Winterhalter should probably join for this :)
Théo Winterhalter (Jul 12 2021 at 09:25):I cannot guarantee I can join as I am starting my vacations today.
Matthieu Sozeau (Jul 12 2021 at 09:25):Ok, enjoy!
Théo Winterhalter (Jul 12 2021 at 09:27):Thanks. If I can make time I'll try to be there.
Emilio Jesús Gallego Arias (Jul 13 2021 at 14:32):Reminder the call is going on today, not tomorrow
Emilio Jesús Gallego Arias (Sep 07 2021 at 16:25):Hi folks, I happen to have a doctor before the call, I may be late tomorrow
Emilio Jesús Gallego Arias (Sep 15 2021 at 13:57):Hi folks, it seems I'm super late on another call, which is critical :S
Emilio Jesús Gallego Arias (Sep 15 2021 at 15:33):Actually, regarding the CI platform build, there are two open bugs in the platform already: https://github.com/coq/platform/issues/130 and https://github.com/coq/platform/issues/131 , so not adding duplicated coq bugs for now
Emilio Jesús Gallego Arias (Sep 15 2021 at 15:54):@Pierre-Marie Pédrot "quien dijo miedo" w.r.t. compiler-libs, c.f. https://twitter.com/derKha/status/1438064239365738498
Zig might be the craziest compiler project I've seen recently. After solving cross-compilation by shipping ALL THE LIBCS, and after starting work on their very own, incremental linker, adding a custom C compiler feels only natural :big_smile: . https://twitter.com/andy_kelley/status/1438029763348602884
- Sebastian Ullrich (@derKha) Enrico Tassi (Sep 22 2021 at 13:36):It seems the only topic is a PR by @Pierre-Marie Pédrot which happens to be merged. Do we really need to chat about it?
Pierre-Marie Pédrot (Sep 22 2021 at 13:38):I think @Emilio Jesús Gallego Arias wanted to chat about the old and new invariants of the kernel
Pierre-Marie Pédrot (Sep 22 2021 at 13:43):I don't know if it's super interesting for everybody, we can turn that into a private discussion with the relevant people
Pierre-Marie Pédrot (Sep 22 2021 at 13:43):I do need input from @Matthieu Sozeau about MetaCoq though
Emilio Jesús Gallego Arias (Sep 22 2021 at 13:43):I am OK both chatting online of sending my questions on the issue tracker
Enrico Tassi (Sep 22 2021 at 13:49):I won't attend, but if someone writes these invariants down I'd be happy to read them
Pierre-Marie Pédrot (Sep 22 2021 at 13:50):easy: it's the opposite of MetaCoq
Enrico Tassi (Sep 22 2021 at 13:51):Oh I see, the two invariants are A and not(A). Its a good start ;-)
Matthieu Sozeau (Sep 22 2021 at 13:54):@Pierre-Marie Pédrot We can have a quick chat the three of us at the Coq Call, can't hurt
Pierre-Marie Pédrot (Sep 22 2021 at 13:54):fine
Ali Caglayan (Sep 28 2021 at 11:14):I've added a page for tomorrow since there are a few things I want to discuss
Gaëtan Gilbert (Sep 28 2021 at 12:06):If you want feedback on PRs you shouldn't leave them as draft
Matthieu Sozeau (Oct 06 2021 at 08:04):Just to inform you I won’t be available today and certainly Gaëtan and Pierre-Marie won’t make it either: it’s Gallinette’s “séminaire au vert”
Théo Zimmermann (Oct 06 2021 at 08:59):Should we postpone today's call? @Emilio Jesús Gallego Arias WDYT? You were the one who added the single item on the agenda.
Emilio Jesús Gallego Arias (Oct 06 2021 at 10:22):Sure, let's postpone then; tho we should try to postpone the day before at the very least so people have time to react
Théo Zimmermann (Oct 06 2021 at 10:24):Yeah, @Matthieu Sozeau, @Gaëtan Gilbert and @Pierre-Marie Pédrot, you could have told us about this seminar earlier. I suppose you didn't learn about it today!
Emilio Jesús Gallego Arias (Oct 06 2021 at 10:29):I will be around if anyone was planning to attend and would like to discuss stuff I could help with
Matthieu Sozeau (Oct 12 2021 at 12:17):Sorry for the late notice indeed
Théo Zimmermann (Oct 13 2021 at 16:52):Feel free to continue posting your ideas on automatically reporting warnings in CI in https://github.com/coq/bot/issues/169.
Emilio Jesús Gallego Arias (Oct 14 2021 at 15:57):Folks this is a reminder to move the topics not handled in a call to the next one; I've done so myself a few times.
Emilio Jesús Gallego Arias (Oct 26 2021 at 19:03):I won't likely be available tomorrow [tho I'll try, but likely not online at that time]
Emilio Jesús Gallego Arias (Oct 26 2021 at 19:03):So if you need me for any topic, it must be moved to next week, sorry
Emilio Jesús Gallego Arias (Oct 27 2021 at 00:52):I'd be happy to discuss on the issues too
Karl Palmskog (Oct 27 2021 at 15:11):my interpretation of what was said about announcements of Coq releases in the call:
On the release of the first release candidate for a major Coq version, we make essentially the same announcement publicly as Michael Soegtrop does to Platform project maintainers, in the vein of
A new Coq release candidate is out - Coq library maintainers and plugin authors, please test your code against this version and tag your repos to ensure your users will have a timely package for the final Coq version release
Guillaume Melquiond (Oct 27 2021 at 15:13):This is what I wrote in the wiki notes. Feel free to modify as you see fit.
Release candidate has been tagged. It can be experimented using core-dev. Library maintainers are encouraged to test and upgrade their libraries so that they are ready by the time of the actual release. In particular, maintainers of libraries that are part of the Coq platform should eagerly release compatible versions, so as to not delay the release of the Coq platform.
Théo Zimmermann (Oct 27 2021 at 15:32):Following your note on the wiki page, I've opened a PR updating the release documentation: https://github.com/coq/coq/pull/15080
Gaëtan Gilbert (Nov 10 2021 at 15:14):having some browser issues, trying to get it fixed
Emilio Jesús Gallego Arias (Dec 03 2021 at 13:00):@Enrico Tassi Francois can make it next week, you can too then?
Enrico Tassi (Dec 03 2021 at 13:39):Yes I'll do my best
Emilio Jesús Gallego Arias (Dec 08 2021 at 13:17):Hi folks very unfortunately due to travel changes I won't be able to make the call today
Emilio Jesús Gallego Arias (Dec 08 2021 at 13:17):I may, I dunno, I'll be on a train, so I'll try
Emilio Jesús Gallego Arias (Dec 08 2021 at 13:17):François is coming so please let him know if there is some other problem
Jason Gross (Dec 08 2021 at 15:03):I'm getting a "wait for the host to start the meeting" message
Jason Gross (Dec 08 2021 at 15:03):0e3147b9-1858-4e46-9bd6-fab5160d0d72.png
Gaëtan Gilbert (Dec 08 2021 at 15:05):on https://rdv2.rendez-vous.renater.fr/coq-call ? works for me
Jason Gross (Dec 08 2021 at 15:15):Strange, I guess jitsi doesn't automatically let me in when the meeting starts if I join before the host?
Emilio Jesús Gallego Arias (Dec 08 2021 at 16:15):Didn't manage to make it worry folks
Emilio Jesús Gallego Arias (Dec 08 2021 at 16:18):What Francois able to make it too? I just saw a message from him telling me he had some trouble
Théo Zimmermann (Dec 08 2021 at 16:22):Yes he was there.
Théo Zimmermann (Dec 08 2021 at 16:23):See the notes that Enrico has added in the header of PR https://github.com/coq/coq/pull/15220.
Théo Zimmermann (Dec 15 2021 at 18:46):What ended up being discussed in today's call?
Emilio Jesús Gallego Arias (Dec 15 2021 at 23:28):A lot of stuff
Emilio Jesús Gallego Arias (Dec 15 2021 at 23:28):For the name change, we discussed whether we should provide/update a roadmap
Emilio Jesús Gallego Arias (Dec 15 2021 at 23:28):For the Feb 2022 WG, a preliminar date is 14 Feb and that week, but still too many variables, so not fixed
Emilio Jesús Gallego Arias (Dec 15 2021 at 23:29):Dune + findlib chat time was mostly a review of things we have already said regarding the roadmap of the build system, such a generating rules ourselves instead of using the ML side implementation
Emilio Jesús Gallego Arias (Dec 15 2021 at 23:29):Holiday break I don't remember
Emilio Jesús Gallego Arias (Dec 15 2021 at 23:30):Also Ali asked about SerAPI and Coq's CI, I answered with my point of view
Emilio Jesús Gallego Arias (Dec 15 2021 at 23:30):Then there was a long discussion I had to miss regarding the front-end, but it is interesting many of this points were known a long time ago
Emilio Jesús Gallego Arias (Dec 15 2021 at 23:30):there are like basic things you want when buidling a UI
Emilio Jesús Gallego Arias (Dec 15 2021 at 23:31):So there was a lot of discussion here, and I'm not sure I still understand many of the arguments but I guess we wil have more meetings soon
Ali Caglayan (Dec 16 2021 at 00:00):We also discussed moving forward with the inductive inductive branch briefly at the end
Ali Caglayan (Dec 16 2021 at 00:01):We can def break some stuff up in there and implement finished parts
Maxime Dénès (Dec 16 2021 at 08:42):Emilio Jesús Gallego Arias said:
Holiday break I don't remember
No calls for the next two weeks, something like that. @Matthieu Sozeau will know exactly.
Maxime Dénès (Dec 16 2021 at 08:43):Emilio Jesús Gallego Arias said:
there are like basic things you want when buidling a UI
Yes, we mentioned separation of phases (parsing, globalisation of names, execution).
Matthieu Sozeau (Dec 16 2021 at 10:16):Sorry I forgot to take notes, but Emilio’s summary is right. Indeed next call is in January
Jim Fehrle (Jan 02 2022 at 06:30):The next call is January 5?
Gaëtan Gilbert (Jan 02 2022 at 10:15):only if someone adds a topic
Jim Fehrle (Jan 04 2022 at 04:15):Done.
Théo Zimmermann (Jan 05 2022 at 14:52):Hi all, and happy new year! If nobody needs me for the Call, I think I will skip it today to focus on pressing topics.
Matthieu Sozeau (Jan 11 2022 at 19:48):Happy New Year Théo. I likely won't be able to make it tomorrow, I have an overlapping meeting, can someone take over the "chair" role?
Emilio Jesús Gallego Arias (Jan 11 2022 at 21:30):No worries @Matthieu Sozeau I can take the notes
Matthieu Sozeau (Feb 23 2022 at 10:09):I’m on holidays this week, can someone else act as chair for the call ?
Emilio Jesús Gallego Arias (Feb 23 2022 at 10:17):It is very bad timing for me for the call too
Emilio Jesús Gallego Arias (Feb 23 2022 at 10:18):due to inria CR deadline being next Tue
Emilio Jesús Gallego Arias (Feb 23 2022 at 10:18):I'd appreciate if non urgent topics of my interest could be discussed next week
Ali Caglayan (Feb 23 2022 at 10:33):I can act as chair if needed
Enrico Tassi (Feb 23 2022 at 10:49):I will attend, and I can take notes.
Enrico Tassi (Feb 23 2022 at 10:50):@Emilio Jesús Gallego Arias there is a topic by jim which may be of interest for you (but postponing it now is not ideal for jim)
Emilio Jesús Gallego Arias (Feb 23 2022 at 10:52):thanks @Enrico Tassi , I guess it is fine if you folks discuss that one without me, all that I have to say about that is from discussion with Makarius and Clement on the topic of editors and UI locking
Emilio Jesús Gallego Arias (Feb 23 2022 at 10:52):indeed they recommend to avoid it at all costs, however that requires a protocol which act as a state machine
Emilio Jesús Gallego Arias (Feb 23 2022 at 10:53):jscoq uses this approach and works well, but I'm not sure if it can be done without rewriting the xml protocol
Emilio Jesús Gallego Arias (Feb 23 2022 at 10:53):I will maybe say more on the UI meeting
Emilio Jesús Gallego Arias (Feb 23 2022 at 18:01):So are there notes of the meeting today?
Enrico Tassi (Feb 23 2022 at 18:24):I have not posted them yet, I'll do it later today, or tomorrow
Enrico Tassi (Feb 23 2022 at 21:11):Notes are online, all people attending are welcome to improve them
Emilio Jesús Gallego Arias (Mar 02 2022 at 13:28):No Coq call today, correct?
Matthieu Sozeau (Mar 02 2022 at 14:21):Correct
Gaëtan Gilbert (Mar 30 2022 at 13:11):not a lot of calls recently
Pierre-Marie Pédrot (Mar 30 2022 at 13:33):too busy wreaking havoc in universe internals to chat about it :nuclear:
Théo Zimmermann (Mar 30 2022 at 13:58):We could try to plan next week's Coq Call already. For instance, shouldn't we discuss if we want to bump OCaml in 8.16?
Michael Soegtrop (Mar 30 2022 at 16:21):FTR: I latest Coq Platform 8.15~2022.03 I am now using Ocaml 4.13+flambda. Newer versions might also work, but this is what @Emilio Jesús Gallego Arias recommended. 8.14 uses OCaml 4.12+flambda and older versions use 4.10.2 (all because some packages don't build with newer OCaml). So this is the first Coq Platform, where different picks use different OCaml versions - which I guess was inevitable on the long term.
Emilio Jesús Gallego Arias (Mar 30 2022 at 16:23):@Michael Soegtrop I don't understand what you mean by "different picks use different OCaml versions"
Emilio Jesús Gallego Arias (Mar 30 2022 at 16:24):Yup 4.13 is good, specially for those on newer mac
Michael Soegtrop (Mar 30 2022 at 16:37):@Emilio Jesús Gallego Arias : each release of Coq Platform (like 2022.03) supports different Coq versions, usually each with 2 package picks - one with packages which where current when this version of Coq was released and one which is close to the initial pick of the next Coq version. These combinations of Coq versions and package selection are called "picks" in Coq Platform jargon.
In the past all picks used the same version of OCaml (4.10.2 in the 2022.01 release). Now each pick can specify an OCaml version.
Michael Soegtrop (Mar 30 2022 at 16:37):See (https://github.com/coq/platform/blob/main/README.md)
Emilio Jesús Gallego Arias (Mar 30 2022 at 16:42):Ah, I see thanks. I didn't know you supported multiple Coq versions per platform
Michael Soegtrop (Mar 30 2022 at 16:48):This makes maintenance for old versions easier - e.g. in case OCaml breaks by a system change as seen for Ubuntu 21. We want old Coq versions still to work to ease porting and/or paper artifact exploration. Currently it goes back to 8.12.2. Also having structured support for multiple Coq versions (by separate opam switches) makes porting easier. E.g. my opam switch output looks like this:
# switch compiler description
__coq-platform.2022.03.0~8.12 ocaml-base-compiler.4.10.2 Coq 8.12.2 (released Dec 2020) with the first package pick from Dec 2020
__coq-platform.2022.03.0~8.13~2021.02 ocaml-base-compiler.4.10.2 Coq 8.13.2 (released Apr 2021) with the first package pick from Feb 2021
__coq-platform.2022.03.0~8.13~2021.09 ocaml-base-compiler.4.10.2 Coq 8.13.2 (released Apr 2021) with an extended package pick from Sep 2021
__coq-platform.2022.03.0~8.13~2022.01 ocaml-base-compiler.4.10.2 Coq 8.13.2 (released Apr 2021) with an updated package pick from Jan 2022
__coq-platform.2022.03.0~8.14~2022.01 ocaml-option-flambda.1,ocaml-variants.4.12.1+options Coq 8.14.1 (released Nov 2021) with the first package pick from Jan 2022
__coq-platform.2022.03.0~8.14~2022.03 ocaml-option-flambda.1,ocaml-variants.4.12.1+options Coq 8.14.1 (released Nov 2021) with an updated package pick from Mar 2022
__coq-platform.2022.03.0~8.15~2022.03 ocaml-option-flambda.1,ocaml-variants.4.13.1+options Coq 8.15.1 (released Mar 2022) with the first package pick from Mar 2022
-> __coq-platform.2022.03.0~dev ocaml-option-flambda.1,ocaml-variants.4.12.1+options Coq dev (latest master of all packages)
Also this way all enhancements to the Coq Platform infrastructure - say nicer Readme files - automatically apply to all Coq versions.
Jason Gross (Mar 31 2022 at 15:19):I'd also be interested in discussing https://github.com/coq/coq/issues/15663 synchronously (and should be able to actually make the call this time because I'll be in London for the next two months)
Pierre-Marie Pédrot (Apr 06 2022 at 12:02):Do we get a call today? We still haven't discussed the OCaml version bump.
Pierre-Marie Pédrot (Apr 06 2022 at 12:03):(I'd like to discuss https://github.com/coq/coq/pull/15890 as well but the main people that care about this are already aware of it)
Jason Gross (Apr 06 2022 at 12:35):I can make it (and would be interested in discussing https://github.com/coq/coq/issues/15663 if @Enrico Tassi is available), though there's no link on the wiki
Théo Zimmermann (Apr 06 2022 at 12:36):The link gets created by whoever wants the call to happen (usually not that late, but well...)
Jason Gross (Apr 06 2022 at 12:40):Is it too late to make it now?
Gaëtan Gilbert (Apr 06 2022 at 12:41):we can do anything we want, even have a visio right now instead of waiting for the usual time if we decide to
Théo Zimmermann (Apr 06 2022 at 12:44):I'd say go ahead and create the page. You're just not guaranteed to get as many participants as if it had been announced earlier.
Pierre-Marie Pédrot (Apr 06 2022 at 12:50):let's get a call then
Pierre-Marie Pédrot (Apr 06 2022 at 12:52):https://github.com/coq/coq/wiki/Coq-Call-2022-04-06
Enrico Tassi (Apr 06 2022 at 12:54):@Jason Gross I'm on VAC today, I may be able to chat a little, but not join the call
Enrico Tassi (Apr 06 2022 at 12:55):Next week does not work either for me, but the following one should be fine
Enrico Tassi (Apr 06 2022 at 12:56):So IMO the best is to chat asynchronously if the issue if pressing for you
Pierre-Marie Pédrot (Apr 06 2022 at 12:58):the ocaml version bump has been discussed regularly but we never converged
Pierre-Marie Pédrot (Apr 06 2022 at 12:58):I think we need a synchronous decision for this one
Jason Gross (Apr 06 2022 at 13:12):The issue is not pressing, let's postpone to the week after next?
Pierre-Marie Pédrot (Apr 06 2022 at 13:15):fine fine
Pierre-Marie Pédrot (Apr 06 2022 at 13:16):I might not be around though
Pierre-Marie Pédrot (Apr 06 2022 at 13:16):so do we cancel this short-lived call already?
Ali Caglayan (Apr 06 2022 at 13:21):I don't think they are talking about cancelling this call, just what Jason wanted to talk about.
Jason Gross (Apr 06 2022 at 13:52):Yeah, I'm just talking about postponing the OCAMLPATH / COQBIN issue
Jason Gross (Apr 06 2022 at 13:52):(sorry for the ambiguity)
Jason Gross (Apr 06 2022 at 14:01):(ah, actually it looks like I won't be able to make it to the call today. Guess it's good the OCAMLPATH wasn't scheduled for today)
Gaëtan Gilbert (Apr 12 2022 at 11:01):lots of stuff in https://github.com/coq/coq/wiki/Coq-Call-2022-04-13 but will people be there to discuss? (I won't)
Pierre-Marie Pédrot (Apr 12 2022 at 11:56):won't be there either
Enrico Tassi (Apr 12 2022 at 12:24):Sorry @Jim Fehrle , but I don't think I'll make it either.
Maxime Dénès (Apr 12 2022 at 17:22):Let's postpone, to avoid having the discussions twice, then
Théo Zimmermann (Apr 13 2022 at 07:08):It doesn't look to me like @Jim Fehrle has seen these messages. It's unfortunate that the Coq Call page was not modified.
Emilio Jesús Gallego Arias (Apr 13 2022 at 12:36):Yes, let's postpone, I don't be available today and next week either.
Théo Zimmermann (Apr 13 2022 at 12:37):Can someone update the wiki?
Matthieu Sozeau (Apr 13 2022 at 13:03):I'll do it
Jim Fehrle (Apr 13 2022 at 13:54):OK, see you guys next week, then.
Jim Fehrle (Apr 14 2022 at 19:05):@Matthieu Sozeau Shouldn't the postponed topics be addressed first in the Coq Call and agenda for April 20?
Gaëtan Gilbert (Apr 14 2022 at 19:08):will there be any more people available next week? it's still easter holiday season
Maxime Dénès (Apr 15 2022 at 13:03):I'll be on vacations
Emilio Jesús Gallego Arias (Apr 15 2022 at 14:08):I won't be available either
Jim Fehrle (Apr 18 2022 at 20:23):Can we figure out whether the meeting will take place by the end of Tuesday? Not a fan of getting up at 6:30 AM for a meeting that doesn't take place. If @Emilio Jesús Gallego Arias isn't available, perhaps I should postpone the debugger items until next week.
Enrico Tassi (Apr 18 2022 at 20:25):I won't be available.
Théo Zimmermann (Apr 19 2022 at 08:30):It looks like lots of developers won't be there (I'm not sure I can attend either), so it looks safer to postpone.
Maxime Dénès (Apr 19 2022 at 08:58):Yes, let's postpone.
Matthieu Sozeau (Apr 19 2022 at 09:48):Ok, let's postpone again, I'll put your items on top @Jim Fehrle
Karl Palmskog (Apr 27 2022 at 10:18):just FYI, was hoping we could do a quick "roll call" at start of the call about who (if anyone?) is going to FLoC from core this year
Théo Zimmermann (Apr 27 2022 at 11:30):I know that Jason will go, and I think I won't.
Gaëtan Gilbert (May 04 2022 at 14:02):allo
Théo Zimmermann (May 04 2022 at 14:06):Nobody's here today?
Pierre-Marie Pédrot (May 04 2022 at 14:06):As for myself, I'm in a train with a crappy connection.
Emilio Jesús Gallego Arias (May 04 2022 at 15:50):I was busy today, sorry for not attending
Ali Caglayan (May 17 2022 at 15:31):For the record, I've added some topics for the call tomorrow
Enrico Tassi (May 25 2022 at 09:33):It seems there is no Coq call wiki page yet. If the interested people are available, we could discuss the META.pkg business. At least on my side communication was a bit too scattered around, hard to follow.
Gaëtan Gilbert (Feb 21 2023 at 16:03):will there be enough people tomorrow or should we postpone?
Théo Zimmermann (Feb 21 2023 at 16:37):I wouldn't mind postponing again given the new ITP deadline
Emilio Jesús Gallego Arias (Feb 21 2023 at 17:06):I won't indeed be there
Matthieu Sozeau (Feb 21 2023 at 22:47):Me neither, let's postpone
Matthieu Sozeau (Mar 01 2023 at 15:40):Here's a poll to see if we can move the Coq Call to another time, please answer quickly https://evento.renater.fr/survey/coq-call-time-n3712anh
Matthieu Sozeau (Mar 01 2023 at 15:43):@Emilio Jesús Gallego Arias @Théo Zimmermann @Guillaume Melquiond @Gaëtan Gilbert @Enrico Tassi @Hugo Herbelin @Maxime Dénès @Jason Gross @Pierre Roux @nicolas tabareau @Yves Bertot ^^
Théo Zimmermann (Mar 01 2023 at 15:58):I'm responding assuming that this is for a regular schedule, not taking into account my specific availabilities (or rather non-availabilities) for next week.
Matthieu Sozeau (Mar 01 2023 at 15:58):Indeed, that's the idea
Gaëtan Gilbert (Mar 07 2023 at 17:37):so what's the result?
Matthieu Sozeau (Mar 08 2023 at 06:17):The new chosen time is Tuesdays from 4pm to 5pm. It ties with the current slot but it’s better for me as I anticipate not being available wednesdays afternoons at all for a few years. Only Jason has nos for both of them.
Matthieu Sozeau (Mar 08 2023 at 06:19):Correction: Nicolas also has a no for Wednesday at 4, it’s just me that didn’t put a no for that slot although I meant to. So Tuesday 4-5pm is the clear winner with only Jason and me having a no for it.
Matthieu Sozeau (Mar 08 2023 at 06:20):Actually, I won’t make it to today’s call, can somebody volunteer to chair it?
Enrico Tassi (Mar 08 2023 at 09:25):I can chair it
Enrico Tassi (Mar 08 2023 at 09:25):So from next week we move the call to Tuesday, same time. Am I right?
Matthieu Sozeau (Mar 08 2023 at 12:32):Yes
Emilio Jesús Gallego Arias (Mar 08 2023 at 13:49):I have a doctor now so I may be 5-10 late.
Ali Caglayan (Mar 08 2023 at 14:18):We have a call today at 16:00 Paris time right?
Pierre-Marie Pédrot (Mar 08 2023 at 14:37):It seems so.
Emilio Jesús Gallego Arias (Mar 08 2023 at 15:06):I am back
Enrico Tassi (Mar 14 2023 at 10:27):The Coq call of today was cancelled, but I cannot find a reason.
Enrico Tassi (Mar 14 2023 at 10:27):Am I missing anything?
Gaëtan Gilbert (Mar 14 2023 at 11:12):no topics
Matthieu Sozeau (Mar 14 2023 at 15:00):Yep, I saw no topics this morning, did I miss the page?
Enrico Tassi (Mar 14 2023 at 17:16):I was just expecting a message here, no pb
Matthieu Sozeau (Mar 16 2023 at 00:43):Ok, will do next time !
Matthieu Sozeau (Mar 20 2023 at 15:13):Exceptionally, I will not be able to join tomorrow, so someone else please chair this session.
Enrico Tassi (Mar 20 2023 at 15:15):On the wiki I see "No Coq Call on 2023-03-21 (no topics)"
Enrico Tassi (Mar 20 2023 at 15:16):I think there is some confusion about who is organizing the call ;-)
Matthieu Sozeau (Mar 22 2023 at 12:00):Indeed. I'll actually make a point next week to settle the rules at least on paper :)
Matthieu Sozeau (Mar 28 2023 at 14:05):In case you don't remember, the call is now :)
Matthieu Sozeau (Mar 28 2023 at 14:07):@Yves Bertot @Emilio Jesús Gallego Arias @Maxime Dénès @Jason Gross @Hugo Herbelin @Guillaume Melquiond ?
Gaëtan Gilbert (Mar 31 2023 at 14:32):The proposed coq call next week is at 5pm
Are coqide related people planning to be there?
Maxime Dénès (Mar 31 2023 at 14:58):I guess the point of the discussion is to make the position of the team on the future of CoqIDE more official, so it would be good if @Matthieu Sozeau can attend (and @Pierre-Marie Pédrot and @Théo Zimmermann who were involved in the discussion as well).
Karl Palmskog (Mar 31 2023 at 14:59):if I may ask, what is the position leaning towards?
Karl Palmskog (Mar 31 2023 at 15:06):this is not pure curiosity
Ali Caglayan (Mar 31 2023 at 17:12):Tuesday right? I think I can also attend.
Enrico Tassi (Mar 31 2023 at 18:21):My opinion is well known, CoqIDE should have never existed. Since we have not one, but two, LSP servers in the making, I think it is the right time to sink it.
Enrico Tassi (Mar 31 2023 at 18:21):I won't be able to attend, I'm on VAC
Théo Zimmermann (Apr 02 2023 at 17:11):I will be able to attend for only half an hour.
Théo Zimmermann (Apr 02 2023 at 17:13):And FTR, my own position is that CoqIDE would benefit from being split out from the Coq repository / release management process, but that we should clarify that it is volunteer-maintained and not the official IDE anymore.
Théo Zimmermann (Apr 02 2023 at 17:15):To discuss this, it would be nice to also have @Karl Palmskog (Coq-community co-admin), @Emilio Jesús Gallego Arias (who proposed the split many years ago) and @Jim Fehrle (who has taken interest in CoqIDE several years ago already). The 5pm unusual timing might actually increase the chances that Jim can attend.
Karl Palmskog (Apr 02 2023 at 17:17):5pm Tuesday? I can attend then, sure.
Matthieu Sozeau (Apr 03 2023 at 10:33):Ok for 5pm tomorrow
Matthieu Sozeau (Apr 03 2023 at 16:49):The rules discussed last week are now in place (https://github.com/coq/coq/wiki/Coq-Meetings-Organization). @nicolas tabareau proposed to be chairman for the first few meetings but I'm not sure he'll be available at this later time.
nicolas tabareau (Apr 03 2023 at 17:15):I will be there
nicolas tabareau (Apr 03 2023 at 17:18):I can chair, but we also need a secretary.
Théo Zimmermann (Apr 04 2023 at 08:09):In the end, I will be able to attend for one hour.
Michael Soegtrop (Apr 04 2023 at 08:14):Next week or the week after I would like to have a discussion on what we do about Coq on Windows - I can present the status quo in about 5 minutes and would plan for a discussion of about 10 minutes.
Michael Soegtrop (Apr 04 2023 at 08:16):We are getting into a situation where all the band-aids don't quite keep it together any more.
Théo Zimmermann (Apr 04 2023 at 08:45):Ideally, then, we could invite some opam representative to get a better idea of what the current plans actually are.
Théo Zimmermann (Apr 04 2023 at 08:46):I can try to reach out and get some representative to come once you tell me when this would happen.
Michael Soegtrop (Apr 04 2023 at 09:13):Indeed this is a good idea. I am quite flexible about the time. We could also make this an independent meeting.
nicolas tabareau (Apr 11 2023 at 13:04):It seems there is no Coq call today
Sylvain Chiron (Apr 18 2023 at 16:02):Hello. I was not available for a Coq call today, but I would like to have one tomorrow (Wednesday), to discuss things I already wanted to discuss 2 weeks ago (but we didn’t have time). Would this be possible?
Next week, I will be available at the usual time (Tuesday), and later I might not be available before July.
Théo Zimmermann (Apr 18 2023 at 20:50):Unless some specific people are interested and available to talk with you tomorrow, I think that a proper Coq Call will have to wait for next week.
Théo Zimmermann (Apr 24 2023 at 15:13):@Sylvain Chiron I've added an item to tomorrow's call about the just opened CEP on splitting CoqIDE: https://github.com/coq/ceps/pull/68. I hope that you don't mind, but this means that you will have to shrink the time you need for the topics you wanted to discuss, or reduce their number (I think the latter is a safer choice). Our Coq Call rules say that no one is supposed to take more than 30 minutes with their topics. Some of your topics are not unrelated with the new one on splitting CoqIDE anyway, so grouping them in the same call does not sound like such a bad idea.
Sylvain Chiron (Apr 24 2023 at 15:16):OK. I’m not in a hurry anyway, as I will probably not work on internationalization and Coq2latex before July. I’ve just removed the item about Coq2latex.
Sylvain Chiron (Apr 24 2023 at 15:18):I would take only 10 minutes for each topic, but people generally talk a lot…!
Your item should be the first, shouldn’t it?
Théo Zimmermann (Apr 24 2023 at 15:21):I think last time people had a lot more to say than for usual topics.
Théo Zimmermann (Apr 24 2023 at 15:21):And it will be the chair's role to cut the discussions if they take too long.
Théo Zimmermann (Apr 24 2023 at 15:22):Yes, talking about the CEP first could make sense, but it's not absolutely necessary.
Matthieu Sozeau (Apr 25 2023 at 09:06):@nicolas tabareau will you be able to chair? I will likely not be able to, so someone else should take this role this time.
Matthieu Sozeau (Apr 25 2023 at 13:58):I will not make it today, don’t wait on me
Ali Caglayan (Apr 25 2023 at 15:05):I've pushed the meeting notes. There was a lot said so I couldn't keep up with everyting but I got a general idea of discussion points.
Théo Zimmermann (Apr 25 2023 at 15:16):Thanks! It's usually fine not to cover everything in the notes but to summarize the main points instead.
Jim Fehrle (Apr 25 2023 at 15:26):On https://github.com/coq/coq/wiki/Coq-Meetings-Organization, it says to propose topics by 9 am Tuesday for a Coq call (later that day). Can we get back to 24 hours notice so those few of us not in Europe have advance notice?
Matthieu Sozeau (Apr 25 2023 at 15:35):Right, we can ask for 4pm the day before, that'd be easier on everyone actually
Matthieu Sozeau (Apr 25 2023 at 15:36):Unless someone opposes this in the coming week, I'll update it
Enrico Tassi (Apr 25 2023 at 19:18):I could not attend, but I could read the notes which are very helpful. Thanks for taking them.
Matthieu Sozeau (Apr 26 2023 at 07:04):Enrico Tassi said:
I could not attend, but I could read the notes which are very helpful. Thanks for taking them.
Same, thanks Ali!
Matthieu Sozeau (May 01 2023 at 18:15):I changed the deadline for topics, and according to those there will be no call tomorrow.
Gaëtan Gilbert (May 09 2023 at 09:30):no chairman for today?
Ali Caglayan (May 09 2023 at 10:52):I can chair today
nicolas tabareau (May 09 2023 at 13:36):I will not be there but @Pierre-Marie Pédrot can be the secretary for today
Ali Caglayan (May 09 2023 at 14:51):@Pierre-Marie Pédrot can you add the meeting notes to the wiki?
Gaëtan Gilbert (May 16 2023 at 12:39):The chairman rotation seems problematic
consequently it seems nobody gets picked
nicolas tabareau (May 16 2023 at 12:59):I picked myself
Gaëtan Gilbert (May 23 2023 at 14:02):call is now
Théo Zimmermann (May 30 2023 at 13:53):FWIW, there are quite a few of us (Maxime, Enrico, Emilio, Hugo, Jim, myself...) that are currently in another meeting (Coq UI meeting) that lasts until 5pm.
Gaëtan Gilbert (May 30 2023 at 13:56):I guess we should postpone then
will there be many missing people next week too?
Théo Zimmermann (May 30 2023 at 13:59):I will be missing too. (I could switch calls now, though.)
Gaëtan Gilbert (Jun 06 2023 at 14:06):it is now
cc @Emilio Jesús Gallego Arias I think you would be interested
Emilio Jesús Gallego Arias (Jun 06 2023 at 16:32):Thanks @Gaëtan Gilbert , I am indeed interested but had other commitements
Emilio Jesús Gallego Arias (Jun 06 2023 at 16:33):See also https://github.com/ocaml/dune/issues/3449 and https://github.com/coq/coq/issues/11542
Gaëtan Gilbert (Jul 18 2023 at 18:18):Risk of losing GitHub PR / issue data
what is this about?
Emilio Jesús Gallego Arias (Jul 18 2023 at 18:21):@Gaëtan Gilbert when github bans accounts or users delete theirs, there is some non-trivial loss of meta-data
Karl Palmskog (Jul 18 2023 at 18:22):I didn't create the item, but there is a general risk of GitHub metadata getting lost if an account with edit rights is compromised (or similar). We have an issue in Coq-community about this: https://github.com/coq-community/manifesto/issues/76 - Théo mentions coqbot could mirror metadata via GitHub's API
Emilio Jesús Gallego Arias (Jul 18 2023 at 18:22):Also mails from github can help reconstructing history, but archiving them takes lots of space.
Théo Zimmermann (Jul 18 2023 at 20:36):Théo mentions coqbot could mirror metadata via GitHub's API
It would be probably better to use a standard tool for this rather than building our own though.
Karl Palmskog (Jul 18 2023 at 20:39):the following was already linked (but expensive): https://github.com/marketplace/backhub
Gaëtan Gilbert (Aug 08 2023 at 14:03):is there a call today?
Rodolphe Lepigre (Aug 08 2023 at 14:04):I did add things to the agenda, but it does not look like it is happening (still waiting for a host).
Gaëtan Gilbert (Aug 08 2023 at 14:09):Discussing potential blockers for merging our various MRs
main blocker is probably summer holidays ;)
Rodolphe Lepigre (Aug 08 2023 at 14:09):Haha :) That is what I figured, but I was hoping to force some progress.
Théo Zimmermann (Sep 05 2023 at 13:59):I won't be available to attend today.
Théo Zimmermann (Sep 19 2023 at 13:50):Unfortunately, again, I won't be able to attend today.
Gaëtan Gilbert (Nov 10 2023 at 13:51):Can fiat crypto devs be there for the next call? fiat crypto is still not stable in CI
Théo Zimmermann (Nov 10 2023 at 16:39):FWIW, I won't be at the next coq call unfortunately, because of teaching obligations.
Jason Gross (Nov 11 2023 at 11:22):What issues are currently coming up with Fiat Crypto?
Gaëtan Gilbert (Nov 11 2023 at 12:55):couple recent ones
https://gitlab.inria.fr/coq/coq/-/jobs/3581284
https://gitlab.inria.fr/coq/coq/-/jobs/3581980
go to https://gitlab.inria.fr/coq/coq/-/pipelines?page=1&scope=all&ref=master and look at failures, easy to find more
Andres Erbsen (Nov 11 2023 at 13:57):I read that one of the files with large nsatz proofs is getting signal 9, I figure that's an out-of-memory kill. But 2387024 ko | Total Time / Peak Me is substantially below MemTotal: 3397620 kB. Does anyone else spot additional hints for what may be going on?
I might make it to the Coq call, I'll try, but it's looking to be a packed day even without it.
Jason Gross (Nov 11 2023 at 21:26):This is one of the few files that uses par:, right? I imagine the timeout is that the worker got killed (or swapped) without the main process realizing it. Note, though, that this file has not changed on the Fiat Crypto side in a very long time, so if the memkill is new this must be a regression on the Coq side, right?
Wasn't there an option that we started passing to Fiat Crypto to prevent the duplication that occurs with par: though?
Hugo Herbelin (Nov 12 2023 at 13:28):For the record, the nsatz tests also fail with a sigfault on my setting for a couple of months now. I thought it was related to a brew update but maybe it is after all related to Coq. In any case, it is possibly related to parallelism (when I add printf here and there, it stops failing).
Théo Zimmermann (Nov 13 2023 at 13:14):It looks like the Coq Call agenda for today (tomorrow) is already too full. The chair should make a choice and pick which topics will be discussed and which will be postponed.
Pierre Roux (Nov 13 2023 at 13:22):I guess you mean tomorrow, I did marked one of my subjects as less urgent and postponable
Théo Zimmermann (Nov 27 2023 at 14:42):There is no Coq Call agenda (so I guess no Coq Call) for this week. For next week, we have to decide if we keep the 2023-12-05 date as on the wiki, or if we move it to Monday as we discussed in the last Coq Call.
Hugo Herbelin (Nov 27 2023 at 15:17):Monday 4pm would be as well ok to me (thus including 2023-12-04).
Hugo Herbelin (Nov 29 2023 at 10:54):Hi, is there a decision taken about whether it'll be Monday or Tuesday? For instance, can I change the current 5/12 entry to Monday or would it raise problems?
Pierre Roux (Nov 29 2023 at 12:20):I would say yes: there was an agreement last time for Monday, and apparently no opposition here.
Pierre Roux (Nov 29 2023 at 12:45):done: https://github.com/coq/coq/wiki/Coq-Call-2023-12-04
Last updated: Nov 29 2023 at 18:01 UTC