CRGTCoq20100426

Présents : Benjamin Grégoire, Cyril Cohen, Jean-Marc Notin, Stéphane Glondu, Guillaume Melquion, Danko Illik, Arnaud Spiwack, Matthieu Boespflug, Elie Soubiran, Bruno Barras, Vincent Siles, Pierre Boutillier, Maxime Dénès, Hugo Herbelin, Yann Regis-Gianas, Pierre Letouzey

Quelques aspects juridiques liés à Coq

• Hugo a présenté les problèmes juridiques liés à Coq.
• Multi-localisation de Coq (X, Orsay, P7, Cnam, INRIA ...).
• Proposition : signer un accord pour donner un mandat à l'INRIA pour prendre les décisions sur Coq.
• But : fluidifier la prise de décision mais les autres institutions doivent poser leurs conditions.
• Méthode : INRIA va proposer trois types de contrats à PPS, LIX et LRI:
  1. Contrats stratégiques.
  2. Contrats non stratégiques pour les collaborations ponctuelles.
  3. Contrats avec personne physique (soit parce que leurs institutions ne veulent pas s'impliquer ou parce qu'ils font du consulting). Ce dernier aspect semble assez flou: qu'est-ce que le "code écrit le week-end et en soirée" pour un chercheur?
• Conclusion: invitation d'une spécialiste de l'INRIA pour mieux comprendre?

Avenir de la liste de développement Coq-dev

• Vers une liste publique pour le développement?
• Rendre publique le rapport de GT?
• Hugo: pas de sens d'ouvrir coq-dev.
  • Plus de coq-bench sur coq-dev: un serveur web sera mis en place avec un archivage systématique.
  • Pour l'organisation de réunions, pas de sens que cela soit publique.
  • Cocorico : des pages qui pourraient être construites par discussion pour expliquer des aspects techniques plus précis que ce qui se passe sur coq-club. Base d'informations pour les développeurs.
  • D'ailleurs, il est dommage qu'il n'y ait pas d'espace de discussions dans ce wiki.
• Propositions:
  • Rendre publique les rapports de GTs sur Cocorico.
  • Ecrire le compte-rendu en anglais.
  • Compilation de mails coq-club et coq-dev (?) sur des pages Cocorico.
  • Deux solutions :
    1. couper coq-club en deux sous-ML (une plutôt maths, l'autre plutôt ingénierie)
    2. rendre publique coq-dev et avoir un coq-internal/private/team/gt-coq pour les organisations internes ou les discussions privées (chez BSD : core-developpers, developpers, ...)
  • Solution 2 retenue.
• Remarques: coq-bugs fonctionne bien.

Utilisation de Git

Pierre Letouzey : on devrait attendre pour passer au GIT natif la fin de la réflexion menée à l'INRIA sur la nouvelle version de la forge INRIA. Pour le moment, le support par défaut est trop faible (pas de ML, les comptes par défaut n'ont pas assez de permissions, ...)

Nouveau Coqdoc

Yann Régis-Gianas :

• réécrire coqdoc en utilisant des meta-informations fournies par Coq (plus de pseudo-parseur coq dans coqdoc).
• phase d'analyse de besoins pour spécifier la nature de ces méta-informations.

Arnaud : nouveau moteur

• nouveau moteur activé depuis 23 avril
• permet l'ouverture et la fermeture de sous-preuves et offre un mécanisme rudimentaire de puces
• du travail de débogage à faire (cf p.ex. contribs)

Discussion générale sur l'implémentation des tactiques.

• consensus pour aller vers un langage d'implémentation des tactiques plus modulaire.
• Deux directions:
  • comprendre quoi mettre dans ltac pour redéfinir les tactiques actuelles (par exemple ajouter l'unification)
  • recenser les blocs nécessaires à la reconstruction des tactiques actuelles

Benjamin Grégoire : Ajout des entiers natifs et des tableaux dans Coq.

Motivation

Verification des preuves SAT:

Preuve par resolution:

• resolution entre deux clauses
• chaine de resolution : genere une nouvelle clause
• sequence de chaine de resolution : permet de deriver la clause vide

• Les literaux sont represent'es par des entiers.

• Les clauses sont des listes de literaux.

• Un (tres) gros tableau contient les clauses initialles et celles apprisent.

• La trace a verifier est une sequence de chaine de resolution.

  Utilisation intensive des entiers et des tableaux. Pb: Les traces peuvent etre tres grosses. C'est le principal probleme pour les verifiers.

Representation des tableaux

L'ajout des tableaux c'est fait facilement en suivant l'approche mise en place par Arnaud pour les entiers. Pour le kernel un tableau est une liste avec une valeur par defaut (pour la vm un tableau persistant).

Verification des traces SAT en Coq

1 Construire le terme Coq correspondant a la trace. 2 Verifier que la trace est un terme bien type. 3 Verifier que la trace permet de generer la clause vide.

Le point limitant : 2.

Representation actuelle des entiers machines

Un type inductif a un constructeur et 31 arguments booleans. Le compilateur et la vm represente cet inductif (quand tout les arguments sont clos) directement par un entier machine. Mais pas le kernel ==>

application : 3 (tag, fonction, tableau d'arguments) arguments : 1 (tag des tableaux) + 31 (si bien partage) constructeur : ...

Au total il faut plus de 35 mots machines pour representer un entier. Oui, mais on peut les partager (mais le type checker ne gere pas le partage). De plus substitution dans le type non-dependant => introduire un produit non dependant?

Une premiere solution

• Introduire un type inductif a 5000 constructeurs constants, plus un pour la sequence (i.e. base 5000).

• Une fonction de traduction des entier 5000 vers les int31.

  Ce n'est pas tres elegant mais ca marche. Ca ne suffit pas, le type checker est encore un facteur limitant. Different problemes:

  • Pas recursif terminal

    la taille des listes (donc des traces est limite)

    Solution: liste de listes

  • Le type checker realoue les termes qu'il type

    Encore un probleme de consomation memoire

    Solution: Modification (simple) du type checker

    Reduction importante du temps de typechecking Mais encore trop de consommation memoire pour les grosses traces.

Les chaines de resolution sont representees par des listes

taille d'un cons

application : 3 tableau des arguments : 3 (le constructeur cons : 1)

Une solution: reduire la taille des listes

• Nil : L
• Cons1 : A -> L
• Cons2 : A -> A -> L
• Cons3 : A -> A -> A -> L
• Cons4 : A -> A -> A -> A -> L
• Cons5 : A -> A -> A -> A -> A -> L -> L
• Cons10 : A -> A -> A -> A -> A -> A -> A -> A -> A -> A -> L -> L

Ca marche mais encore une fois pas tres elegant.

Decision d'ajouter les entiers natifs et les tableaux directement dans le kernel.

Plus generalement, les types primitifs (et leurs constructeurs)

Avantages esperes:

• Tout le systeme Coq en profite (evaluation lazy), pas seulement la vm. - Representation plus compacte de certains termes (typiquement les certificats des preuves reflexives).

Problemes rencontres:

• C'est un gros travail, le code est peu documente.

Question: Quels autres types primitifs peut-on vouloir: entiers exactes, tuple, string ?

Solution mise en place (travail en cours)

Ajout de deux constructeurs au type constr:

NativeInt of int | NativeArray of constr * constr array

Pour l'instant pas de tableau persistant ... Les primitives sur ces types sont des definitions globales:

• Sans corps (des parametres) mais qui ont des regles de reecritures associees. => Modification des declarations des constant_body:

  Supression du champ const_opaque

  Modification du champ const_body:

  Primitive of prim | Opaque of constr option | Def of constr

Modification des fonctions de reductions

Il y a plusieurs fonctions de reduction utilisant differentes representation des termes (lazy, cbv, vm). Mise en place, d'un module foncteur generique pour la reduction des primitives.

Modification de l'algo de conversion (cas des primitives a prendre en compte).

Quelques remarques

• Ajout des certainnes operations sur les entiers :

  • print_int (ajouter print_char, print_utf8 ?). + operations logique: land, lor, lxor.

• Plus de definitions des primitives

  => les specifications doivent etre totales

• Plus de possibilites de faire du pattern machine sur les entiers et les tableaux (seule les primitives permettent de manipuler ces objets)

  => simplifications du compilateur et de la vm (mais aussi des cases)

Difficultes particuliere pour les tableaux

• Polymorphisme des tableaux (ok ...) - Comment faire pour que le type

  tree :=

  Leaf : A -> tree | Node : array tree -> tree.

  soit accepte?

  • Si p est un tableau de tree sous terme de t, comment faire pour que (get p n) soit un sous terme accepte par la condition de garde (trivial avec type based termination).

Des questions pour vous

• Qui commente son code ? (moi pas beaucoup)

• Beaucoup de representation des termes: constr, fconstr, raw_constr, constr_pattern ... ou s'arreter? - Y a t-il beaucoup d'endroit (hors fonction de reduction) ou

  l'on fait de la delta reduction?

  Certainement dans le refiner et puis ...

Declaration des primitives

Je pense ajouter la declarations des primitives comme actuellement:

• Declaration d'un parametre:

  Parameter add31 : int31 -> int31 -> int31.

• Reconnaisance du parametre comme une primitive:

  Register add31 as add.

Avantage: donne une forme de documentation Question:

• Le systeme doit-il connaitre directement les primitives et leur type - Si oui comment l'implementer? - Probleme avec le type de certaines primitives: besoin de le definition de certain type inductif: bool, pair, carry

Notations

• Pour les entiers pas vraimment de discution. - Notations pour les tableaux: [| def | v0; ...; vn|]