CoqWG20150106

Organization

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

Participants

Bruno Barras, Yves Bertot, Pierre Boutillier, Pierre Courtieu, Pierre-Évariste Dagand, Maxime Dénès, Hugo Herbelin, Marc Lasson, Guillaume Claret, Guillaume Melquiond, Pierre-Marie Pédrot, Matthieu Sozeau, Arnaud Spiwack, Enrico Tassi, Andrew Tolmach.

Talks

Pierre Courtieu: how to do better than manually naming hypothesis

I always thought that naming my hypothesis by hand was the best way to write script, then I realize that when changing a definition in a development I had to shift hypothesis names, add new names everywhere in my script. Even if the main part of the script was ok after that, this first step was still painful. I will show how a very simple user directed automatic naming scheme for hypothesis made my life easier. The current implementation is in Ltac and not general enough but it should be easy to make something nice if implemented in ocaml, if you think it is worth it.

Marc Lasson: A new parametricity plugin for the coq proof assistant

During this talk, I will present the implementation of a new plugin for the coq proof assistant. It implements the parametricity transformation which allows to generate the logical relations of parametricity as well as the proof that all terms satisfies these relations. Both the proofs and the relations are defined by induction over syntax. I will introduce the various functionalities of the plugin through concrete examples of practical applications.

Talking points

Policy for pull requests: anonymity required? need for at least two reviews? guaranteeing answering delays?

• Anonymity may raise legal issues. INRIA lawyers may help in answering the issues about anonymity.
• It is suggested that pull requests reviewed by at least one person knowledgeable of the corresponding part of the code is enough for acceptance. This does not prevent that other opinions express a posteriori.

Library/contribs: editorial board? community managment? licensing? (suggested by B. Spitters)

The developers support the idea but with which model?

• An editorial board asking for expertise from external reviewers as in a journal?
• An editorial board doing the reviews itself?
• In any case, we would need volunteers for an editorial committee
• The discussion is postponed

Policy: have code that does not require a particular OCaml version to run

(see One-liner segfault)

Things done so that compilation with OCaml from 4 years ago (roughly the life span of a stable installation), namely 3.12, is supported for 8.5.

Emit a warning for nested Lemma and the like

Discussions with pros and cons. It seems that it is more burden than advantages. Warning ok for 8.5 if done before branching. Otherwise 8.6.

Discussion about nf_constraints + async proofs

Matthieu and Enrico solved this problem.

Require inside modules now forbidden

This is validated.

8.5 release

• Type classes: Local vs Global (to be addressed for 8.6)
• coqchk bugs: to be addressed between beta and final
• .vi will be renamed to .vio
• fail / lazymatch (accepted)
• Fragility wrt to order of evars (nothing possible now): going back to previous order for 8.5
• Reminder that US rather than British spelling is the rule in Coq code and documentation

Roadmap

• Prepare the tarball for the 13th, Enrico will do the Windows package, release just before the CoqPL workshop
• Branching to be done when the bench is stabilized and at latest on the 12th of January
• After 8.5 branch is created, 8.5 fixes are committed to 8.5 and git-merged to trunk, other changes to trunk
• 8.6 beta release targeted for 2015, so that to avoid the available-now or wait-two-years effects.