CoqWG 2023 01 31
The next Coq Working Group will take place on Janurary 31-Feburary 01 2023 in Inria Paris (2 Rue Simone IFF, 75012 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:
- Tuesday link: https://inria.webex.com/inria-fr/j.php?MTID=mb77525e91f37b6d6b2fb48f491d93585
- Wednesday link: https://inria.webex.com/inria/j.php?MTID=m4ec39a9329569d4d988f793011f0dc03
Please add your topic, and an estimated duration.
10am-noon (recording)
- Switching to the new Test Suite (Ali) (1h)
- Function to Equations and let-ins (30min, Matthieu)
2pm-5pm: Interfaces (recording)
- (3pm - 5pm) Research topics in UI for interactive provers (2h, remote, J.Bengtson - B.Pierce)
5pm-end of day: Social event and Dinner
- 5pm : Drinks at some local place
- 7:30pm: Dinner, La fille à papa, 28 Rue du Sergent Bauchat, 75012 Paris
10am-noon
- Core team meeting - New members, Renaming (1h, Matthieu, core-team only)
- 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 | No |
| Matthieu Sozeau | Yes | Yes | Yes |
| Théo Zimmermann | Yes | Yes | Yes |
| Enrico Tassi | Yes | Yes | Yes |
| Yves Bertot | Yes | Yes | Yes |
| Pierre-Marie Pédrot | Yes | Yes | Yes |
| Kenji Maillard | Yes | Yes | Yes |
| Romain Tetley | Yes | Yes | Yes |
| Hugo Herbelin | Yes | Yes | Yes |
-
Equations and let-ins:
- Desire to keep the "expected" cbv semantics of definitions, which requires using abstract let-bindings + the inspect pattern.
- Equations should support an expert mode with no inspect pattern introduction, while the default mode adds inspects at each
withandletbinding.
-
core-team meeting:
- Emilio suggest a way to make an interoperable "future" language with the current tactics etc...
- Version numbers? Should it change to natural numbers to reflect the evolution of releases.
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.