CRGTCoq20100113

root edited this page Oct 11, 2017 · 3 revisions

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 ?
Clone this wiki locally
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.