CoqWG 2023 01 31
The next Coq Working Group will take place on Janurary 31-Feburary 01 2023 in Paris, room C115 Alan Turing (Building C).
Organizers : Matthieu Sozeau (main), Emilio J. Gallego Arias (local / Paris)
We will use Inria's Cisco webex support. We'll have a test meeting on Monday January 30th between 6 and 7pm if you want to check that you can connect (some installations need an up-to-date H.323 codec).
Link: https://inria.webex.com/inria/j.php?MTID=md599a92cb89038552da5fb97aa0ecb96
Meeting number: 2743 326 5792
Password: kMbQEMPv498
To join from a video system: 27433265792@inria.webex.com or 62.109.219.4 and the meeting number above.
Please add your topic, and an estimated duration.
10am-noon
- Switching to the new Test Suite (Ali) (1h)
- Phasing out funind / phasing in Equations (and let-bindings in Equations) (30min, Matthieu)
2pm-5pm: Interfaces
- (3pm - 5pm) Research topics in UI for interactive provers (2h, remote, J.Bengtson - B.Pierce)
10am-noon
- Renaming (1h, Matthieu)
- Extensible module system brainstorm (ie how to make things like ltac2 work with functors) (Gaëtan)
2pm-5pm: Interfaces
- Vernacular interpretation API (Emilio) (1h)
- Presentation of coq-lsp (Emilio) (1h)
- Brainstorming on libobject CEP and https://github.com/coq/coq/pull/16484 (Discussion)
- Discussion on the future of the various interfaces and documentation tools.
CEPs, PRs and fixes to discuss:
- Tooltips in CoqIDE, future of the XML protocol
- Le Repaire, 100 Av. Daumesnil, 75012 Paris
A classic with a nice lunch menu - Resturant Bon Ga , 6 Rue Montgallet, 75012 Paris
A trendy korean barbecue, with lunch menu
- L'Alchimiste, 181 Rue de Charenton, 75012 Paris
Refined and cozy French - La fille à papa, 28 Rue du Sergent Bauchat, 75012 Paris
A 100% grill au sarment , very nice and modern food - L'Aubergeade, 17 Rue Chaligny, 75012 Paris
Traditional neighborhood bristo, several menus for dinner - Mi Perú, 7 Rue Rondelet, 75012 Paris
Tasty and authentic peruvian food - Le Chasséen, 6 Rue Crozatier, 75012 Paris
Cuisine Française de produits frais
Participants (please register yourself, and note our attendance for both days and Tue dinner / social event)
| Name | Tue | Wed | Dinner |
|---|---|---|---|
| Ali Caglayan | Yes | Yes | Yes |
| Maxime Dénès | Yes | Yes | Yes |
| Emilio J. Gallego Arias | Yes | Yes | Yes |
| Gaëtan Gilbert | Yes | Yes | Yes |
| Guillaume Melquiond | Yes | Yes | Yes |
| Matthieu Sozeau | Yes | Yes | Yes |
| Théo Zimmermann | Yes | Yes | Yes |
| Enrico Tassi | Yes | Yes | Yes |
| Yves Bertot | No | Yes | Yes |
| Pierre-Marie Pédrot | Yes | Yes | Yes |
| Kenji Maillard | Yes | Yes | Yes |
| Romain Tetley | Yes | Yes | Yes |
| Hugo Herbelin | Yes | Yes | Yes |
To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.