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


Last updated: Oct 21 2021 at 20:02 UTC