Stream: Coq devs & plugin devs

Topic: coq call


view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (May 13 2020 at 14:01):

Yes, the server is down :S

view this post on Zulip Théo Zimmermann (May 13 2020 at 14:01):

I get the same. I suggest using BBB instead.

view this post on Zulip Pierre-Marie Pédrot (May 13 2020 at 14:01):

Great :/

view this post on Zulip Emilio Jesús Gallego Arias (May 13 2020 at 14:01):

Should we move to visio.inria?

view this post on Zulip Théo Zimmermann (May 13 2020 at 14:02):

I'll create a room.

view this post on Zulip Théo Zimmermann (May 13 2020 at 14:02):

(visio.inria is discouraged right now for non-confidential meetings)

view this post on Zulip Enrico Tassi (May 13 2020 at 14:02):

waiting for the link

view this post on Zulip Théo Zimmermann (May 13 2020 at 14:02):

https://bbb2.math.univ-paris-diderot.fr/b/the-ume-p6v

view this post on Zulip Enrico Tassi (May 13 2020 at 14:03):

should I put this link on the wiki?

view this post on Zulip Enrico Tassi (May 13 2020 at 14:03):

you are blazing fast

view this post on Zulip Théo Zimmermann (May 13 2020 at 14:03):

I did it already

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (May 13 2020 at 14:10):

We're talking.

view this post on Zulip Théo Zimmermann (May 13 2020 at 14:10):

In principle, you should have sound testing when you join

view this post on Zulip 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).

view this post on Zulip Théo Zimmermann (May 13 2020 at 14:12):

You can try to rejoin in headphone only...

view this post on Zulip Gaëtan Gilbert (May 13 2020 at 14:12):

Isn't the test about the mic?

view this post on Zulip Théo Zimmermann (May 13 2020 at 14:13):

Yeah but since you're supposed to have echo you can can also hear sound.

view this post on Zulip 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!

view this post on Zulip Janno (May 13 2020 at 14:23):

Chromium to the rescue!

view this post on Zulip Pierre-Marie Pédrot (May 20 2020 at 13:56):

Is the link is supposed to be posted here?

view this post on Zulip Enrico Tassi (May 20 2020 at 13:57):

I hope so

view this post on Zulip Pierre-Marie Pédrot (May 20 2020 at 13:57):

Or are we reusing the same room as last time?

view this post on Zulip Enrico Tassi (May 20 2020 at 13:57):

Last time it did not work and we moved to BBB no?

view this post on Zulip Enrico Tassi (May 20 2020 at 13:58):

@Théo Zimmermann can we use BBB this time as well?

view this post on Zulip Théo Zimmermann (May 20 2020 at 13:58):

Yes, let me create the room.

view this post on Zulip Théo Zimmermann (May 20 2020 at 13:59):

https://bbb2.math.univ-paris-diderot.fr/b/the-mt4-7q4

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 :)

view this post on Zulip Hugo Herbelin (May 27 2020 at 13:40):

No call today, right?

view this post on Zulip Théo Zimmermann (May 27 2020 at 13:42):

Indeed, no topics, no call.

view this post on Zulip Maxime Dénès (Jun 03 2020 at 13:58):

@Théo Zimmermann do we have a link for today's call?

view this post on Zulip 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

view this post on Zulip Maxime Dénès (Jun 10 2020 at 11:40):

No Coq call today?

view this post on Zulip Matthieu Sozeau (Jun 10 2020 at 12:49):

Indeed, there were no topics added.

view this post on Zulip Hugo Herbelin (Jun 10 2020 at 13:55):

@maximedenes had a topic though...

view this post on Zulip 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?

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Maxime Dénès (Jun 10 2020 at 16:04):

I'm reading the last message in the PR.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Maxime Dénès (Jun 11 2020 at 09:11):

Sure, it sounds interesting!

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 13:57):

Are we reusing the same link as the last time?

view this post on Zulip 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

view this post on Zulip Janno (Jun 17 2020 at 14:00):

What is the room? (I'll be there in a few minutes)

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 14:03):

https://bbb2.math.univ-paris-diderot.fr/b/the-mt4-7q4

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 14:03):

doesn't seem to have been activated though

view this post on Zulip Enrico Tassi (Jun 17 2020 at 14:03):

It seems no yet open

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 14:04):

so he won't be able to open the room

view this post on Zulip Maxime Dénès (Jun 17 2020 at 14:04):

lol

view this post on Zulip Matthieu Sozeau (Jun 17 2020 at 14:04):

Indeed I just saw his message tooo

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 14:04):

we need a fallback

view this post on Zulip Enrico Tassi (Jun 17 2020 at 14:04):

hum, he is the owner ;-)
shall we try visio.inria.fr or renater?

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 14:04):

why not

view this post on Zulip Matthieu Sozeau (Jun 17 2020 at 14:04):

Let's try renater?

view this post on Zulip Enrico Tassi (Jun 17 2020 at 14:05):

@Matthieu Sozeau pelase create a link and post it here

view this post on Zulip Matthieu Sozeau (Jun 17 2020 at 14:05):

https://rdv2.rendez-vous.renater.fr/coq-call

view this post on Zulip Théo Zimmermann (Jun 17 2020 at 15:52):

Sorry about this folks! :confounded:

view this post on Zulip Matthieu Sozeau (Jun 17 2020 at 18:25):

No problem, we managed !

view this post on Zulip Enrico Tassi (Jun 24 2020 at 13:51):

Shall we use BBB this time?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Jun 24 2020 at 14:00):

People are already connected, so let's stick to Renater for now?

view this post on Zulip Matthieu Sozeau (Jun 24 2020 at 14:00):

Let's do BBB again next time

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2020 at 14:04):

Yup info is a mess, still the inria link is there

view this post on Zulip Gaëtan Gilbert (Jul 01 2020 at 09:58):

Are people available for today's call considering fscd?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 01 2020 at 10:09):

That's a good point @Gaëtan Gilbert , maybe we should delay?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Cyril Cohen (Jul 01 2020 at 13:13):

It does seem reasonable to postpone it

view this post on Zulip 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

view this post on Zulip Jason Gross (Jul 01 2020 at 14:04):

Ah, okay

view this post on Zulip Jason Gross (Jul 01 2020 at 14:04):

I guess that means I can go back to sleep :-)

view this post on Zulip Matthieu Sozeau (Jul 01 2020 at 14:04):

Sorry for the late notice !

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip Matthieu Sozeau (Jul 01 2020 at 15:09):

I moved them to July 8th already !

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 07 2020 at 18:57):

Sure, NP @Matthieu Sozeau , have fun!

view this post on Zulip Maxime Dénès (Jul 07 2020 at 19:41):

I'll be in vacations too.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 07 2020 at 20:29):

Then likely we will postpone, let's see what happens

view this post on Zulip Pierre-Marie Pédrot (Jul 07 2020 at 22:06):

FTR, I am in vacations this week as well.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Jul 09 2020 at 09:41):

Will anyone be unavailable next week?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 09 2020 at 12:32):

I will be available

view this post on Zulip Théo Zimmermann (Jul 09 2020 at 12:44):

Yeah, me too.

view this post on Zulip Enrico Tassi (Jul 09 2020 at 15:04):

I won't be available, I'll be probably travelling

view this post on Zulip Jim Fehrle (Jul 10 2020 at 15:39):

I will be available. I'd like to cover my twice-postponed item.

view this post on Zulip 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.

view this post on Zulip Jim Fehrle (Jul 14 2020 at 21:27):

Is the meeting on for Wednesday?

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.)

view this post on Zulip Théo Zimmermann (Jul 15 2020 at 14:05):

Where is everybody?

view this post on Zulip Théo Zimmermann (Jul 15 2020 at 14:05):

We are just two right now.

view this post on Zulip Jim Fehrle (Jul 15 2020 at 14:06):

I don't see you.

view this post on Zulip Jim Fehrle (Jul 15 2020 at 14:06):

Or hear you.

view this post on Zulip Théo Zimmermann (Jul 15 2020 at 14:07):

Did you use this link to join? https://rdv2.rendez-vous.renater.fr/coq-call

view this post on Zulip Jim Fehrle (Jul 15 2020 at 14:14):

I was using the link on the web page. Should that one be added to it?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 15 2020 at 14:21):

https://github.com/coq/coq/pull/12259

view this post on Zulip Emilio Jesús Gallego Arias (Jul 15 2020 at 14:34):

https://x80.org/coq-coverage/vernac/g_vernac.ml.html

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 21 2020 at 14:01):

Seems we have quorum for tomorrow

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jul 22 2020 at 14:40):

@Jason Gross we are here

view this post on Zulip Emilio Jesús Gallego Arias (Jul 22 2020 at 14:40):

waiting for you

view this post on Zulip Théo Zimmermann (Jul 22 2020 at 14:40):

We were just about to discuss your point.

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Aug 25 2020 at 12:57):

Actually that's on conflict with the break stated there

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 02 2020 at 14:18):

We were supposed to hold a call today right?

view this post on Zulip Gaëtan Gilbert (Sep 02 2020 at 14:22):

apparently

view this post on Zulip Karl Palmskog (Sep 02 2020 at 14:23):

if there is one, may I join?

view this post on Zulip Emilio Jesús Gallego Arias (Sep 02 2020 at 14:23):

I was waiting for a ping here :)

view this post on Zulip Emilio Jesús Gallego Arias (Sep 02 2020 at 14:23):

but indeed it was already started

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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...)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Enrico Tassi (Sep 09 2020 at 05:22):

I've updated the title. Any error causes the problem.

view this post on Zulip 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?

view this post on Zulip Enrico Tassi (Sep 09 2020 at 07:12):

ok

view this post on Zulip Paolo Giarrusso (Sep 09 2020 at 08:46):

Thanks to you both.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 09 2020 at 14:01):

I guess the call is starting now

view this post on Zulip Gaëtan Gilbert (Sep 23 2020 at 13:58):

starting soon?

view this post on Zulip Jason Gross (Sep 23 2020 at 14:00):

I'm running a couple minutes late, sorry

view this post on Zulip Théo Zimmermann (Sep 23 2020 at 15:23):

Oops, I forgot about it :frown:

view this post on Zulip Enrico Tassi (Sep 23 2020 at 15:40):

me too

view this post on Zulip Enrico Tassi (Sep 23 2020 at 15:40):

but it's not on renater

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Oct 07 2020 at 13:56):

call today?

view this post on Zulip Théo Zimmermann (Oct 07 2020 at 14:04):

@Karl Palmskog Did you see my e-mail suggesting to join the call today?

view this post on Zulip Karl Palmskog (Oct 07 2020 at 14:08):

@Théo Zimmermann ah, is the call now? I can join now

view this post on Zulip Théo Zimmermann (Oct 07 2020 at 14:08):

Yes :smile:

view this post on Zulip Théo Zimmermann (Oct 07 2020 at 14:53):

Thanks for your participation! This was really useful.

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Nov 04 2020 at 14:33):

call in 30min

view this post on Zulip Théo Zimmermann (Nov 04 2020 at 15:02):

Why am I alone in the meeting?

view this post on Zulip Pierre-Marie Pédrot (Nov 04 2020 at 15:03):

same here?

view this post on Zulip Matthieu Sozeau (Nov 04 2020 at 15:03):

Why am I too? :)

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2020 at 15:03):

I am too

view this post on Zulip 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).

view this post on Zulip Matthieu Sozeau (Nov 10 2020 at 09:23):

I think we should postpone to Thursday

view this post on Zulip Matthieu Sozeau (Nov 10 2020 at 09:23):

@Erik Martin-Dorel would that be ok with you?

view this post on Zulip 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?

view this post on Zulip Théo Zimmermann (Nov 10 2020 at 10:33):

No, that would be too late for me. What about Friday?

view this post on Zulip 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 ?

view this post on Zulip Théo Zimmermann (Nov 10 2020 at 10:38):

Friday 15.00 would work for me. Let's see what the others' availability are.

view this post on Zulip Erik Martin-Dorel (Nov 10 2020 at 10:40):

@Théo Zimmermann can one ping the stream by Cc "@all" ?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Enrico Tassi (Nov 10 2020 at 11:01):

ok

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Nov 13 2020 at 14:01):

ok

view this post on Zulip Gaëtan Gilbert (Nov 13 2020 at 14:05):

for those who didn't notice: the call is starting now, not in 1h

view this post on Zulip Théo Zimmermann (Dec 09 2020 at 16:00):

Sorry, I had to leave to attend a talk.

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Dec 09 2020 at 17:34):

Thanks, my mistake

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Jan 05 2021 at 17:43):

I won't be able to attend, I'm afraid.

view this post on Zulip 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

view this post on Zulip Jim Fehrle (Jan 05 2021 at 19:53):

Postponing to next week would be fine. I will update the web page.

view this post on Zulip Matthieu Sozeau (Jan 13 2021 at 15:02):

Call is starting now

view this post on Zulip Matthieu Sozeau (Jan 20 2021 at 13:20):

There will be no call today, I updated the wiki page.

view this post on Zulip Gaëtan Gilbert (Feb 03 2021 at 11:45):

looks like nothing this week

view this post on Zulip Gaëtan Gilbert (Feb 03 2021 at 11:46):

Didn't something get postponed last week though?

view this post on Zulip 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?

view this post on Zulip Théo Zimmermann (Feb 03 2021 at 14:08):

Yes, I'm available.

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Feb 03 2021 at 14:09):

Ok, let's move them both to today's page

view this post on Zulip Matthieu Sozeau (Feb 03 2021 at 15:02):

@Enrico Tassi will you join us today?

view this post on Zulip Enrico Tassi (Feb 03 2021 at 15:02):

Sure, 1 minute

view this post on Zulip Gaëtan Gilbert (Feb 04 2021 at 10:02):

I checked and ocamldebug is still dead slow on 4.11.1 btw

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip Enrico Tassi (Feb 17 2021 at 14:00):

I can take notes

view this post on Zulip Matthieu Sozeau (Feb 17 2021 at 14:08):

Thanks !

view this post on Zulip Enrico Tassi (Feb 24 2021 at 08:35):

I see no page but we have the dune update to discuss, right?

view this post on Zulip Enrico Tassi (Feb 24 2021 at 08:35):

Cc @Emilio Jesús Gallego Arias

view this post on Zulip Matthieu Sozeau (Feb 24 2021 at 14:01):

I'm still on vacations, so don't wait for me :)

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Mar 04 2021 at 07:23):

Did anyone take notes yesterday?

view this post on Zulip Théo Zimmermann (Mar 04 2021 at 08:30):

@Emilio Jesús Gallego Arias said he would.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 04 2021 at 14:12):

once the notes are in the wiki I mean

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Mar 12 2021 at 14:38):

code in vscoq-lsp that was already solved in sername by Karl

can you elaborate?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 12 2021 at 14:42):

can you elaborate?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Mar 31 2021 at 11:26):

bit late to schedule a call @Pierre-Marie Pédrot

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 11:27):

that's fine if we don't discuss this today

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 11:28):

it's long term stuff for which I am seeking wise advice

view this post on Zulip 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

view this post on Zulip Matthieu Sozeau (Mar 31 2021 at 12:33):

Let's have it then

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Arthur Charguéraud (Apr 07 2021 at 07:58):

sorry if my comment on coq name was inappropriate, i'm probably lacking context here

view this post on Zulip 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.

view this post on Zulip 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 :)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Jason Gross (Apr 14 2021 at 12:07):

Ah, okay, I'll postpone to next week

view this post on Zulip Théo Zimmermann (Apr 14 2021 at 12:39):

Updated on the wiki

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (May 10 2021 at 07:29):

I'm on vacations and won't be available for the Coq Call this week.

view this post on Zulip Jason Gross (May 12 2021 at 13:12):

Is the call happening? I get that the call hasn't started yet

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip Enrico Tassi (May 12 2021 at 13:30):

There is a topic by Jim

view this post on Zulip Enrico Tassi (May 12 2021 at 13:30):

I'd also like some advice for the opaque-def-no-body patch

view this post on Zulip Pierre-Marie Pédrot (May 12 2021 at 13:30):

hm, for this kind of stuff I prefer having a one-to-one conversation

view this post on Zulip Enrico Tassi (May 12 2021 at 13:30):

isn't the call in 30' ?

view this post on Zulip Pierre-Marie Pédrot (May 12 2021 at 13:31):

yup

view this post on Zulip Enrico Tassi (May 12 2021 at 13:31):

I get that the call hasn't started yet

view this post on Zulip Jason Gross (May 12 2021 at 13:38):

Oops, I was off by an hour

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (May 12 2021 at 13:57):

Jim just committed, so he obviously plans on attending.

view this post on Zulip Théo Zimmermann (May 12 2021 at 13:58):

Postponing now would not be nice given that he has woken up early for this.

view this post on Zulip Pierre-Marie Pédrot (May 12 2021 at 14:00):

ok

view this post on Zulip Théo Zimmermann (May 12 2021 at 14:04):

@Emilio Jesús Gallego Arias are you joining as well?

view this post on Zulip 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

view this post on Zulip Matthieu Sozeau (May 19 2021 at 13:35):

I updated the main page

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (May 26 2021 at 13:57):

the call approaches

view this post on Zulip Théo Zimmermann (May 26 2021 at 14:00):

So it seems that rendez-vous is down?

view this post on Zulip Gaëtan Gilbert (May 26 2021 at 14:01):

is it?

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (May 26 2021 at 14:01):

I'll share a Zoom link

view this post on Zulip Matthieu Sozeau (May 26 2021 at 14:02):

https://univ-nantes-fr.zoom.us/j/3070423803

view this post on Zulip Gaëtan Gilbert (May 26 2021 at 14:03):

no zoom please

view this post on Zulip Gaëtan Gilbert (May 26 2021 at 14:03):

it regularly bugs for me

view this post on Zulip Théo Zimmermann (May 26 2021 at 14:03):

Ahem

view this post on Zulip Matthieu Sozeau (May 26 2021 at 14:04):

Let's do https://whereby.com/mattam82

view this post on Zulip Emilio Jesús Gallego Arias (Jun 02 2021 at 14:02):

Hi folks, I see no call today, right?

view this post on Zulip Matthieu Sozeau (Jun 02 2021 at 14:02):

Yep, no call today

view this post on Zulip Matthieu Sozeau (Jun 09 2021 at 13:25):

No call today either, I guess everyone is busy finishing his/her PRs ;)

view this post on Zulip 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/

view this post on Zulip Emilio Jesús Gallego Arias (Jun 15 2021 at 15:30):

only 106 comments XD

view this post on Zulip Théo Zimmermann (Jun 15 2021 at 15:45):

Thanks for the pointer.

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 15 2021 at 18:05):

As the reporter writes "according to Théo" XD

view this post on Zulip Théo Zimmermann (Jun 15 2021 at 21:07):

They didn't. They cite what I wrote in the wiki.

view this post on Zulip Matthieu Sozeau (Jun 16 2021 at 08:59):

The article is a nice summary!

view this post on Zulip 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.

view this post on Zulip Hugo Herbelin (Jul 06 2021 at 08:31):

I forgot, sorry.

view this post on Zulip Gaëtan Gilbert (Jul 08 2021 at 15:27):

Is next call really July 14th? cc @Emilio Jesús Gallego Arias

view this post on Zulip Gaëtan Gilbert (Jul 08 2021 at 15:27):

(who made the page)

view this post on Zulip Théo Zimmermann (Jul 08 2021 at 15:49):

Probably a silly mistake. Let's move it to the week after.

view this post on Zulip Matthieu Sozeau (Jul 08 2021 at 15:55):

We said we wanted to move it the 13th.

view this post on Zulip Matthieu Sozeau (Jul 08 2021 at 15:55):

After that I'll be on vacations, and I expect I'm not the only one :)

view this post on Zulip Théo Zimmermann (Jul 08 2021 at 17:18):

Ah OK.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Jul 12 2021 at 08:53):

@Théo Winterhalter should probably join for this :)

view this post on Zulip Théo Winterhalter (Jul 12 2021 at 09:25):

I cannot guarantee I can join as I am starting my vacations today.

view this post on Zulip Matthieu Sozeau (Jul 12 2021 at 09:25):

Ok, enjoy!

view this post on Zulip Théo Winterhalter (Jul 12 2021 at 09:27):

Thanks. If I can make time I'll try to be there.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 13 2021 at 14:32):

Reminder the call is going on today, not tomorrow

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 13:43):

I do need input from @Matthieu Sozeau about MetaCoq though

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 13:50):

easy: it's the opposite of MetaCoq

view this post on Zulip Enrico Tassi (Sep 22 2021 at 13:51):

Oh I see, the two invariants are A and not(A). Its a good start ;-)

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 13:54):

fine

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Sep 28 2021 at 12:06):

If you want feedback on PRs you shouldn't leave them as draft

view this post on Zulip 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”

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip Matthieu Sozeau (Oct 12 2021 at 12:17):

Sorry for the late notice indeed

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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]

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 27 2021 at 00:52):

I'd be happy to discuss on the issues too

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Nov 10 2021 at 15:14):

having some browser issues, trying to get it fixed

view this post on Zulip Emilio Jesús Gallego Arias (Dec 03 2021 at 13:00):

@Enrico Tassi Francois can make it next week, you can too then?

view this post on Zulip Enrico Tassi (Dec 03 2021 at 13:39):

Yes I'll do my best

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Jason Gross (Dec 08 2021 at 15:03):

I'm getting a "wait for the host to start the meeting" message

view this post on Zulip Jason Gross (Dec 08 2021 at 15:03):

0e3147b9-1858-4e46-9bd6-fab5160d0d72.png

view this post on Zulip Gaëtan Gilbert (Dec 08 2021 at 15:05):

on https://rdv2.rendez-vous.renater.fr/coq-call ? works for me

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Dec 08 2021 at 16:15):

Didn't manage to make it worry folks

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Dec 08 2021 at 16:22):

Yes he was there.

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Dec 15 2021 at 18:46):

What ended up being discussed in today's call?

view this post on Zulip Emilio Jesús Gallego Arias (Dec 15 2021 at 23:28):

A lot of stuff

view this post on Zulip Emilio Jesús Gallego Arias (Dec 15 2021 at 23:28):

For the name change, we discussed whether we should provide/update a roadmap

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 15 2021 at 23:29):

Holiday break I don't remember

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 15 2021 at 23:30):

there are like basic things you want when buidling a UI

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Dec 16 2021 at 00:00):

We also discussed moving forward with the inductive inductive branch briefly at the end

view this post on Zulip Ali Caglayan (Dec 16 2021 at 00:01):

We can def break some stuff up in there and implement finished parts

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip Jim Fehrle (Jan 02 2022 at 06:30):

The next call is January 5?

view this post on Zulip Gaëtan Gilbert (Jan 02 2022 at 10:15):

only if someone adds a topic

view this post on Zulip Jim Fehrle (Jan 04 2022 at 04:15):

Done.

view this post on Zulip 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.

view this post on Zulip 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?

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

No worries @Matthieu Sozeau I can take the notes

view this post on Zulip Matthieu Sozeau (Feb 23 2022 at 10:09):

I’m on holidays this week, can someone else act as chair for the call ?

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

It is very bad timing for me for the call too

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

due to inria CR deadline being next Tue

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Feb 23 2022 at 10:33):

I can act as chair if needed

view this post on Zulip Enrico Tassi (Feb 23 2022 at 10:49):

I will attend, and I can take notes.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 23 2022 at 10:53):

I will maybe say more on the UI meeting

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

So are there notes of the meeting today?

view this post on Zulip Enrico Tassi (Feb 23 2022 at 18:24):

I have not posted them yet, I'll do it later today, or tomorrow

view this post on Zulip Enrico Tassi (Feb 23 2022 at 21:11):

Notes are online, all people attending are welcome to improve them

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 13:28):

No Coq call today, correct?

view this post on Zulip Matthieu Sozeau (Mar 02 2022 at 14:21):

Correct

view this post on Zulip Gaëtan Gilbert (Mar 30 2022 at 13:11):

not a lot of calls recently

view this post on Zulip Pierre-Marie Pédrot (Mar 30 2022 at 13:33):

too busy wreaking havoc in universe internals to chat about it :nuclear:

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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"

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2022 at 16:24):

Yup 4.13 is good, specially for those on newer mac

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Mar 30 2022 at 16:37):

See (https://github.com/coq/platform/blob/main/README.md)

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Michael Soegtrop (Mar 30 2022 at 16:49):

Also this way all enhancements to the Coq Platform infrastructure - say nicer Readme files - automatically apply to all Coq versions.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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...)

view this post on Zulip Jason Gross (Apr 06 2022 at 12:40):

Is it too late to make it now?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 12:50):

let's get a call then

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 12:52):

https://github.com/coq/coq/wiki/Coq-Call-2022-04-06

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Apr 06 2022 at 12:55):

Next week does not work either for me, but the following one should be fine

view this post on Zulip Enrico Tassi (Apr 06 2022 at 12:56):

So IMO the best is to chat asynchronously if the issue if pressing for you

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 12:58):

the ocaml version bump has been discussed regularly but we never converged

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 12:58):

I think we need a synchronous decision for this one

view this post on Zulip Jason Gross (Apr 06 2022 at 13:12):

The issue is not pressing, let's postpone to the week after next?

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 13:15):

fine fine

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 13:16):

I might not be around though

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 13:16):

so do we cancel this short-lived call already?

view this post on Zulip 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.

view this post on Zulip Jason Gross (Apr 06 2022 at 13:52):

Yeah, I'm just talking about postponing the OCAMLPATH / COQBIN issue

view this post on Zulip Jason Gross (Apr 06 2022 at 13:52):

(sorry for the ambiguity)

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip Pierre-Marie Pédrot (Apr 12 2022 at 11:56):

won't be there either

view this post on Zulip Enrico Tassi (Apr 12 2022 at 12:24):

Sorry @Jim Fehrle , but I don't think I'll make it either.

view this post on Zulip Maxime Dénès (Apr 12 2022 at 17:22):

Let's postpone, to avoid having the discussions twice, then

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Apr 13 2022 at 12:37):

Can someone update the wiki?

view this post on Zulip Matthieu Sozeau (Apr 13 2022 at 13:03):

I'll do it

view this post on Zulip Jim Fehrle (Apr 13 2022 at 13:54):

OK, see you guys next week, then.

view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (Apr 14 2022 at 19:08):

will there be any more people available next week? it's still easter holiday season

view this post on Zulip Maxime Dénès (Apr 15 2022 at 13:03):

I'll be on vacations

view this post on Zulip Emilio Jesús Gallego Arias (Apr 15 2022 at 14:08):

I won't be available either

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Apr 18 2022 at 20:25):

I won't be available.

view this post on Zulip 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.

view this post on Zulip Maxime Dénès (Apr 19 2022 at 08:58):

Yes, let's postpone.

view this post on Zulip Matthieu Sozeau (Apr 19 2022 at 09:48):

Ok, let's postpone again, I'll put your items on top @Jim Fehrle

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Apr 27 2022 at 11:30):

I know that Jason will go, and I think I won't.

view this post on Zulip Gaëtan Gilbert (May 04 2022 at 14:02):

allo

view this post on Zulip Théo Zimmermann (May 04 2022 at 14:06):

Nobody's here today?

view this post on Zulip Pierre-Marie Pédrot (May 04 2022 at 14:06):

As for myself, I'm in a train with a crappy connection.

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

I was busy today, sorry for not attending

view this post on Zulip Ali Caglayan (May 17 2022 at 15:31):

For the record, I've added some topics for the call tomorrow

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (May 25 2022 at 11:15):

Sure, I would be interested.

view this post on Zulip Ali Caglayan (May 25 2022 at 11:43):

@Enrico Tassi I've tried to condense my points into a somewhat parseable document for the call today: https://github.com/coq/coq/wiki/Coq-Call-2022-05-25

view this post on Zulip Ali Caglayan (May 25 2022 at 11:58):

Also if anybody else wants to add some topics please do, only talking about build systems will probably be quite dull.

view this post on Zulip Matthieu Sozeau (May 25 2022 at 14:00):

I'll be a little late, please start without me

view this post on Zulip Maxime Dénès (Jun 29 2022 at 09:17):

Is there a Coq call today?

view this post on Zulip Matthieu Sozeau (Jun 29 2022 at 11:13):

Apparently not

view this post on Zulip Emilio Jesús Gallego Arias (Jun 29 2022 at 12:07):

Not very conveneint for me

view this post on Zulip Emilio Jesús Gallego Arias (Jun 29 2022 at 12:07):

so I propose that if there are no topics we postpone

view this post on Zulip Erik Martin-Dorel (Jun 29 2022 at 12:20):

I have one topic to suggest actually:
applying to https://about.gitlab.com/solutions/open-source/join/

Actually there is not much to discuss (so maybe a Coq call is unneeded), I'd just like to discuss the text of the application itself, before:

(assuming the fact different maintainers apply for different namespaces is better)

Théo and Matthieu, could we talk together to do so? e.g. today at 16:00 if you're available

view this post on Zulip Matthieu Sozeau (Jun 29 2022 at 12:21):

If I’m not mistaken, Coq is already on it

view this post on Zulip Erik Martin-Dorel (Jun 29 2022 at 12:21):

OK, good news then, but I know that this has to be renewed every year…

view this post on Zulip Erik Martin-Dorel (Jun 29 2022 at 12:22):

and this has a big impact, beyond the number of CI/CD minutes:
namely, after September 1st, namespaces for regular Free projects will only have 5 members maximum :-/
https://about.gitlab.com/pricing/faq-efficient-free-tier/#user-limits-on-gitlab-saas-free-tier

view this post on Zulip Matthieu Sozeau (Jun 29 2022 at 12:23):

Yes, good point, I will check when it expires

view this post on Zulip Matthieu Sozeau (Jun 29 2022 at 12:25):

We renewed last september, it experis on september 29th 2022 precisely

view this post on Zulip Erik Martin-Dorel (Jun 29 2022 at 12:28):

OK :+1: BTW, do you know if you kept some of the application text you had posted last time?
(if it can helps somehow for the coq-community application…)

As I can confirm that coq-community is not enrolled yet… and it'll be blocking for us soonish :'-|

view this post on Zulip Matthieu Sozeau (Jun 29 2022 at 12:30):

The application was pretty short :)

view this post on Zulip Erik Martin-Dorel (Jun 29 2022 at 12:31):

OK ^^
BTW @Théo Zimmermann and Matthieu, do you think we could meet up briefly in the Coq weekly call video room today?
or it's better to think of another slot, or just chat in a private Zulip stream for example.

view this post on Zulip Théo Zimmermann (Jun 29 2022 at 12:58):

If we need to meet briefly, I'm available.

view this post on Zulip Matthieu Sozeau (Jun 29 2022 at 14:04):

I'm available as well

view this post on Zulip Théo Zimmermann (Jun 29 2022 at 14:53):

Application for coq-community done :check:

view this post on Zulip Erik Martin-Dorel (Jun 29 2022 at 14:58):

Thanks @Théo Zimmermann !
I added a summary in the wiki here: https://github.com/coq/coq/wiki/Coq-Call-2022-06-29

view this post on Zulip Erik Martin-Dorel (Jun 29 2022 at 14:58):

And I'll ask Cyril Cohen before doing the same application for docker-mathcomp…

view this post on Zulip Matthieu Sozeau (Jul 20 2022 at 13:04):

It seems we won't have another Coq Call before the end of (french) holidays time, I'll setup a page for August 17th (where at least I will be there) for a "back to work" session.

view this post on Zulip Théo Zimmermann (Jul 20 2022 at 14:01):

I won't be there on August 17th, but I will be there the week after.

view this post on Zulip Matthieu Sozeau (Aug 24 2022 at 11:49):

It seems won’t be a call today, which is good since I’m again on holidays :)

view this post on Zulip Gaëtan Gilbert (Aug 31 2022 at 08:37):

bit late to decide to have a call today isn't it?

view this post on Zulip Emilio Jesús Gallego Arias (Aug 31 2022 at 11:29):

@Gaëtan Gilbert seems so

view this post on Zulip Enrico Tassi (Aug 31 2022 at 12:49):

I did check this morning and the page was there, so I've added an item. I've no problem moving it to next week.

view this post on Zulip Théo Zimmermann (Aug 31 2022 at 13:00):

The page was created by @Pierre-Marie Pédrot at 8:06.

view this post on Zulip Théo Zimmermann (Aug 31 2022 at 13:01):

I have no problem not having a meeting today, but I won't be available next week unfortunately.

view this post on Zulip Pierre-Marie Pédrot (Aug 31 2022 at 13:17):

We have to take a decision for the findlib fix, otherwise this will defer the release

view this post on Zulip Pierre-Marie Pédrot (Aug 31 2022 at 13:17):

I'm not a specialist of this part of the code so I can't just merge it

view this post on Zulip Enrico Tassi (Aug 31 2022 at 13:58):

I can join

view this post on Zulip Gaëtan Gilbert (Aug 31 2022 at 21:59):

any results from the pr process discussion?

view this post on Zulip Maxime Dénès (Sep 01 2022 at 07:00):

Nothing concrete, AFAICT

view this post on Zulip Maxime Dénès (Sep 01 2022 at 07:02):

But we mentioned:

view this post on Zulip Matthieu Sozeau (Sep 07 2022 at 12:59):

There'll be no call today.

view this post on Zulip Matthieu Sozeau (Sep 14 2022 at 13:05):

Again, no call today for lack of subjects. I'll make a page for next week with topic RM for 8.17.

view this post on Zulip Karl Palmskog (Sep 20 2022 at 22:38):

a bit of confusion about the next call - the URL says Sept 21, but the content says Sept 22: https://github.com/coq/coq/wiki/Coq-Call-2022-09-21

view this post on Zulip Matthieu Sozeau (Sep 21 2022 at 06:45):

Fixed

view this post on Zulip Théo Zimmermann (Sep 21 2022 at 07:47):

The Coq Call is today, as usual

view this post on Zulip Karl Palmskog (Sep 21 2022 at 09:44):

I have a very short Coq Call item today Sept 21 that probably doesn't require more than a minute or two. Any chance I could talk about that early in the call? (Conflicting meeting)

view this post on Zulip Karl Palmskog (Sep 21 2022 at 09:47):

either this, or towards the end maybe?

view this post on Zulip Gaëtan Gilbert (Sep 21 2022 at 09:55):

if you mean the vscoq item on the wiki then yes

view this post on Zulip Karl Palmskog (Sep 21 2022 at 09:56):

OK thanks

view this post on Zulip Théo Zimmermann (Sep 21 2022 at 09:59):

I'd be surprised it just take a minute or two, but we'll see :grinning:

view this post on Zulip Karl Palmskog (Sep 21 2022 at 10:01):

spoiler: I'm just going to raise and wave a figurative flag and ask what can we/I can do to help

view this post on Zulip Paolo Giarrusso (Sep 21 2022 at 17:45):

who's going to follow up re VsCoq? Notes are super-terse but potentially exciting

view this post on Zulip Karl Palmskog (Sep 21 2022 at 17:51):

my bottom line: I asked for a decision on some sort of interim maintenance of VsCoq while we wait for this: https://github.com/coq-community/vscoq/wiki/VsCoq-1.0-Roadmap

however, some of the people involved were not able to attend the Call, so we have to wait for their opinions

view this post on Zulip Karl Palmskog (Sep 21 2022 at 17:53):

what we can do from community side is help out with advertising for interim VsCoq maintainers, but we need advice and thumbs-up from core to do this (in my view). It's also going to be potentially unthankful to be an interim maintainer, since a lot of the old code is potentially on the way out via the roadmap

view this post on Zulip Karl Palmskog (Sep 21 2022 at 17:58):

here is the key piece of background/motivation: https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/ide-multiple-barplot.png

view this post on Zulip Paolo Giarrusso (Sep 21 2022 at 18:09):

I recall quite a few existing MRs about highlighting/autocompletion/… etc that probably wouldn’t be replaced at first?

view this post on Zulip Paolo Giarrusso (Sep 21 2022 at 18:10):

At least, that’s been my assumption, but hopefully some scope could be identified

view this post on Zulip Paolo Giarrusso (Sep 21 2022 at 18:12):

Either way, there are enough users of older Coq’s and enough work maturing things that I don’t know how soon this work would be superseded.

view this post on Zulip Paolo Giarrusso (Sep 21 2022 at 18:14):

I’m on mobile and can’t fork a thread here, but I’m going to tag @Ramkumar Ramachandra as another of the contributors there

view this post on Zulip Ramkumar Ramachandra (Sep 21 2022 at 18:21):

Yeah, we’ve been waiting for that item for a long time. It’s safe to say that VSCoq is in low-maintenance mode, not accepting new patches now.

view this post on Zulip Matthieu Sozeau (Sep 22 2022 at 08:34):

I think we need to know, how close is coq-lsp to providing the same functionality as VsCoq?

view this post on Zulip Karl Palmskog (Sep 22 2022 at 08:36):

that's important information, for sure. But also, even if the functionality might be there, how far off is appropriate packaging, how stable is it for everyday use, etc.

view this post on Zulip Karl Palmskog (Sep 22 2022 at 08:37):

I think a lot of users might want to stay on the "old but proven" VsCoq version if there are stability problems.

view this post on Zulip Matthieu Sozeau (Sep 22 2022 at 08:56):

Sure, it's quite likely to be case that we won't completely replace VsCoq in the very short term. I'm happy with asking for volunteers to maintain the current VsCoq in the meantime.

view this post on Zulip Karl Palmskog (Sep 22 2022 at 09:01):

OK, that's great! But, I'd like to get permission on this also from the key players: @Maxime Dénès, @Enrico Tassi, @Emilio Jesús Gallego Arias. We don't want to step on people's toes here, we (or at least I) just want there to be basic VsCoq maintenance: review and merging of bugfixes, documentation improvements, bugfix releases, etc., even in the face of the fact this code might be obsoleted.

view this post on Zulip Matthieu Sozeau (Sep 22 2022 at 09:21):

Yes, I want that too :)

view this post on Zulip Enrico Tassi (Sep 22 2022 at 11:20):

I'm OK to ask for help maintaining what we have for the coming months

view this post on Zulip Enrico Tassi (Sep 22 2022 at 11:21):

The only thing I ask is to make the volunteers aware of the roadmap

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 11:47):

Hi folks, turns out there is a double seminar today so I may arrive half an hour late, hopefully earlier

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 13:16):

So maybe it is better to postpone my topics for next week?


Last updated: Feb 01 2023 at 16:03 UTC