CRGTCoq20090116

Compte rendu du GT Coq du 16 janvier 2009

Participants: Arnaud, Élie, Hugo, Jean-Marc, Matthieu, Pierre L., Stéphane, Tom, Vincent G., Yves.

For 8.2, Hugo observed that the archive de facto gets more stable and asks whether the time is ready for releasing the final 8.2 [21/1/09 addition: specific 8.2 known bugs that can reasonably be treated in a short delay have been taken into account].

Stephane asks if the syntax is now stable? The syntax is settled. Especially, Matthieu changed the notation of classes so that it requires curly braces as in Record.

Currently when you define a record, you have to be careful to avoid making a truly inductive type. Arnaud wants the modification that it will be impossible to define an inductive type [21/1/09: done].

Hugo implemented the proposal that "Local" or "Global" are prefix modifiers for state changing commands, with the meaning that "local" will imply local to the current section (when in a section) or the current file (when not in a section). For now Local is not supported for Definition, using Global inside a section might be used for forcing discharge, but this is not implemented.

For instance "Local Notation" now replace "Notation Local" and the latter is warned as deprecated.

Legacy ring is scheduled to become a user-contribution,

Question about coq-interface and parser, can they be removed. The answer is probably.

Then it is suggested that all parts of a tactic should be given at the same place: the parsing, the prettyprinting, a little documentation, etc... Maybe every tactic declaration should be done using a camlp4 directive TAC_EXTEND.

Pierre Letouzey inserted a few differences in FSETS during the holiday break.

Beware that the documentation should be viewable off-network and the documentation should not contain any hard-link to a full URL. This is to be done by Jean-Marc for the release.

Where should the new big numbers be documented. There is also the numbers module hierarchy [21/1/09 addition: the main current documentation is the stdlib page on the coq site].

Question about compiling the documentation. About getting rid of too many messages when compiling this documentation, either messages from Latex or messages from hevea, but then the question is pushed aside as not important for the release of 8.2 [21/1/09 addition: HH applied an experimental output filter to improve the readability of doc compilation messages].

Problem with the {| a := True; b := False |} notation, which is as it is (instead of { a := True; b := False }) for parsing reasons.

Make sure that coqtop -version gives the information about which ocaml was used to compile, what version of the sources, etc... But avoid that the binary changes everytime the revision changes. HH proposal to move the revision file to .ml file should be reverted. Instead the textual revision file should be installed so that -version knows about it. Necessary informations are VCS and compilation date. The problem is not really with developers, but with occasional followers of the trunk. Compilation date is currently not accurate (HH's mistake?) and should be fixed.

Jean-Marc plans to install the new Coq server (with virtualization and ethernet reboot) within a one-month delay. It has been decided that the new web site will be activated when the new server will be up. The server will be located at Polytechnique so as to be in the place in case of problems (see the recent failure to take care of logical.saclay.inria.fr by the Parc Club's staff).

In the meantime, it has been decided to make the new site more visible by moving the link upwards to the top of the home page of the old site.

Explanation about using git. An interesting point is that everybody can start using git without changing the main repository, by relying on git-svn.

Protocol for the release

We publish and announce (on coq-club, see Damien's announces for OCaml RCs) a release candidate (RC) next Wednesday, in source-only form [21/1/09 addition: an extra day delay is given for MS and JMN ending ongoing fixes and HH preparing the release files]. That means a tag in the svn, and publication of a source tarball. Then commits are frozen in the 8.2 branch. Only packaging-related changes (including documentation) are allowed. Basically, no changes in .v or.ml* files. No correction of bug unless they really hinder compilation or basic usage (keep them for patch levels). Otherwise said, the diff between 8.2rc1 and 8.2 should ideally be only the version number. Most likely, there should be changes only in Makefiles, documentation or such. Ask for feedback (positive or negative) directly on coq-club, in reply. Two weeks later (around February 6th), we release 8.2. The final release announce can mention main changes from 8.1, and (separately) changes from the RC.

This should leave time to make binary packages (including the official ones from INRIA) and have them tested (of course, people might not have the time to migrate their developments, but they should be able to start with the RC). Binary packages for the RC can be announced in reply of the RC announce.

Concerning binaries (ideas from Stephane): we provide them only for Mac OS and Windows, and we provide only a source distribution for other unices. In Stephane's humble opinion, it doesn't make sense (it can even be troublesome), to provide binaries for Linux.

Each distribution has a page on its website for each package, we should provide a link to them, for example:

http://packages.debian.org/coq http://packages.ubuntu.com/coq https://admin.fedoraproject.org/pkgdb/packages/name/coq

Moreover, a wiki page should be set up so that external people provide links to other binary packages (emphasizing that these are external contributions, not "official" INRIA stuff).