CoqWG20150708

Organization

The WG was held in Paris on July 8th at PPS, Sophie Germain, 10am.

Participants

Yves Bertot, Maxime Dénès, Hugo Herbelin, Guillaume Melquiond, Pierre Letouzey, Cyprien Mangin, Pascal Manoury, Thomas Sibut-Pinote, Matthieu Sozeau, Enrico Tassi.

Talks

• Pascal Manoury: An ordinal measure for proof termination (diapos: gtcoq.pdf (lost attachment))

Talking points

• Pull requests from the CoqCS

  • Most pull requests are for trunk, and this is postponed

• Document opam archive / contribs on Coq's www

  • Constatation of some progresses
  • Majority against guaranteeing that submitted packages will be maintained from one version of Coq to the other: the idea is that the developers will do "best effort"

• Status of v8.5

  • we shall do a beta3 and Matthieu is appointed responsible of the finalization of the 8.5
  • reminder: only bug fixes to be committed in 8.5 (e.g. f_equal to be solved for 8.6)
  • developers shal mark in documentation and CHANGES their features which are not stable yet (e.g. universe polymorphism)

• Reflections on development organization (Yves Bertot)

  See [https://pad.inria.fr/p/QkAmQ3AzUMNB1WaK_Devenir-Coq].

• Miscellaneous

  • Mail traffic from github: we shall use a specific list, different from coqdev
  • Discussion about sympa for coq-club: search is painful, no indexing; a possible alternative is to use gmane.
  • discussion about a few committing rules:
    • to start commit messages by a 80-line description followed by a blank line; the body of the commit message comes after (idea: will serve for the change log)
    • no constraint on removing spaces at end of lines
    • avoid obfuscating a semantic change with syntactic changes (which cannot be hidden with "git diff -w")
    • it is recommended to limit the lines to 80 characters in files
  • use of ocamlfind: consensus for following the move of the community towards using it, even though it is not necessary for compiling Coq
  • immutable strings #4278 (skipped)
  • Primitive projection representation (skipped)
  • left2right ref in kernel (skipped)