CRGTCoq20131126 - coq/coq GitHub Wiki

Participants: Bruno Barras, Yves Bertot, Frédéric Blanqui, Pierre Boutillier, Thomas Braibant, Arthur Charguéraud, Guillaume Claret, Cyril Cohen, Pierre-Ëvariste Dagais, Lourdes del Carmen Gonzalez Huesca, Pierre Letouzey, Assia Mahboubi, Guillaume Melquiond, Pierre-Marie Pédrot, Yann Régis-Gianas, Gabriel Scherer, Matthieu Sozeau, Arnaud Spiwack, Enrico Tassi

Talks

Demo of the new interactive mode - Enrico Tassi

slides-tassi.pdf (lost attachment)

A Coq Wish List for Scaling Up - Arthur Charguéraud

slides-chargueraud.pdf (lost attachment)

Universe Polymorphism and Fast Projections - Matthieu Sozeau

slides-sozeau.pdf (lost attachment)

How to make a Rooster run fast, on a Camel - Pierre-Marie Pédrot

No slides - to be linked here.

Opam - Thomas Braibant

slides-braibant.pdf (lost attachment)

Miscellaneous discussions

Coq working groups

  • It has been decided that M. Sozeau is responsible for the next Coq working groups, to be held every two months (5 times a year, skipping Summer vacations), time being decided with a doodle sent right after each GT for the following one.

Bugs and pull requests

  • It has been decided to have a bug session every two months (5 times a year, skipping Summer vacations). A rotation will be done for the organization and preparation of the session. Pierre Letouzey will organize the first one in February. Pending pull requests will at worst be dealt with during the bug session.
  • Question is open whether wishes should be posted on Cocorico or on the bug tracker.
  • Some statistics: Pierre B. says there are 10 bugs about MacOS, and 80 bugs since 8.4 is released.

Tentative schedule for 8.5

  • February 2014: alpha release
  • April 2014: beta release and opening of new branch (only bug fixes in trunk between alpha and beta)
  • August 2014: final release

Other issues

  • coq.inria.fr is regularly down: solution could be to move it to Rocquencourt (cf Rocquencourt admins) and get access on the server
  • Consortium: for supporting an engineer, 8 partners with a 10keuros fee are required. Thomas thinks the motivation of Americans is strong enough for a consortium to be settled; Thomas proposes to prepare a poll to better know Coq's users.
  • Patch level releases: Assia urges for conferences such as ITP to release a new 8.4pl; Pierre B. will set up automatic patch level releases
  • International implementation meeting: Matthieu ok to organize a one-week meeting in an isolated place, maybe June or July, possible location: Fontainebleau (owned by Paris-Diderot)
⚠️ **GitHub.com Fallback** ⚠️