CoqWG20140404

Organisation

The WG took place on friday April 4th at Sophie Germain, 3rd floor, in the morning, from 9.30am to noon (coffee at 9am). No talks were given, it was mainly a developers meeting about the status of 8.5 and the remaining issues associated to it.

Talking points

• -R/-I (15min)
• .aux and .native files vis-a-vis Makefiles (15min)
• Guardedness check patch (30min)
• [instantiate] tactic in the new proof engine (30min)
• Survey results (15min)
• Consortium (30min)
• Other issues (30mins-1hour).
  • Locality stuffs : Bug 3206 (Arguments), Bug 3264 (rewrite)
  • ideslave protocol status
• Status of migrating coq web services (if time permits)

Participants

Bruno Barras, Pierre Boutillier, Maxime Denès (remotely), Yann Régis-Gianas, Julien Forest, Hugo Herbelin, Pierre Letouzey, Guillaume Melquiond, Matthieu Sozeau, Bas Spitters, Arnaud Spiwack, Pierre-Marie Pédrot, Enrico Tassi

Guardness

• Maxime implemented a restriction of the guardness criterion in situations such as "f (match c with ... => b end)" which preserves consistency with axioms such as propositional extensionality.
• Discussion on backporting the patch to 8.4 as it happens that requiring the file Ensembles.v, which states propositional extensionality, is inconsistent with the commutative cuts extension of the guard:
  • For 8.4pl4: too late because it has to be made on now
  • For 8.4pl5: Maxime proposes to turns his patch into a warning whenever the extension of the guard which is inconsistent with propositional extensionality is used

Primitive integers

• Native compilation not yet aware that Int31 can be compiled to words. Maxime will do it for 8.5
• Discussion on having primitive integers in the syntax of constr for 8.5. Maxime would prefer to wait for next version

Native compilation

• Do we keep the files .aux and .native as they are: yes

Ideslave protocol status

• Initial communication should be textual and not ocaml marshalling so that e.g. vi can communicate with coq.
• Question about separating the release of CoqIDE from Coq: People developing IDE's should talk (Pierre Courtieu, Thomas Refis, Enrico Tassi, Pierre Letouzey, ...)

Options -R, -I and -L

• Long discussion. Patch from Guillaume Melquiond is accepted.

Tactic "instantiate"

• Tactic "instantiate" does not support instantiation of variables of the context which were not named explicitly. Arnaud will update the documentation accordingly.

Other points

• Paper on Coq: nothing new at this time
• Action de Développement Technologique has been accepted
• Consortium: Matthieu is willing to make progress on the consortium, taking contact with Yves
• Yann asks about making the development of coqdoc asynchronous to the one of Coq

Status of migrating coq web services

• Move to Jenkins for benches
• Pierre B., Matthieu are going to proceed