Compte-rendu sommaire du GT du 13 janvier 2010
Participants: Bruno Barras, Pierre Courtieu, Julien Forest, Hugo Herbelin, Pierre Letouzey, Matthieu Sozeau, Elie Soubiran
V8.3
- Branchement très bientôt (Pierre fait une dernière correction pour CoRN)
- Annonce d'une V8.3beta sur coq-club avant les JFLA
- D'ici là :
- Documentation par les développeurs (CHANGES + Reference Manual)
- Correction des bugs (Bruno fait une passe et assigne aux personnes concernées)
- Mise en place d'un nouveau test compilant les contribs 8.2 avec la 8.3 pour mesurer le niveau d'incompatibilité
La 8.3 n'aura pas de fonctionnalités vraiment nouvelles à part Groebner qui offre une alternative à Micromega pour la résolution de systèmes d'equations (non linéaires) dans Z et R. La 8.3 offre avant tout des extensions/améliorations du système de modules, des classes de types, des tactiques en général, coqdoc, coqide, ainsi que la bibliothèque MSets et une extension significative de Numbers.
Autres discussions
- Faire de constr un type privé et l'identifier avec kind_of_term ?
- Factoriser les fonctions communes du noyau et de coqchk ?
- Hash-conser systématiquement ?
- Brancher ZArith sur Numbers ?