CRGTCoq20081118
Étaient présents: Bruno Barras, Stéphane Glondu, Hugo Herbelin, Pierre Letouzey, Assia Mahboubi, Jean-Marc Notin, Matthieu Sozeau, Vincent Silès
Secrétaire: Jean-Marc Notin
Après plusieurs discussions, il a été convenu de créer au sein de Cocorico! un espace privé pour les discussions entre les développeurs de Coq. On utilisera les groupes et les acl pour restreindre les droits d'accès. L'option d'utiliser le wiki sur Gforge a été evoquée, puis finalement abandonnée car celui-ci ne permet pas une gestion fine de la visibilité des pages. Certaines discussions commencées sur la mailing list coq-dev seront reportées dans le wiki (JMN).
Pauillac ne sera bientôt plus accessible directement depuis l'extérieur. Il est donc envisagé de transférer les listes de diffusion coqdev et coqclub vers les serveurs inria (sympa). Le transfert devrait se faire de manière automatisée. Néanmoins, les profils des utilisateurs seront a priori perdus.
Hugo estime difficile de figer la programmation des réunions 3 semaines à l'avance (ce qui faciliterait la venue des développeurs non-parisiens intéressés). L'alternative qu'il propose est de mettre en ligne les propositions d'ordre du jour sur le wiki pour permettre aux développeurs non-parisiens de Coq de manifester leur intérêt pour les thèmes proposés.
D'une manière générale, le nouveau site web de Coq est plus esthétique et plus pratique que l'ancien site. Quelques lacunes ont néanmoins été soulevées:
- les bandeaux prennent trop de place, ce qui restreint significativement la zone de contenu pour les résolutions basses;
- le menu de droite se trouve souvent au-dessus du texte (c'est le cas pour coq-bugs et pour les contributions utilisateurs)
- Hugo voudrait faire quelques modifications ponctuelles (crédits, ...)
Il a été convenu que le site pouvait être rendu officiellement public, et que les modifications pourraient être faites après la mise en ligne du site.
Actuellement, les liens vers les .css dans les fichiers .html engendrés par la compilation de la documentation de Coq (refman, stdlib, etc.) sont externes. La bonne visualisation de la documentation générée localement nécessite donc une connexion Internet permanente. Ce problème devra être résolu dès lors que les styles du nouveau site web seront stabilisés (et avant la sortie de la 8.2).
Par ailleurs, Matthieu s'inquiète de l'impact de ses modifications dans coqdoc sur la documentation de la librairie standard. La dernière version en ligne (compilée avec Coq 8.2beta4) ne semble pas présenter de problème. Une attention particulière devra être portée à cette partie de la documentation avant la sortie officielle de la 8.2.
Il y a actuellement 2 types de fichiers de test dans la test-suite:
- d'une part ceux relatifs à une fonctionnalité précise de Coq (unification.v, rewrite.v, ...)
- d'autre part, ceux liés à un bug (1993.v, ...) (Hugo rappelle à ce propos que chaque développeur qui analyse ou corrige un bug est invité à ajouter un fichier de test relatif au bugs dans la test-suite)
Le problème est que les fichiers numérotés ne permettent pas d'identifier directement le composant concerné (et donc le responsable). Il est donc suggéré que lors de la création de tels fichiers, la première ligne soit un commentaire contenant des mots-clé ou un description succincte du bug. Cette ligne sera affichée par coqbench lors du compte-rendu journalier.
Hugo soulève le problème que, pour les messages d'erreur de plusieurs phrases, une confusion est possible entre le '.' de la ponctuation, et le '.' des identificateurs. L'usage courant est de rajouter un espacement entre un terme et le '.' de la ponctuation finale de la phrase. Ex: «Reference not found Foo.Bar.Toto .»
Pierre a récemment intégré CompCert aux contributions utilisateurs de Coq. Un certain nombre de modifications de Coq avait provoqué une perte d'efficacité significative dans ce développement. Pierre a identifié les grosses sources d'inefficacité (les contraintes d'univers, les tactiques fequal et eauto). Après modifications, la différence de temps de compilation entre 8.1 et 8.2 a été ramenée à +14%. Pour plus d'information, voir le message de Pierre en rapport au bug 1896. Par ailleurs, Assia a relevé une différence du même ordre de grandeur avec Ssreflect (+20%).
Pour détecter plus facilement les problèmes liés à l'efficacité, Coqbench pourrait être amélioré pour générer des alertes lorsqu'une contribution voit son temps de compilation évoluer de manière trop brusque. Il serait également intéressant de pouvoir accéder aux temps de compilation de chaque fichier d'une contrib, pour mieux localiser les sources d'inefficacité. En outre, les graphes générés actuellement pour rendre compte de l'évolution du temps de compilation des contribs n'est guère exploitable.
Actuellement, la syntaxe des modificateurs Local/Global n'est pas homogène. Deux variantes existent:
-
Local Notation, qui est plus esthétique; -
Notation Local, qui est plus facile à parser.
D'une manière générale, c'est la variante #2 qui est utilisée (ex. Notation Local...) L'idéal est d'aller vers la solution 1. Bruno a proposé de regarder ça. Dans tous les cas, l'uniformisation devra être faite pour la 8.2.
L'impact de la modification pour les développements n'est pas énorme: après un parsing grossier, une centaine d'occurence de Toto Local ... apparaissent dans les contribs, et ce dans un nombre restreint de contribs.
Une discussion s'est amorcée autour des tactiques assert et specialize. La dernière étant un raffinement de la première, la question s'est posée de ne garder que assert pour éviter la multiplication des noms de tactiques.
Dans certains cas, on peut être confronté à une différence notable entre la conversion utilisée au niveau des tactiques et celle du Qed. . Le phénomène est lié à des problèmes de transparence des sous-termes de preuve.
Matthieu a rapporté un problème rencontré avec vm_conv, lié (?) au fait que refine ne se comporte pas comme Definition pour les contraintes de types données par l'utilisateur.
Pierre a soulevé le problème de l'uniformisation de la syntaxe des classes de types par rapport à celle existant pour les structures (Record ...).
Avec l'arrivée des classes de types dans Coq, il devient nécessaire d'étendre la syntaxe des lieurs pour permettre de spécifier si un paramètre est implicite, généralisé, ou implicite et généralisé. Les contraintes sont diverses et nombreuses: il faut que cette syntaxe soit légère, intuitive, cohérente avec les systèmes existants, compatible avec de futures extensions de Coq (par exemple, la syntaxe [x] est utilisée dans le Calcul des Constructions Implicites).
La discussion a été longue, et les propositions nombreuses. Aucune décision n'a été prise, si ce n'est de continuer les propositions via le wiki (cf CoqDevelopment/SyntaxeDesLieurs).
La syntaxe proposée au départ est la suivante:
- les
{ .. }sont utilisées pour les lieurs implicites; - ` est utilisé pour les lieurs généralisés
Ce qui donne:
<table><tr><td> x </td><td> variable dont le type est à inférer </td></tr>
<tr><td> (x:T) </td><td> variable avec type contraint </td></tr>
<tr><td> {x} </td><td> (={x:_}) variable implicite </td></tr>
<tr><td> {x:T} </td><td> </td></tr>
<tr><td> (x:T) </td><td> variable généralisée </td></tr>
<tr><td> {x:T} </td><td> généralisée implicite </td></tr>
</table>
Il manque (pour les classes de types) une notation pour `{_:T} .
Cette syntaxe pourrait être étendue au niveau toplevel, pour permettre d'écrire: Definition t := `body. ou Goal `formule.
To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.