-
Notifications
You must be signed in to change notification settings - Fork 635
CoqWG 2023 01 31
Guillaume Melquiond edited this page Jan 18, 2023
·
66 revisions
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
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 |
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.