CoqWG20161214
The Working Group took place on December 14th and 15th at Inria Paris (2, rue Simone Iff). The room was "Jacques-Louis Lions 2" the first day and A215 the second day.
Yves Bertot, Frédéric Blanqui, Pierre-Évariste Dagand, Maxime Dénès, Emilio Jésus Gallego Arias, Georges Gonthier, Hugo Herbelin, Pierre Jouvelot, Matej Košík, Assia Mahboubi, Cyprien Mangin, Guillaume Melquiond, Pierre-Marie Pédrot, Thibaut Sibut-Pinote, Matthieu Sozeau, Enrico Tassi, Théo Zimmermann
- 10:00 8.6 debriefing (Maxime Dénès)
- 10:30 pp_new branch (Emilio Jesús Gallego Arias)
- 10:45 Thoughts on IDE protocols (Emilio Jesús Gallego Arias)
- 11:15 Break
- 11:30 Splitting CoqIDE ? (Emilio Jesús Gallego Arias)
- 11:45 Report on Ltac2 (Pierre-Marie Pédrot)
- 12:30 Lunch
- Afternoon: bug squashing or work in small groups
- 18:30 Social event (location TBA)
- 10:00 Quick review on the organization of the development (Hugo Herbelin)
- 10:15 8.7 roadmap and schedule (Maxime Dénès)
- 10:45 Evar-insensitive terms (Pierre-Marie Pédrot)
- 11:00 Break
- 11:15 Thoughts on Hints, Typeclasses, Sections & Namespaces (Matthieu Sozeau)
- 11:45 New Deriving plugin opportunity, apart from Equations (Matthieu Sozeau)
- 12:00 A new benchmark infrastructure (Matej Košík)
- 12:15 Lunch
- Afternoon: bug squashing or work in small groups
Bonus: Some bottles to drink at some time to celebrate the 8.6 release
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.