Stream: Coq devs & plugin devs

Topic: Coq Working Group June 2022


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

We had agreed some time ago to hold a two-day Coq Working Group in June, at Inria Sophia-Antipolis. Here's the evento to pick the date: https://evento.renater.fr/survey/coq-working-group-june-2022-rw66vmhw

view this post on Zulip Maxime Dénès (Apr 27 2022 at 07:54):

I would also like to collect topics in order to prepare the agenda. Any suggestions?

view this post on Zulip Ali Caglayan (Apr 27 2022 at 10:14):

@Maxime Dénès I have a few suggestions:

  1. Reorganizing / reforming the stdlib / stdlib2 projects. I have a lot more detailed notes on what needs to be done to get this project moving from the last hackathon.
  2. Separation of ltac2 from ltac. We discussed with PMP how to do this, but there are still a few obstacles.
  3. The namespacing CEP https://github.com/coq/ceps/pull/25
  4. The unification of vernac definitions CEP https://github.com/coq/ceps/pull/42
  5. Separate compilation CEP https://github.com/coq/ceps/pull/62 (I know you have been working on related things)

These honestly might be too big to do in 2 days, but other than fixing bugs I don't know what we could do.

view this post on Zulip Gaëtan Gilbert (Apr 27 2022 at 10:18):

finish coq_dune? although it would be nice if that could be done earlier

view this post on Zulip Ali Caglayan (Apr 27 2022 at 10:22):

The test-suite is very close to completion, I was planning to show it off in a call soon. It should be straightforward to adapt what we learnt there to coq_dune. This is of course @Emilio Jesús Gallego Arias's project however so I cannot say for certain.

view this post on Zulip Gaëtan Gilbert (Apr 27 2022 at 10:26):

I don't care about the test suite, I want a way to deal with bugs like https://github.com/coq/coq/pull/15951

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

@Emilio Jesús Gallego Arias I think it could be nice if you present a quick status report in the build infrastructure at this June WG. Do you thinkl it would be a good idea?

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

@Théo Zimmermann Do you need a slot related to presenting the poll results, or the name change?

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

Btw, I'm afraid @Théo Zimmermann and @Ali Caglayan gave incompatible constraints in the evento. Are the "no" hard for both of you? Or could you still make it in some scenarios?

view this post on Zulip Ali Caglayan (May 02 2022 at 09:47):

My no is not hard at all. I thought those were preferred dates, but I don't mind removing my constraints entirely, I can be adaptable.

view this post on Zulip Théo Zimmermann (May 02 2022 at 10:16):

My no for June 1st is hard, but not for June 2nd (I'd have to travel in the morning), and not for next week (there is Journées du GDR GPL which I planned to attend, but I could skip as I have no commitment there yet). My no for the end of June is hard because of JFLA but I guess this is not an option anymore given the other answers.

view this post on Zulip Théo Zimmermann (May 02 2022 at 10:35):

And sure, if I can make it to the WG, I'd be happy to have a slot to present poll results / discuss the name change.

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

Maxime Dénès said:

Emilio Jesús Gallego Arias I think it could be nice if you present a quick status report in the build infrastructure at this June WG. Do you thinkl it would be a good idea?

Sure, what would you like to see in that presentation? Note that https://github.com/coq/coq/pull/15560 will be merged by the WG time.

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

@Maxime Dénès But I would appreciate if the date of the WG could be set soon. If I can go to Journées du GDR GPL, I have to register soon.

view this post on Zulip Maxime Dénès (May 04 2022 at 09:27):

Yes, I'll try to finalize the reservation of rooms today. Until it is done, I can't be sure of the dates.

view this post on Zulip Maxime Dénès (May 04 2022 at 11:56):

It seems more likely to be June 15-16 given the availability of rooms. I'll keep you posted.

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

The Working Group will take place on June 15-16 in Sophia-Antipolis. I will post more details shortly.

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

@Théo Zimmermann You wanted to know the final dates.

view this post on Zulip Enrico Tassi (May 06 2022 at 09:20):

CC @Enzo Crance

view this post on Zulip Maxime Dénès (May 11 2022 at 12:31):

Please post the topics you'd like to discuss here: https://github.com/coq/coq/wiki/Next-Coq-Working-Group

view this post on Zulip Maxime Dénès (May 11 2022 at 12:31):

For those who can, we'd recommend the Moxy hotel in Sophia Antipolis. Likely to be the most convenient for a short event.

view this post on Zulip Maxime Dénès (May 11 2022 at 12:31):

I don't think it is in the Inria hotel market, though.

view this post on Zulip Maxime Dénès (May 16 2022 at 13:08):

@all We need to communicate a list of participants. Could you please add your name to the list if you plan to attend? https://github.com/coq/coq/wiki/Next-Coq-Working-Group

view this post on Zulip Maxime Dénès (May 23 2022 at 07:47):

We have only 5 participants listed, so far. Do not hesitate to add your name to the list, even if you are not 100% sure you can attend. The point is only to make people here at Inria Sophia aware that they should let you in.

view this post on Zulip Gaëtan Gilbert (May 25 2022 at 15:09):

Is there a guide to get there (train or what?)?

view this post on Zulip Enrico Tassi (May 25 2022 at 15:11):

From the airport, take the 230. From Antibes, take the 100 or 1 (aka A), from the Moxy, walk.

view this post on Zulip Enrico Tassi (May 25 2022 at 15:12):

https://www.inria.fr/en/how-get-inria-centre-universite-cote-dazur-and-its-montpellier-antenna

view this post on Zulip Enrico Tassi (May 25 2022 at 15:13):

There are night trans to Antibes

view this post on Zulip Enrico Tassi (May 25 2022 at 15:13):

(from Paris)

view this post on Zulip Enrico Tassi (May 25 2022 at 15:14):

IIRC 230 is in T1, but there is a free tram from T2 (airfrance/easyjet) to T1 (luftansa)

view this post on Zulip Enrico Tassi (May 25 2022 at 15:15):

From the train station, climb the stairs to the "passerelle SNCF" (google map knows) and you'll find the "pole d'echange" where you have the A bus of the 100 express bus

view this post on Zulip Enrico Tassi (May 25 2022 at 15:15):

100 stops at "Templier" which is 200m away from Inria, A stop is called "Inria".

view this post on Zulip Enrico Tassi (May 25 2022 at 15:16):

But for the 1 -> A renaming, I think this page is still OK https://team.inria.fr/marelle/en/venue/

view this post on Zulip Enrico Tassi (May 25 2022 at 15:17):

Also, you can ask Enzo, which I think did already plan the trip

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

what hours will the wg be on? eg just the afternoon on the 15th?

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

@Maxime Dénès ping

view this post on Zulip Maxime Dénès (May 31 2022 at 08:39):

Could you guys add to the wiki page how much time you'd like to have for your slot? @Enrico Tassi @Théo Zimmermann @Ali Caglayan @Michael Soegtrop

view this post on Zulip Maxime Dénès (May 31 2022 at 08:40):

Once I know this, I'll prepare a schedule.

view this post on Zulip Michael Soegtrop (May 31 2022 at 10:47):

My intention was mostly to have an open discussion on

view this post on Zulip Ali Caglayan (May 31 2022 at 10:55):

My topic isn't even that important or interesting so I will remove it

view this post on Zulip Enrico Tassi (May 31 2022 at 10:58):

I think/hope there will be time to chat about tech issues like linking even if without a formal slot. Maybe keep the topic on a side list.

view this post on Zulip Ali Caglayan (May 31 2022 at 11:03):

@Enrico Tassi I've created a "side topics" section.

view this post on Zulip Maxime Dénès (May 31 2022 at 11:20):

@Théo Zimmermann 45 min for the renaming? Are you sure we shouldn't allocate more time?

view this post on Zulip Théo Zimmermann (May 31 2022 at 11:22):

I didn't want to take too much time from the WG for survey-related topics, but sure we can allocate more time, and if we manage to finish the discussion more efficiently, we can always reallocate.

view this post on Zulip Maxime Dénès (May 31 2022 at 11:26):

I meant not so much about the survey, but the renaming.

view this post on Zulip Maxime Dénès (May 31 2022 at 11:27):

Sounds to me like a topic which will need a lot of time for discussion, but I may be wrong.

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

The proposed schedule is online: https://github.com/coq/coq/wiki/Next-Coq-Working-Group

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

Cc @Gaëtan Gilbert

view this post on Zulip Maxime Dénès (Jun 01 2022 at 12:01):

I guess a significant part of the attendees will have to leave during the afternoon of the 16th, so the idea is to keep the organization of the technical session flexible.

view this post on Zulip Pierre-Marie Pédrot (Jun 01 2022 at 12:02):

Question for the non-locals: where are you staying? Last time we did a CUDW or whatever that was called in Sophia, most people were at the same hotel and it was nicer.

view this post on Zulip Pierre-Marie Pédrot (Jun 01 2022 at 12:02):

I say nicer and not Nice, because it was actually Juan-les-Pins.

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

I am in Antibes, didn't find many hotels around, and Nice can be a long way I heard

view this post on Zulip Pierre-Marie Pédrot (Jun 01 2022 at 12:08):

Yeah, Nice is quite far away. Usually people stick to Antibes or Juan-les-Pins. Sophia is a barren no-man's land so I wouldn't recommend staying there.

view this post on Zulip Maxime Dénès (Jun 01 2022 at 12:12):

I'd say it depends if you have a car. Staying at the Moxy hotel like Michael does, if you have a car or can be transported, looks very reasonable.

view this post on Zulip Michael Soegtrop (Jun 01 2022 at 16:12):

@Pierre-Marie Pédrot : I am staying at the Moxy close by (@Enrico Tassi recommended it).

view this post on Zulip Enrico Tassi (Jun 01 2022 at 19:26):

These days Inria is not the land of wild bores anymore (although they some times still show up at night). You have a few restaurants/bars, a super market, post office, pharmacy etc at walking distance (https://www.google.com/maps/place/Casino+supermarket+and+drive/@43.6178105,7.0713571,16.75z/data=!3m1!5s0x12cc2a85fdb64b29:0x51973583d01330ac!4m13!1m7!3m6!1s0x12cc2b1976147919:0x81c6d85aa9a40d8!2sSaint-Philippe,+06410+Biot!3b1!8m2!3d43.617955!4d7.066923!3m4!1s0x12cdd4ca212b1f91:0xd78731fb68ef07ae!8m2!3d43.6177625!4d7.0752006) so you can safely forget you toothbrush. Sure, Antibes is nicer, but it is 30 minutes of bus away.

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

Which room are we meeting?

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

Ok never mind I see It is in Kahn, I'm in the 230 so should arrive before first session

view this post on Zulip Enrico Tassi (Jun 15 2022 at 07:59):

Highway is free, you should roll fine

view this post on Zulip Maxime Dénès (Jun 15 2022 at 07:59):

Yes, Kahn. You can ask at the "poste de garde", they will tell you.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 16 2022 at 08:06):

Almost there


Last updated: Feb 05 2023 at 23:30 UTC