Coq Working Group February 2023 · Coq devs & plugin devs

Stream: Coq devs & plugin devs

Topic: Coq Working Group February 2023

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

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.

Maxime Dénès (Dec 09 2022 at 16:54):

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

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.

Maxime Dénès (Dec 09 2022 at 17:02):

Thanks a lot!

Matthieu Sozeau (Jan 04 2023 at 14:13):

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

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?

Maxime Dénès (Jan 04 2023 at 14:27):

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

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)

Matthieu Sozeau (Jan 04 2023 at 14:36):

It is still possible.

Matthieu Sozeau (Jan 04 2023 at 14:36):

It is still possible.

Maxime Dénès (Jan 04 2023 at 14:37):

Sorry about that :)

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

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

Ali Caglayan (Jan 08 2023 at 16:26):

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

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?

Théo Zimmermann (Jan 09 2023 at 08:37):

is it at the usual inria near gare de lyon?

Yes

Maxime Dénès (Jan 09 2023 at 11:32):

@Matthieu Sozeau Did you book a room?

Matthieu Sozeau (Jan 09 2023 at 11:33):

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

Matthieu Sozeau (Jan 10 2023 at 11:39):

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

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

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) ?

Emilio Jesús Gallego Arias (Jan 10 2023 at 12:13):

Yes @Matthieu Sozeau

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.

Emilio Jesús Gallego Arias (Jan 10 2023 at 12:38):

Yes, I will, thanks Theo

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

Emilio Jesús Gallego Arias (Jan 10 2023 at 12:39):

Will finish catching up later today

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

Emilio Jesús Gallego Arias (Jan 11 2023 at 19:32):

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

Jim Fehrle (Jan 11 2023 at 19:44):

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

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.

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.

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

Emilio Jesús Gallego Arias (Jan 11 2023 at 20:26):

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

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

Emilio Jesús Gallego Arias (Jan 11 2023 at 20:40):

Good idea, the assumption was a 1 hour slot each

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 ?

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?

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?

Enrico Tassi (Jan 16 2023 at 21:34):

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

Karl Palmskog (Jan 16 2023 at 21:49):

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

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

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 ?

Emilio Jesús Gallego Arias (Jan 16 2023 at 23:01):

Seems like there are no more topics

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

TJ Barclay (Jan 18 2023 at 17:08):

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

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?

TJ Barclay (Jan 18 2023 at 17:28):

I was particularly interested in discussions around Equations on Tuesday morning

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

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.

Emilio Jesús Gallego Arias (Jan 18 2023 at 19:19):

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

Théo Zimmermann (Jan 18 2023 at 19:26):

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

Matthieu Sozeau (Jan 19 2023 at 14:27):

The one I reserved has visio indeed

Matthieu Sozeau (Jan 19 2023 at 14:27):

So in principle it should work fine

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

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)

Maxime Dénès (Jan 20 2023 at 12:29):

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

Maxime Dénès (Jan 20 2023 at 12:30):

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

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??

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.

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).

Maxime Dénès (Jan 20 2023 at 18:23):

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

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.

Ali Caglayan (Jan 20 2023 at 23:17):

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

Matthieu Sozeau (Jan 21 2023 at 18:14):

Yep, same here actually

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?

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.

Matthieu Sozeau (Jan 21 2023 at 19:31):

Sure, I think we can swap at will

Enrico Tassi (Jan 21 2023 at 19:35):

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

Emilio Jesús Gallego Arias (Jan 21 2023 at 19:44):

No constraints on my side

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.

Emilio Jesús Gallego Arias (Jan 21 2023 at 20:14):

Let me see if I can stop by

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.

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.

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 ?

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?

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.

Emilio Jesús Gallego Arias (Jan 27 2023 at 17:14):

Thanks for the feedback Théo

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

Emilio Jesús Gallego Arias (Jan 30 2023 at 00:05):

Thanks for the feedback Enrico

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.