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)
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.
- 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.
10am-noon
- Renaming (1h, on Wednesday, Matthieu)
- Extensible module system brainstorm (ie how to make things like ltac2 work with functors) (Gaëtan)
2pm-5pm
CEPs, PRs and fixes to discuss:
- Tooltips in CoqIDE, future of the XML protocol
-
Le Repaire, 100 Av. Daumesnil, 75012 Paris
-
Resturant Bon Ga , 6 Rue Montgallet, 75012 Paris
-
L'Alchimiste, 181 Rue de Charenton, 75012 Paris
-
La fille à papa, 28 Rue du Sergent Bauchat, 75012 Paris
-
L'Aubergeade, 17 Rue Chaligny, 75012 Paris
-
Mi Perú, 7 Rue Rondelet, 75012 Paris
-
Le Chasséen, 6 Rue Crozatier, 75012 Paris
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.