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
Yes, the server is down :S
I get the same. I suggest using BBB instead.
Great :/
Should we move to visio.inria?
I'll create a room.
(visio.inria is discouraged right now for non-confidential meetings)
waiting for the link
https://bbb2.math.univ-paris-diderot.fr/b/the-ume-p6v
should I put this link on the wiki?
you are blazing fast
I did it already
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.
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
We're talking.
In principle, you should have sound testing when you join
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).
You can try to rejoin in headphone only...
Isn't the test about the mic?
Yeah but since you're supposed to have echo you can can also hear sound.
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!
Chromium to the rescue!
Is the link is supposed to be posted here?
I hope so
Or are we reusing the same room as last time?
Last time it did not work and we moved to BBB no?
@Théo Zimmermann can we use BBB this time as well?
Yes, let me create the room.
https://bbb2.math.univ-paris-diderot.fr/b/the-mt4-7q4
The recording of Emilio's presentation at the last Coq Call is now available at the above link.
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.
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.
OK for me if someone was to save, just saying that was not a proper "talk" but a quite improvised discussion :)
No call today, right?
Indeed, no topics, no call.
@Théo Zimmermann do we have a link for today's call?
We can reuse the same as last time: https://bbb2.math.univ-paris-diderot.fr/b/the-mt4-7q4
No Coq call today?
Indeed, there were no topics added.
@maximedenes had a topic though...
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?
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.)
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.
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?
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.
I can add an item if you like, but it should be the way you want.
I'm reading the last message in the PR.
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.
@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!
@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...
@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.
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!
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.
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.
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.
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?
Sure, it sounds interesting!
@Enrico Tassi I see that this topic was not added to today's call. Is it on purpose?
Because I failed to get in touch with them, also I did not get many answers here
Are we reusing the same link as the last time?
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
What is the room? (I'll be there in a few minutes)
https://bbb2.math.univ-paris-diderot.fr/b/the-mt4-7q4
doesn't seem to have been activated though
It seems no yet open
and now that I think about it, @Théo Zimmermann told me he wouldn't be able to assist today
so he won't be able to open the room
lol
Indeed I just saw his message tooo
we need a fallback
hum, he is the owner ;-)
shall we try visio.inria.fr or renater?
why not
Let's try renater?
@Matthieu Sozeau pelase create a link and post it here
https://rdv2.rendez-vous.renater.fr/coq-call
Sorry about this folks! :confounded:
No problem, we managed !
Shall we use BBB this time?
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.
I guess we could just go back to adding a link to the preferred room of choice
People are already connected, so let's stick to Renater for now?
Let's do BBB again next time
Yup info is a mess, still the inria link is there
Are people available for today's call considering fscd?
That's a good point @Gaëtan Gilbert , maybe we should delay?
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?
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
It does seem reasonable to postpone it
@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
Ah, okay
I guess that means I can go back to sleep :-)
Sorry for the late notice !
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)
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?
I moved them to July 8th already !
Ah, but the link was still pointing to the now-empty July 1 page. I fixed this.
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?
Sure, NP @Matthieu Sozeau , have fun!
I'll be in vacations too.
Then likely we will postpone, let's see what happens
FTR, I am in vacations this week as well.
Well, I think it makes sense to postpone then; I will update the wiki tomorrow
In view of the availability of developers, I've postponed the call to next week.
Will anyone be unavailable next week?
I will be available
Yeah, me too.
I won't be available, I'll be probably travelling
I will be available. I'd like to cover my twice-postponed item.
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.
Is the meeting on for Wednesday?
I plan on showing up, though I might be around 5 minutes late (or possibly 10, if I'm very tired)
(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)
Monday and Tuesday were holidays in France so not a lot of feedback on this one folks
But my guess is that quite a few people will be back, so we can try to have the call
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.)
Where is everybody?
We are just two right now.
I don't see you.
Or hear you.
Did you use this link to join? https://rdv2.rendez-vous.renater.fr/coq-call
I was using the link on the web page. Should that one be added to it?
https://github.com/coq/coq/pull/12259
https://x80.org/coq-coverage/vernac/g_vernac.ml.html
Please check the notes I took: https://github.com/coq/coq/wiki/Coq-Call-2020-07-15
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?
Feel free to expand the notes. I didn't want to make them too long and it was hard to decide what to select.
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.
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.
Seems we have quorum for tomorrow
I seem to have been dropped from the call due to connection issues, and rejoining does not seem to be working
@Jason Gross we are here
waiting for you
We were just about to discuss your point.
A page has been added for tomorrow; however it wasn't added to the main wiki page?
Actually that's on conflict with the break stated there
Actually that's on conflict with the break stated there
OK, so let's move it to next Wednesday.
We were supposed to hold a call today right?
apparently
if there is one, may I join?
I was waiting for a ping here :)
but indeed it was already started
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.
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.
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).
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?
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.
(I don't recall if we fixed it in MC, or worked around it in MC, or fixed in Coq...)
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.
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.
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.
(I naively promised today to @Janno that upgrading to 8.12 would be easy, luckily he's not as easily fooled as me)
I've updated the title. Any error causes the problem.
@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?
ok
Thanks to you both.
I guess the call is starting now
starting soon?
I'm running a couple minutes late, sorry
Oops, I forgot about it :frown:
me too
but it's not on renater
There are no points on the Coq Call page for today, so there will be no call this afternoon.
call today?
@Karl Palmskog Did you see my e-mail suggesting to join the call today?
@Théo Zimmermann ah, is the call now? I can join now
Yes :smile:
Thanks for your participation! This was really useful.
I'm on vacations for the next two weeks, so won't be able to attend the calls.
call in 30min
Why am I alone in the meeting?
same here?
Why am I too? :)
I am too
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).
I think we should postpone to Thursday
@Erik Martin-Dorel would that be ok with you?
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?
No, that would be too late for me. What about Friday?
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 ?
Friday 15.00 would work for me. Let's see what the others' availability are.
@Théo Zimmermann can one ping the stream by Cc "@all"
?
There are lots of people subscribed to the stream (252). Let's just ping the usual suspects.
@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?
ok
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)
Sorry I'll have 5' delay for the Coq call... but I'll be available till 16:00
ok
for those who didn't notice: the call is starting now, not in 1h
Sorry, I had to leave to attend a talk.
@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.
Thanks, my mistake
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.
I won't be able to attend, I'm afraid.
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
Postponing to next week would be fine. I will update the web page.
Call is starting now
There will be no call today, I updated the wiki page.
looks like nothing this week
Didn't something get postponed last week though?
Théo had a point about locality attributes that was not adressed IIRC. @Théo Zimmermann are you available to talk about it?
Yes, I'm available.
And there was a second point by @Enrico Tassi which was not discussed about the minimal OCaml version to require for 8.14.
Ok, let's move them both to today's page
@Enrico Tassi will you join us today?
Sure, 1 minute
I checked and ocamldebug is still dead slow on 4.11.1 btw
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
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!
I can take notes
Thanks !
I see no page but we have the dune update to discuss, right?
Cc @Emilio Jesús Gallego Arias
I'm still on vacations, so don't wait for me :)
Oh I thought we had updated the page, indeed it would be good if we could chat a bit about the build system
Did anyone take notes yesterday?
@Emilio Jesús Gallego Arias said he would.
I took notes for the first part that was on the agenda, the rest of the discussion maybe someone else is better to summarize?
@Enrico Tassi I ping you as indeed the discussion needs a bit more feedback
once the notes are in the wiki I mean
@Enrico Tassi here they are https://github.com/coq/coq/wiki/Coq-Call-2021-03-03
not sure what more can I add to the notes, please review and let me know what you think
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
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.
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.
code in vscoq-lsp that was already solved in sername by Karl
can you elaborate?
can you elaborate?
I don't recall the details, was some parsing / tokenization stuff, that Maxime was doing then by chance was already done by Karl
so indeed these kind of common requirements for the platform can be better identified
This is the thread https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs.20.26.20plugin.20devs/topic/Parsing.20interface/near/199297523
bit late to schedule a call @Pierre-Marie Pédrot
that's fine if we don't discuss this today
it's long term stuff for which I am seeking wise advice
I have many woes with libobject too , so indeed even if it is just some chat about options would be very helpful
Let's have it then
@Arthur Charguéraud It's a bit late to add that many topics to the Coq Call, don't you think?
@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.
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.
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.
sorry if my comment on coq name was inappropriate, i'm probably lacking context here
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.
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 :)
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.
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.
@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.
Ah, okay, I'll postpone to next week
Updated on the wiki
@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.
I'm on vacations and won't be available for the Coq Call this week.
Is the call happening? I get that the call hasn't started yet
Tomorrow (Thursday) stats a long week-end for most French people, so it's likely that there are not many people around.
(I'd myself prefer postponing the call, but I can attend if we maintain it.)
There is a topic by Jim
I'd also like some advice for the opaque-def-no-body patch
hm, for this kind of stuff I prefer having a one-to-one conversation
isn't the call in 30' ?
yup
I get that the call hasn't started yet
Oops, I was off by an hour
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.
Jim just committed, so he obviously plans on attending.
Postponing now would not be nice given that he has woken up early for this.
ok
@Emilio Jesús Gallego Arias are you joining as well?
There is one point to discuss on today's Coq Call: https://github.com/coq/coq/wiki/Coq-Call-2021-05-19
I updated the main page
Sorry I was on the road and couldn't login to signal my abscence
the call approaches
So it seems that rendez-vous is down?
is it?
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.
I'll share a Zoom link
https://univ-nantes-fr.zoom.us/j/3070423803
no zoom please
it regularly bugs for me
Ahem
Let's do https://whereby.com/mattam82
Hi folks, I see no call today, right?
Yep, no call today
No call today either, I guess everyone is busy finishing his/her PRs ;)
Related to tomorrow's call https://www.theregister.com/2021/06/15/coq_programming_language_change/
only 106 comments XD
Thanks for the pointer.
Théo Zimmermann said:
Thanks for the pointer.
I assume Théo they didn't contact you, right?
As the reporter writes "according to Théo" XD
They didn't. They cite what I wrote in the wiki.
The article is a nice summary!
@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.
I forgot, sorry.
Is next call really July 14th? cc @Emilio Jesús Gallego Arias
(who made the page)
Probably a silly mistake. Let's move it to the week after.
We said we wanted to move it the 13th.
After that I'll be on vacations, and I expect I'm not the only one :)
Ah OK.
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.
Yup, we said we'd do the 13th, sorry we didn't move the page
By the way I added CEP #50 to the coq call so we can discuss it if that's alright.
@Théo Winterhalter should probably join for this :)
I cannot guarantee I can join as I am starting my vacations today.
Ok, enjoy!
Thanks. If I can make time I'll try to be there.
Reminder the call is going on today, not tomorrow
Hi folks, I happen to have a doctor before the call, I may be late tomorrow
Hi folks, it seems I'm super late on another call, which is critical :S
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
@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)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?
I think @Emilio Jesús Gallego Arias wanted to chat about the old and new invariants of the kernel
I don't know if it's super interesting for everybody, we can turn that into a private discussion with the relevant people
I do need input from @Matthieu Sozeau about MetaCoq though
I am OK both chatting online of sending my questions on the issue tracker
I won't attend, but if someone writes these invariants down I'd be happy to read them
easy: it's the opposite of MetaCoq
Oh I see, the two invariants are A and not(A). Its a good start ;-)
@Pierre-Marie Pédrot We can have a quick chat the three of us at the Coq Call, can't hurt
fine
I've added a page for tomorrow since there are a few things I want to discuss
If you want feedback on PRs you shouldn't leave them as draft
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”
Should we postpone today's call? @Emilio Jesús Gallego Arias WDYT? You were the one who added the single item on the agenda.
Sure, let's postpone then; tho we should try to postpone the day before at the very least so people have time to react
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!
I will be around if anyone was planning to attend and would like to discuss stuff I could help with
Sorry for the late notice indeed
Feel free to continue posting your ideas on automatically reporting warnings in CI in https://github.com/coq/bot/issues/169.
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.
I won't likely be available tomorrow [tho I'll try, but likely not online at that time]
So if you need me for any topic, it must be moved to next week, sorry
I'd be happy to discuss on the issues too
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
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.
Following your note on the wiki page, I've opened a PR updating the release documentation: https://github.com/coq/coq/pull/15080
having some browser issues, trying to get it fixed
@Enrico Tassi Francois can make it next week, you can too then?
Yes I'll do my best
Hi folks very unfortunately due to travel changes I won't be able to make the call today
I may, I dunno, I'll be on a train, so I'll try
François is coming so please let him know if there is some other problem
I'm getting a "wait for the host to start the meeting" message
0e3147b9-1858-4e46-9bd6-fab5160d0d72.png
on https://rdv2.rendez-vous.renater.fr/coq-call ? works for me
Strange, I guess jitsi doesn't automatically let me in when the meeting starts if I join before the host?
Didn't manage to make it worry folks
What Francois able to make it too? I just saw a message from him telling me he had some trouble
Yes he was there.
See the notes that Enrico has added in the header of PR https://github.com/coq/coq/pull/15220.
What ended up being discussed in today's call?
A lot of stuff
For the name change, we discussed whether we should provide/update a roadmap
For the Feb 2022 WG, a preliminar date is 14 Feb and that week, but still too many variables, so not fixed
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
Holiday break I don't remember
Also Ali asked about SerAPI and Coq's CI, I answered with my point of view
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
there are like basic things you want when buidling a UI
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
We also discussed moving forward with the inductive inductive branch briefly at the end
We can def break some stuff up in there and implement finished parts
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.
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).
Sorry I forgot to take notes, but Emilio’s summary is right. Indeed next call is in January
The next call is January 5?
only if someone adds a topic
Done.
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.
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?
No worries @Matthieu Sozeau I can take the notes
I’m on holidays this week, can someone else act as chair for the call ?
It is very bad timing for me for the call too
due to inria CR deadline being next Tue
I'd appreciate if non urgent topics of my interest could be discussed next week
I can act as chair if needed
I will attend, and I can take notes.
@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)
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
indeed they recommend to avoid it at all costs, however that requires a protocol which act as a state machine
jscoq uses this approach and works well, but I'm not sure if it can be done without rewriting the xml protocol
I will maybe say more on the UI meeting
So are there notes of the meeting today?
I have not posted them yet, I'll do it later today, or tomorrow
Notes are online, all people attending are welcome to improve them
No Coq call today, correct?
Correct
not a lot of calls recently
too busy wreaking havoc in universe internals to chat about it :nuclear:
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?
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.
@Michael Soegtrop I don't understand what you mean by "different picks use different OCaml versions"
Yup 4.13 is good, specially for those on newer mac
@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.
See (https://github.com/coq/platform/blob/main/README.md)
Ah, I see thanks. I didn't know you supported multiple Coq versions per platform
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.
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)
Do we get a call today? We still haven't discussed the OCaml version bump.
(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)
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
The link gets created by whoever wants the call to happen (usually not that late, but well...)
Is it too late to make it now?
we can do anything we want, even have a visio right now instead of waiting for the usual time if we decide to
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.
let's get a call then
https://github.com/coq/coq/wiki/Coq-Call-2022-04-06
@Jason Gross I'm on VAC today, I may be able to chat a little, but not join the call
Next week does not work either for me, but the following one should be fine
So IMO the best is to chat asynchronously if the issue if pressing for you
the ocaml version bump has been discussed regularly but we never converged
I think we need a synchronous decision for this one
The issue is not pressing, let's postpone to the week after next?
fine fine
I might not be around though
so do we cancel this short-lived call already?
I don't think they are talking about cancelling this call, just what Jason wanted to talk about.
Yeah, I'm just talking about postponing the OCAMLPATH / COQBIN issue
(sorry for the ambiguity)
(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)
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)
won't be there either
Sorry @Jim Fehrle , but I don't think I'll make it either.
Let's postpone, to avoid having the discussions twice, then
It doesn't look to me like @Jim Fehrle has seen these messages. It's unfortunate that the Coq Call page was not modified.
Yes, let's postpone, I don't be available today and next week either.
Can someone update the wiki?
I'll do it
OK, see you guys next week, then.
@Matthieu Sozeau Shouldn't the postponed topics be addressed first in the Coq Call and agenda for April 20?
will there be any more people available next week? it's still easter holiday season
I'll be on vacations
I won't be available either
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.
I won't be available.
It looks like lots of developers won't be there (I'm not sure I can attend either), so it looks safer to postpone.
Yes, let's postpone.
Ok, let's postpone again, I'll put your items on top @Jim Fehrle
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
I know that Jason will go, and I think I won't.
allo
Nobody's here today?
As for myself, I'm in a train with a crappy connection.
I was busy today, sorry for not attending
For the record, I've added some topics for the call tomorrow
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.
will there be enough people tomorrow or should we postpone?
I wouldn't mind postponing again given the new ITP deadline
I won't indeed be there
Me neither, let's postpone
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
@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 ^^
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.
Indeed, that's the idea
so what's the result?
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.
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.
Actually, I won’t make it to today’s call, can somebody volunteer to chair it?
I can chair it
So from next week we move the call to Tuesday, same time. Am I right?
Yes
I have a doctor now so I may be 5-10 late.
We have a call today at 16:00 Paris time right?
It seems so.
I am back
The Coq call of today was cancelled, but I cannot find a reason.
Am I missing anything?
no topics
Yep, I saw no topics this morning, did I miss the page?
I was just expecting a message here, no pb
Ok, will do next time !
Exceptionally, I will not be able to join tomorrow, so someone else please chair this session.
On the wiki I see "No Coq Call on 2023-03-21 (no topics)"
I think there is some confusion about who is organizing the call ;-)
Indeed. I'll actually make a point next week to settle the rules at least on paper :)
In case you don't remember, the call is now :)
@Yves Bertot @Emilio Jesús Gallego Arias @Maxime Dénès @Jason Gross @Hugo Herbelin @Guillaume Melquiond ?
The proposed coq call next week is at 5pm
Are coqide related people planning to be there?
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).
if I may ask, what is the position leaning towards?
this is not pure curiosity
Tuesday right? I think I can also attend.
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.
I won't be able to attend, I'm on VAC
I will be able to attend for only half an hour.
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.
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.
5pm Tuesday? I can attend then, sure.
Ok for 5pm tomorrow
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.
I will be there
I can chair, but we also need a secretary.
In the end, I will be able to attend for one hour.
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.
We are getting into a situation where all the band-aids don't quite keep it together any more.
Ideally, then, we could invite some opam representative to get a better idea of what the current plans actually are.
I can try to reach out and get some representative to come once you tell me when this would happen.
Indeed this is a good idea. I am quite flexible about the time. We could also make this an independent meeting.
It seems there is no Coq call today
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.
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.
@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.
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.
I would take only 10 minutes for each topic, but people generally talk a lot…!
Your item should be the first, shouldn’t it?
I think last time people had a lot more to say than for usual topics.
And it will be the chair's role to cut the discussions if they take too long.
Yes, talking about the CEP first could make sense, but it's not absolutely necessary.
@nicolas tabareau will you be able to chair? I will likely not be able to, so someone else should take this role this time.
I will not make it today, don’t wait on me
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.
Thanks! It's usually fine not to cover everything in the notes but to summarize the main points instead.
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?
Right, we can ask for 4pm the day before, that'd be easier on everyone actually
Unless someone opposes this in the coming week, I'll update it
I could not attend, but I could read the notes which are very helpful. Thanks for taking them.
Enrico Tassi said:
I could not attend, but I could read the notes which are very helpful. Thanks for taking them.
Same, thanks Ali!
I changed the deadline for topics, and according to those there will be no call tomorrow.
no chairman for today?
I can chair today
I will not be there but @Pierre-Marie Pédrot can be the secretary for today
@Pierre-Marie Pédrot can you add the meeting notes to the wiki?
The chairman rotation seems problematic
consequently it seems nobody gets picked
I picked myself
call is now
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.
I guess we should postpone then
will there be many missing people next week too?
I will be missing too. (I could switch calls now, though.)
Last updated: Jun 05 2023 at 10:01 UTC