CoqWG20161214

root edited this page Oct 11, 2017 · 5 revisions

Organization

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.

Participants

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

Schedule

14/12/2016

  • 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)

15/12/2016

  • 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

Clone this wiki locally
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.