Stream: Coq devs & plugin devs

Topic: coq calls


view this post on Zulip Gaëtan Gilbert (Nov 16 2022 at 16:20):

that was a kinda abrupt end :)

view this post on Zulip Emilio Jesús Gallego Arias (Nov 16 2022 at 16:27):

Are you folks gonna add some notes? If not I will

view this post on Zulip Janno (Nov 16 2022 at 16:28):

I'd be interested to learn what came out of the performance working group discussion point. (I was going to join the meeting but I couldn't make it.)

view this post on Zulip Jason Gross (Nov 16 2022 at 16:29):

I'm also quite interested in the performance working group discussion notes. (I forgot to check the agenda before missing the call, but would have shown up if I had seen this.)

view this post on Zulip Théo Zimmermann (Nov 16 2022 at 16:31):

We didn't reach that point. However, we discussed quite a bit about fiat-crypto and CI more generally and it would be nice to schedule a call where we can discuss this again that you can attend.

view this post on Zulip Jason Gross (Nov 16 2022 at 16:32):

Given advance notice, I think I should be able to generally attend coq calls these days

view this post on Zulip Théo Zimmermann (Nov 16 2022 at 16:32):

Are you back on the East coast?

view this post on Zulip Jason Gross (Nov 16 2022 at 16:55):

I'm on the East Coast until around the end of December, then back on the West Coast (but hopefully will be keeping a schedule that still lets me attend).

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

Ok, notes added, topics pushed to next call

view this post on Zulip Jason Gross (Nov 16 2022 at 20:09):

Fiat-crypto failing for a long time, we can't afford to fix it

I think it should be fixed by https://github.com/coq/coq/pull/16809 + https://github.com/coq/coq/pull/16801

view this post on Zulip Gaëtan Gilbert (Nov 18 2022 at 11:58):

why are there a bunch of fake links on https://github.com/coq/coq/wiki/Coq-Calls ? eg https://github.com/coq/coq/wiki/Coq-Call-2022-11-23

view this post on Zulip Théo Zimmermann (Nov 18 2022 at 11:59):

Emilio added them...

view this post on Zulip Emilio Jesús Gallego Arias (Nov 18 2022 at 12:59):

There are no fake links, but placeholders

view this post on Zulip Emilio Jesús Gallego Arias (Nov 18 2022 at 13:00):

until the call of the 14th which is the next I'll join and where I postponed my topcis

view this post on Zulip Emilio Jesús Gallego Arias (Nov 18 2022 at 13:00):

doesn't make sense?

view this post on Zulip Enrico Tassi (Nov 18 2022 at 13:01):

Coq-Call-2022-12-07 (likely not Coq Call, math-comp workshop)

Why?

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

Why what?

view this post on Zulip Enrico Tassi (Nov 18 2022 at 13:05):

I don't see why the call should be canceled.. but if it will for that reason, why the placeholder then?

view this post on Zulip Enrico Tassi (Nov 18 2022 at 13:06):

I guess we can keep the entry actually pointing to a page and kill the other links

view this post on Zulip Emilio Jesús Gallego Arias (Nov 18 2022 at 13:06):

Sure, I guess you can edit it to say: (maybe not Coq Call due to math-comp workshop?)

view this post on Zulip Emilio Jesús Gallego Arias (Nov 18 2022 at 13:06):

Sure for the rest, it is a wiki folks, go ahead and tweak stuff

view this post on Zulip Emilio Jesús Gallego Arias (Nov 18 2022 at 13:07):

The placeholder is because it indeed happens, but also because we have been putting placeholders like this for calls that don't happen

view this post on Zulip Emilio Jesús Gallego Arias (Nov 18 2022 at 13:07):

then we edit them the day of the call to remove the link if the call doesn't happen

view this post on Zulip Théo Zimmermann (Nov 18 2022 at 13:14):

The way we have proceeded so far was to not put the link to the webpage until someone creates it with some agenda.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 18 2022 at 13:25):

Yup, we can remove the links; I was afraid if I didn't put the link it could be interpreted as "no call"? I dunno, it is not common we do like the other day

view this post on Zulip Cyril Cohen (Nov 23 2022 at 13:20):

I had put a point on today's coq call page but I prefer to raise the question on zulip

view this post on Zulip Matthieu Sozeau (Nov 23 2022 at 13:28):

Ok, so no call today. I’ll be back next week!

view this post on Zulip Ali Caglayan (Nov 29 2022 at 21:09):

I've added a topic about OCaml 5.0 to the Coq call for tomorrow so we can discuss what to do about OCaml 5.0 support.

view this post on Zulip Ali Caglayan (Nov 30 2022 at 15:43):

The link Guillaume shared: http://gallium.inria.fr/~scherer/research/constructor-unboxing/constructor-unboxing-jfla.pdf

view this post on Zulip Matthieu Sozeau (Dec 14 2022 at 11:48):

There’ll be no call today as no topics were raised.

view this post on Zulip Jason Gross (Dec 14 2022 at 15:08):

I thought there was going to be a performance working group discussion? (It seems there was one scheduled for today, but it was removed by @Emilio Jesús Gallego Arias on Dec 5 or 6 at https://github.com/coq/coq/wiki/_compare/983221be98158ed1907d8b8cf33ccdb5a73ab75d...d902d6c7806ab5c1988561b7d972c489187f4897 along with:

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

Yup

view this post on Zulip Jason Gross (Dec 14 2022 at 15:36):

Is there going to be a performance working group topic at some point? (I'm also curious about the motivation for putting it on the call in the first place, the motivation for taking it off, etc.)

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

Jason Gross said:

Is there going to be a performance working group topic at some point?

I don't know.

(I'm also curious about the motivation for putting it on the call in the first place, the motivation for taking it off, etc.)

Performance is something I've been interested since a long time (back to my start with Coq), so I thought I'd be a nice idea to discuss more. I took it off because I am not motivated anymore.


Last updated: Feb 06 2023 at 19:03 UTC