Stream: Coq devs & plugin devs

Topic: Coq Working Group February 2023


view this post on Zulip Matthieu Sozeau (Nov 30 2022 at 15:50):

Here's a doodle link to try to find a date for a Working Group in Paris early february: https://framadate.org/mprvHD4vemlkQsUF

view this post on Zulip Guillaume Melquiond (Dec 09 2022 at 16:51):

Note that the ProgLang days have just been scheduled for February 8th (afternoon) and 9th. I am not sure how much overlap between the attendants of both events there is. But if it is important, then February 7th and 8th (morning) might be a sensible choice for the working group, so as to reduce travels.

view this post on Zulip Maxime Dénès (Dec 09 2022 at 16:54):

@Guillaume Melquiond Do you have a pointer to that event? (just curious)

view this post on Zulip Guillaume Melquiond (Dec 09 2022 at 16:59):

I don't think there is anything yet. But if you are not aware of that event, it presumably means you have not been subscribed to the corresponding mailing list, so I am forwarding you the original email.

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

Thanks a lot!

view this post on Zulip Matthieu Sozeau (Jan 04 2023 at 14:13):

We're going to do it february 7 and 8th

view this post on Zulip Maxime Dénès (Jan 04 2023 at 14:26):

Sorry @Matthieu Sozeau , I just saw the results. Doing it on Jan 30/31 or Jan 31/Feb 01 would be a big plus for me. Do you think it is still possible?

view this post on Zulip Maxime Dénès (Jan 04 2023 at 14:27):

There were only small minuses for @Guillaume Melquiond at these dates.

view this post on Zulip Maxime Dénès (Jan 04 2023 at 14:31):

Maxime Dénès said:

Sorry Matthieu Sozeau , I just saw the results. Doing it on Jan 30/31 or Jan 31/Feb 01 would be a big plus for me. Do you think it is still possible?

(it would save me another Nice-Inria Paris trip, essentially)

view this post on Zulip Matthieu Sozeau (Jan 04 2023 at 14:36):

It is still possible.

view this post on Zulip Matthieu Sozeau (Jan 04 2023 at 14:36):

It is still possible.

view this post on Zulip Maxime Dénès (Jan 04 2023 at 14:37):

Sorry about that :)

view this post on Zulip Matthieu Sozeau (Jan 04 2023 at 14:38):

Let's propose Jan 31/Feb 01 for now and see at the call if there are problems with it

view this post on Zulip Ali Caglayan (Jan 08 2023 at 16:26):

I've created a page for the Jan workshop https://github.com/coq/coq/wiki/CoqWG-2023-01-31

view this post on Zulip Ali Caglayan (Jan 08 2023 at 16:26):

Please add yourself if you plan on participating. Also add any topics.

view this post on Zulip Gaëtan Gilbert (Jan 09 2023 at 08:26):

is it at the usual inria near gare de lyon?
what times are we starting/ending?

view this post on Zulip Théo Zimmermann (Jan 09 2023 at 08:37):

is it at the usual inria near gare de lyon?

Yes

view this post on Zulip Maxime Dénès (Jan 09 2023 at 11:32):

@Matthieu Sozeau Did you book a room?

view this post on Zulip Matthieu Sozeau (Jan 09 2023 at 11:33):

I asked @Emilio Jesús Gallego Arias and @Hugo Herbelin , waiting for them

view this post on Zulip Matthieu Sozeau (Jan 10 2023 at 11:39):

Well, I preemptively reserved the Alan Turing room (16 people, with visio support)

view this post on Zulip Matthieu Sozeau (Jan 10 2023 at 11:44):

This was the only room I could book that was free. There are other rooms but bookable only by Parisians

view this post on Zulip Matthieu Sozeau (Jan 10 2023 at 11:47):

Note that originally I indicated I would not be able to help much organize the WG in January, I'm already pretty busy (and tired). So can someone (ideally in Paris) please take the lead to prepare the rest (breaks/lunch/social event, planing of the meeting) ?

view this post on Zulip Emilio Jesús Gallego Arias (Jan 10 2023 at 12:13):

Yes @Matthieu Sozeau

view this post on Zulip Théo Zimmermann (Jan 10 2023 at 12:38):

@Emilio Jesús Gallego Arias if you are taking part in the organization, maybe add your name to the organizers line on the wiki page.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 10 2023 at 12:38):

Yes, I will, thanks Theo

view this post on Zulip Emilio Jesús Gallego Arias (Jan 10 2023 at 12:39):

I've been away til yesterday, sorry I wasn't very helpful with this

view this post on Zulip Emilio Jesús Gallego Arias (Jan 10 2023 at 12:39):

Will finish catching up later today

view this post on Zulip Emilio Jesús Gallego Arias (Jan 11 2023 at 19:31):

For the lunch / coffee breaks we need to know how many we'll be, @all please register at https://github.com/coq/coq/wiki/CoqWG-2023-01-31

view this post on Zulip Emilio Jesús Gallego Arias (Jan 11 2023 at 19:32):

Please note if you would like to come to a "social event" / dinner

view this post on Zulip Jim Fehrle (Jan 11 2023 at 19:44):

Will there be an in-person developer's workshop this year?

view this post on Zulip Théo Zimmermann (Jan 11 2023 at 19:57):

That would be nice, but I don't think anyone has started to plan anything like that yet.

view this post on Zulip Enrico Tassi (Jan 11 2023 at 20:16):

I did register, but the program is still quite empty for a full two days. Before booking a flight at 6:45 AM I'd like to know what will be the topic of Tuesday morning, and if there will be topics for a second day.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 11 2023 at 20:26):

@Enrico Tassi we discussed today about when to start in the call, @all please also add your topics ASAP

view this post on Zulip Emilio Jesús Gallego Arias (Jan 11 2023 at 20:26):

But indeed, if there are only these topics no point in starting early

view this post on Zulip Enrico Tassi (Jan 11 2023 at 20:34):

There are a few topics already, but none with a duration. Please try to say how much time your topics should take

view this post on Zulip Emilio Jesús Gallego Arias (Jan 11 2023 at 20:40):

Good idea, the assumption was a 1 hour slot each

view this post on Zulip Matthieu Sozeau (Jan 12 2023 at 11:03):

Shouldn’t we have a brainstorming session about the libobject CEP and https://github.com/coq/coq/pull/16484 ?

view this post on Zulip Enrico Tassi (Jan 16 2023 at 21:26):

Sorry to insist, but Is the current list final? Anything else?
Who is doing the funind thing?

view this post on Zulip Karl Palmskog (Jan 16 2023 at 21:33):

curious if there is a plan to regain native_compute in OCaml 5? Or if there is an effort that has some status?

view this post on Zulip Enrico Tassi (Jan 16 2023 at 21:34):

Hum, that calls for the roadmap compilation (@Maxime Dénès , @Théo Zimmermann )...

view this post on Zulip Karl Palmskog (Jan 16 2023 at 21:49):

(another possible item for roadmap: Alectryon for Coq refman)

view this post on Zulip Maxime Dénès (Jan 16 2023 at 22:23):

I wrote down the funind item after @Yves Bertot talked about it during the last call, but I don't have anything to present related to that

view this post on Zulip Emilio Jesús Gallego Arias (Jan 16 2023 at 23:01):

Indeed I was thinking of doing the schedule maybe tomorrow, what do you think @Matthieu Sozeau ?

view this post on Zulip Emilio Jesús Gallego Arias (Jan 16 2023 at 23:01):

Seems like there are no more topics

view this post on Zulip Emilio Jesús Gallego Arias (Jan 17 2023 at 10:57):

@Enrico Tassi while we wait for more feedback, I can try to make a preliminary schedule, what is a good time for you to start the first day?

It seems to me we have time to accommodate those travelling in the day?

I will send resto options later in the day

view this post on Zulip TJ Barclay (Jan 18 2023 at 17:08):

Are the working group meetings going to be live-streamed?

view this post on Zulip Emilio Jesús Gallego Arias (Jan 18 2023 at 17:17):

@TJ Barclay I'm unsure, but I guess we could arrange something if you are interested in attending some particular session?

view this post on Zulip TJ Barclay (Jan 18 2023 at 17:28):

I was particularly interested in discussions around Equations on Tuesday morning

view this post on Zulip Gaëtan Gilbert (Jan 18 2023 at 17:31):

when I tried to remote attend the last wg it was no good and I gave up
so if all we have to live stream is a random laptop IMO it won't work out

view this post on Zulip Emilio Jesús Gallego Arias (Jan 18 2023 at 19:17):

TJ Barclay said:

I was particularly interested in discussions around Equations on Tuesday morning

I need to check with the rest of the organizers and see the room but we'll try to work out something.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 18 2023 at 19:19):

But indeed often the streaming setup is not good, but we can try.

view this post on Zulip Théo Zimmermann (Jan 18 2023 at 19:26):

Weren't we supposed to meet in a room with visio capabilities?

view this post on Zulip Matthieu Sozeau (Jan 19 2023 at 14:27):

The one I reserved has visio indeed

view this post on Zulip Matthieu Sozeau (Jan 19 2023 at 14:27):

So in principle it should work fine

view this post on Zulip Emilio Jesús Gallego Arias (Jan 19 2023 at 16:05):

I've added to the webpage a list of possible restaurant choices, please add your own, and express your preferences so we can make the reservations, thanks! https://github.com/coq/coq/wiki/CoqWG-2023-01-31#lunch-and-dinner-events

view this post on Zulip Matthieu Sozeau (Jan 19 2023 at 16:37):

For the people in Nice (@Enrico Tassi and @Maxime Dénès) , we moved topics we thought you could easily miss to Tuesday morning, in case you can change your tickets to something later)

view this post on Zulip Maxime Dénès (Jan 20 2023 at 12:29):

There will be a strike on the 31. What should we do ?

view this post on Zulip Maxime Dénès (Jan 20 2023 at 12:30):

It is likely to be very hard for people to travel from outside Paris.

view this post on Zulip Matthieu Sozeau (Jan 20 2023 at 12:44):

Argh... indeed. I guess we'll have to setup visio stuff? Or people think it's better to postpone??

view this post on Zulip Maxime Dénès (Jan 20 2023 at 12:48):

Good question, I'm not sure. I was happy that we could meet in person at last. But maybe postponing is too complicated, I don't know.

view this post on Zulip Michael Soegtrop (Jan 20 2023 at 13:14):

If it is online, I could participate (in case there are questions or feedback on the Coq Platform / release process - I could also report on my progress on term simplification in automation like VST - I think it gives some clues on what features to add to Coq).

view this post on Zulip Maxime Dénès (Jan 20 2023 at 18:23):

In fact, travelling on the 30th could be ok.

view this post on Zulip Maxime Dénès (Jan 20 2023 at 18:24):

But having also a visio solution would be nice, in case the plan fails. And so that Michael and others can attend.

view this post on Zulip Ali Caglayan (Jan 20 2023 at 23:17):

I will be travelling in on the 30th so it shouldn't affect me right?

view this post on Zulip Matthieu Sozeau (Jan 21 2023 at 18:14):

Yep, same here actually

view this post on Zulip Enrico Tassi (Jan 21 2023 at 18:34):

Hello, here at Coq PL there are people willing to discuss UI related research with us. The problem is that only tuesday works for them. Would it be possible to swap the two afternoons programs an have 2 hours (or more) on Tuesday dedicated to this?

view this post on Zulip Enrico Tassi (Jan 21 2023 at 19:04):

@Matthieu Sozeau @Emilio Jesús Gallego Arias would this be OK for you? It would require remote participation to be possible, of course.

view this post on Zulip Matthieu Sozeau (Jan 21 2023 at 19:31):

Sure, I think we can swap at will

view this post on Zulip Enrico Tassi (Jan 21 2023 at 19:35):

OK then, I'll fix the wiki and tell them ASAP, thanks for the quick reply

view this post on Zulip Emilio Jesús Gallego Arias (Jan 21 2023 at 19:44):

No constraints on my side

view this post on Zulip Maxime Dénès (Jan 21 2023 at 20:12):

Do you guys have any way to test the visio setup next week? So that we could ask for something better if needed.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 21 2023 at 20:14):

Let me see if I can stop by

view this post on Zulip Matthieu Sozeau (Jan 23 2023 at 14:08):

I've setup two Webex meetings for the WG and another test drive meeting on January 30th at 6pm (Paris time), the details are on the WG page.

view this post on Zulip Matthieu Sozeau (Jan 25 2023 at 12:28):

I've updated the slot about renaming, I think we should use that time to discuss other subjects with the core team, like adding new members.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 27 2023 at 13:31):

Folks, last call for restaurant options, I'll make a reservation tomorrow.

By the way, what would you like to know about coq-lsp ?

view this post on Zulip Théo Zimmermann (Jan 27 2023 at 17:05):

The same thing I would like to learn is a general question on which you alone won't be able to answer: what is the future of UI-related work for Coq. For instance, is there any hope that the ongoing work on VsCoq 2 can benefit coq-lsp or the converse? What is the future of SerAPI ? Of CoqIDE / the XML protocol ? Can we start recommending the use of coq-lsp instead of the XML protocol to IDE maintainers ? to other tool writers?

view this post on Zulip Théo Zimmermann (Jan 27 2023 at 17:06):

So any presentation of coq-lsp elements or roadmaps that can help answer partially these questions would be welcome.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 27 2023 at 17:14):

Thanks for the feedback Théo

view this post on Zulip Enrico Tassi (Jan 28 2023 at 06:01):

I'd like to understand how the incrementality of fleche works, and how it does less work than coqtop/emacs or stm/coqide

view this post on Zulip Emilio Jesús Gallego Arias (Jan 30 2023 at 00:05):

Thanks for the feedback Enrico

view this post on Zulip Emilio Jesús Gallego Arias (Jan 30 2023 at 00:06):

Update on local organization: Turns out the strike means on Tuesday we won't be able to have coffee and cookies served; please keep me posted (by private) if you won't be able to make it to the dinner due to this.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 30 2023 at 00:07):

I've reserved for 12 people at La fille à Papa

view this post on Zulip Théo Zimmermann (Jan 30 2023 at 10:14):

Note that the number of people registered for the social event on the wiki page is actually 13.

view this post on Zulip Ali Caglayan (Jan 30 2023 at 12:14):

If we buy some coffee, surely we can make it ourselves no?

view this post on Zulip Matthieu Sozeau (Jan 30 2023 at 17:22):

Hmm, if we get coffee caps certainly the Inria teams will certainly let us use their machines :)

view this post on Zulip Matthieu Sozeau (Jan 30 2023 at 17:22):

FYI, there's a test call at https://inria.webex.com/inria/j.php?MTID=md599a92cb89038552da5fb97aa0ecb96 if you want to check your setup

view this post on Zulip Matthieu Sozeau (Jan 30 2023 at 17:23):

Right now

view this post on Zulip Ali Caglayan (Jan 31 2023 at 07:08):

Good morning, is anybody here yet?

view this post on Zulip Matthieu Sozeau (Jan 31 2023 at 07:09):

I’ll come around a little bit after 9am I think

view this post on Zulip Ali Caglayan (Jan 31 2023 at 08:38):

It is the building where Hugo and Emilios office is right?

view this post on Zulip Enrico Tassi (Jan 31 2023 at 08:47):

Building C

view this post on Zulip Enrico Tassi (Jan 31 2023 at 08:47):

The lady at the entrance knows about a "groupe de travail Coq"

view this post on Zulip Gaëtan Gilbert (Jan 31 2023 at 08:47):

https://www.google.com/maps/place/48%C2%B050'29.9%22N+2%C2%B023'04.2%22E

view this post on Zulip Enrico Tassi (Jan 31 2023 at 08:48):

First floor, room 115 (take the stairs behind the elevator, since without a badge it won't work)

view this post on Zulip Matthieu Sozeau (Jan 31 2023 at 16:06):

Bar la Liberté https://www.google.com/maps/place/La+Libert%C3%A9/@48.8500576,2.3829537,18z/data=!3m1!4b1!4m22!1m16!4m15!1m6!1m2!1s0x47e6720c0b8b18b1:0xac56591ff9a11b20!2sFaidherbe+-+Chaligny,+Paris!2m2!1d2.3841559!2d48.8502738!1m6!1m2!1s0x47e67213981eb799:0x5cac9b4921551bb9!2s2+Rue+Simone+IFF,+Paris!2m2!1d2.3846535!2d48.8414531!3e2!3m4!1s0x47e6720c0609646b:0xdd7ab7d3c977e1fb!8m2!3d48.8500576!4d2.3839759

view this post on Zulip Emilio Jesús Gallego Arias (Jan 31 2023 at 17:25):

Folks by the way the dinner is a 8pm not at 7:30 as I put in the wiki

view this post on Zulip Emilio Jesús Gallego Arias (Jan 31 2023 at 17:25):

just in case


Last updated: Feb 06 2023 at 19:03 UTC