CRGTCoq20110414 - coq/coq GitHub Wiki

Participants: Arnaud Spiwack, Assia Mahboubi, Guillaume Melquiond, Hugo Herbelin, Matthieu Sozeau, Pierre Boutillier, Pierre Letouzey, Stéphane Glondu

Native int and array (Benjamin Grégoire)

• no information from Benjamin; missing features (though not mandatory): fixpoints over arrays, support for extraction

Native compilation (Mathieu Boespflug, Maxime Dénès, Benjamin Grégoire)

• no information; open questions on the soundness of the compilation of fixpoints and cofixpoints

Restructuration library of numbers in trunk (Pierre Letouzey)

• coqdoc is not powerful enough to render the content of a module
• ZArith bigger and its Require is longer

Uniformization of the library of numbers (Pierre Letouzey's branch)

• change of Pcompare, "?=" bound to the binary Pcompare instead of the ternary one.
• moving N and Z to the initial state (would forbid using them as unbound names in "`" command); Assia asks for first checking that it does not break other behaviours such as scopes, notations, ... involving N
• moving "plus" to "add", "mult" to "mul"
• robustness check wrt contribs to be done

Containers library (Stéphane Lescuyer's type classes based finite sets)

• Pierre ready to integrate the library for 8.4 (size is 20kB)

Ergo (Stéphane Lescuyer)

• one axiom was still unproved; otherwise Guillaume thinks it would be a very good thing to integrate it (size is 20kB)
• Guillaume ready to maintain ergo

Rebuilding a library of structure over classes

• Challenging but probably too complex for 8.4

8.4

• Efficiency
  • Pierre L: various improvements of efficiency in loading vo files
  • Pierre L: various improvements of evar handling
  • At the end, efficiency comparable to the one of 8.3
• Arnaud's to-do list for 8.4
  • completing port of declarative mode
  • bullets (with ability to bound user-level semantics)
  • solving anomalies when goal is non-existent
• Summary of coqide process separated from coqtop in 8.4
  • Pierre L: Ctrl-C now working on Unix (but not work under windows)
  • Pierre L: coqide now 3MB only
  • Pierre L: printf not to be used so as to be able to avoid needing a terminal window in parallel to coqide
• File headers: To check with INRIA on how to do them properly
• camlp4/camlp5
  • 8.4 supports both
  • To do: understand why camlp4 issues warning while camlp5 does not
• Status of contributions compilation:
  • Interfaces: it is suggested that the "description" file be removed and therefore that the contrib stopped being released (an alternative is also to remove it)
  • CoRN: Qed w/o beta-reduction in sections introduces artificial dependencies
  • Ssreflect: ongoing problems with bullets and unification in progress
• Minor ongoing changes
  • evars, unification, classes de type (Matthieu)
  • evars, filtrage d√©pendant, notations (Hugo)
• Suggested release timetable
  • recommended contents: containers, native int and arrays (but waiting for more information), native compilation (but waiting for more information), ergo (if someone can prove the axiom), new numbers library naming scheme (majority in favor)
  • decision on contents with steering committee on Apr 22
  • first weeks of June: creation 8.4 branch + release 8.4beta

8.3pl2

• Many corrections made since 8.3pl1: ready for tagging the next day the Ssreflect and MathClasses bench problems are solved

Integration of patches from outside

• Clarify again the situation with INRIA's intellectual property service
• In the meantime, acknowledging the patch's author in commit log (code becomes LGPL)

Windows packages

• grammar.cma to be added
• Assia says that Pierre-Yves Strub has a bundle (with Emacs, PG, ... but not CoqIDE)
• Pierre says: 8.4 Coqide will not be fully functional on Windows (Ctrl-C missing)

MacOS packages

• Pierre B: has the technology to prepare a ssr package for MacOS

In case of move to git

• who is allowed to push or who is handling push requests?
• how to protect against history destruction?
• which server:
  • github for its tools (visualisation, ...)
  • inria's forge for being a priori more trustful