Présents: Bruno Barras, Pierre Letouzey, Pierre Courtieu, Stéphane, Élie, Benjamin Werner, Hugo, et pour le début de la discussion, Assia, Pierre-Yves, Matthias.

Secrétaire: Hugo

Comme on aurait pu s'en douter, la question ssreflect occupa finalement l'essentiel du temps de réunion. L'autre question abordée fut la syntaxe à donner pour la clause "_eq" de destruct.

Pour les questions 8.2 qui n'ont pu être abordées, une nouvelle réunion aura lieu vendredi prochain même lieu même heure (14h au LIX). J'aimerais bien aborder aussi la question de la politique d'utilisation des branches svn.

Sophipolitains, seriez-vous intéressé par ce que la prochaine discussion sur ssreflect se passe à Valbonne ?

Hugo expose les grandes approches possibles :

• ssreflect est considéré comme un plugin distribué indépendamment ;
• ssreflect.ml4 est intégré littéralement à l'archive et la question reste ouverte pour les ssr*.v ;
• le code de ssreflect.ml4 est intégré profondément (chaque fonctionnalité étant installée dans le fichier Coq qui lui est propre) et la question des ssr*.v reste ouverte.

S'ensuit de longues discussions et je me restreins à un résumé :

Il y a consensus sur les questions générales :

• les fonctionnalités développées par ssreflect sont globalement d'intérêt général et souhaitées dans Coq ;
• le travail de maintenance d'Assia doit être facilité.

Au delà les positions divergent :

• Bruno pense qu'il faut intégrer les fichiers dans l'archive mais que le manuel de référence ne doit pas mentionner ssreflect, à défaut de choix de syntaxe consensuels.
• Pierre L. semble considèrer que la coopération avec Math. Comp. est actuellement trop ténue pour justifier en l'état une vraie intégration.
• Pierre C. pense qu'il faut intégrer les fichiers dans l'archive pour faciliter le travail d'Assia.
• Hugo laisse ouverte toute approche qui respecte une totale indépendance de Coq vis à vis de MS.

Sur quelques points précis :

• Benjamin se renseignera pour savoir si en cas d'intégration littérale de ssreflect.ml4, cela peut se faire avec une en-tête standard Coq sous LPGL et un paragraphe explicitant que l'intégration de code financé par MS se fait sur la seule base de la qualité du travail intégré (ou formulation équivalente à discuter collectivement).
• La question de la permissivité des blancs dans les identificateurs (sur lequel repose un triplet de hacks de ssreflect) a entraîné une discussion technique : Bruno défend que le noyau doit reposer sur une notion abstraite d'identificateur et donc ne pas faire de tests de validité ; Pierre C. demande si c'est une question qui doit relever de l'interface et de leur aptitude à gérer des identificateurs avec blancs ou de la spécification du CCI implantée par Coq ; Hugo considère que même si la notion d'identificateur est abstraite dans le noyau, il faut bien spécifier quelque part le type concret avec lequel le type identificateur du noyau est instancié. La discussion n'a pas abouti : des bruits de perceuse !! nous ont obligés à changer de salle et la discussion a repris sur d'autres sujets.
• La question des bibliothèques n'a pas vraiment été discutée. C'est pourtant une question importante. En particulier, Benjamin pose la question : si je veux faire des extensions à la biblio de Coq utilisant les biblios ssr, pourrais-je le faire ?

Mine de rien, cette question rejoint la discussion précédente.

La syntaxe actuellement adoptée par Hugo est :

destruct term_with_bindings as naming_intropattern disjunctive_intropattern

où la présence d'un naming_intropattern est moralement id, pour indiquer qu'on veut garder une égalité de nom id, ou ? pour garder une égalité nommée par Coq, et disjunctive_intropattern est moralement [ ... ] ou ( ... ).

Bruno fait remarquer que la notion d'égalité à garder ne devrait pas être attachée à destruct mais à l'intro-pattern, de telle sorte que dans un intros [ ... | [ ... ] ... ], une égalité puisse être gardée à n'importe quel niveau de destruction.

Pas d'idée de syntaxe trouvée (hors des expressions longues style remembering as) qui, outre leur longueur, se prêtent mal au style symbolique des intro-patterns.

La discussion dérive sur les possibilités (théoriques) d'avoir des intro-patterns ['S (S n) => tactic | 'S n | 'O => tactic] dans l'esprit du "match with", avec possibilité de faire un swap des buts au passage.

La syntaxe du let 'pat := t in c est rediscutée sans davantage de meilleure solution qu'avant.

La syntaxe est le lieu collectif dans lequel nous évoluons ce qui en fait une question naturellement sensible. Faut-il aller dans le sens d'une séparation des syntaxes (comme c'est le cas pour le style mathématique de Pierre Corbineau) parmi lesquelles chacun pourrait naviguer selon son humeur, ses besoins ou son esthétisme ou faut-il viser une unique belle pièce commune ?