12 April 2018

Ordre du jour

• The OpenStack platform of Inria Saclay (Yacine and Guillaume Burel)
• Regeneration of Zenon proofs from the BWare problem database (Yacine)
• Regeneration of Dedukti files from the previous Zenon proofs (Yacine)
• Regeneration of Dedukti files from iProverModulo (Guillaume Burel)
• Make a new release of Dedukti
• Put Dedukti on the official Opam repo (Rodolphe)
• Performance comparison of Dedukti and Lambdapi (Rodolphe)
• A new algorithm for type checking rules? How to deal with unsolvable constraints?
• Can we remove the constraint that the arity of a definable symbol should be fixed?
• AC, ACU, C, others. When, where, why, how?
• Is a feature to have a standard coding style wanted such as OCamlFormat? If not, then probably revert the commit that introduces this. (François)
• Change syntax request: have each rule separated by a dot (Frédéric)

OpenStack

Les services informatiques de Saclay nous ouvrent l'accès à un serveur de calcul: Gulliver.

• possibilité de créer jusqu'à 30 machines virtuelles
• 50 CPU, 125 Go de RAM, 1 To de stockage disque dur
• Accès en SSH aux VM
• Création et configuration des VMs depuis une plateforme

Ce cluster est plus performant que notre ancienne solution, Frogstar. Il est également mieux accessible depuis l'extérieur et semble donc être une solution plus pérenne. Attention cependant: aucun backup du disque dur ! Nécessité de rapatrier les fichiers générés que l'on veut conserver.

2 VM ont déjà été mises en place pour l'instant (Zenon modulo et iProver modulo). A priori ces machines sont dédiées au travail sur les générateur éponymes.

Pour utiliser le cluster, deux solutions:

• créer un compte sur une des machines existantes (mais nécessité de se partager le temps de calcul sur une machine donné)
• créer une nouvelle machine avec les 6 CPUs restants

Dans les deux cas, la connexion nécessite d'envoyer sa clef SSH via le helpdesk d'INRIA. Pour plus d'information sur cette démarche, s'adresser à Guillaume Burel.

Zenon

Zenon tourne actuellement : utilise 28Go de RAM et prends environ 2min par fichier. 312 nouveaux fichiers ont déjà été générés par rapport à l'ancienne bibliothèque ! 34 nouveaux fichiers générés en utilisant 56Go de RAM et 10mn de temps pour chaque fichier ce qui nous fait 10357 fichiers dans la nouvelle bibliothèque.

Se pose la question de l'export des fichiers générés:

• Quelle technique de compression ? Pour un grand nombre de fichier générés au compte goutte, Rodolphe suggère de zipper chaque fichiers et des les ajouter au fur et à mesure dans une archive .tar.
• Où les héberger ?
  • Sur Github ? limite contraignate de 50Mo par fichier.
  • Sur le site de l'équipe sur gforge ?
    • A vérifier: peut-être aucune limite de fichier.
    • A vérifier: le débit de téléchargement/téléversement est-il correct ?

Regénération Zenon

Tous les fichiers générés actuellement passent avec la dernière version de Dedukti. On rappelle que parmi les anciens fichier, 3 fichiers ne passaient pas, or ils passent maintenant.

• La question de savoir s'ils ont été regénérés ou non ne se pose pas car le générateur n'a été modifié qu'à la marge
• Les évolutions de Dedukti expliquent ce changement. -> mieux comprendre

Regénération iProver Modulo

Regénération des fichiers: 3306 passent. Certains ne passent pas mais dans chaque cas le problème est lié à un soucis de confluence (csiho échoue) ou de terminaison (erreurs Dedukti: time out / out of memory)

-> Nécessité d'avoir un vérificateur de terminaison pour Dedukti. Possibilité de se contenter d'un outil au premier ordre vu la forme des fichiers.

Release Dedukti

La condition pour s'autoriser à faire la prochaine release officielle de Dedukti était que tout les générateurs soient adaptés et que les fichiers regénérés soient vérifiés. Maintenant que c'est chose faite, on peut donc faire une release.

TODO:

• Revert le dernier commit de François (cf remarques plus bas)
• Vérifier le code, les tests unitaires
• Envoyer un email pour prévenir dedukti-dev
• Faire une branche 2.6 à partir de master

Dedukti sur OPAM

Une fois que la release sera faite, on pourra également envoyer la branche créée sur le repository officiel d'opam et enfin permettre l'installation de Dedukti directement à partir d'OPAM.

Performances Dedukti vs lambdapi

On a maintenant la possibilité de faire tourner des benchs de Dedukti et lambdapi sur les machines virtuelles du cluster. Actuellement lambdapi est en WIP donc la mise en place est repoussée d'une ou deux semaines.

Etat de lambdapi:

• Problème de divergence de branches à merger
  • Frédéric a une branche proof-assistant avec meta-variables et un algorightme d'unification plus évolué
  • Rodolphe a effectué un travail de nettoyage, correction et intégration des patterns à la Miller sur la branche master en parallèle.
• Niveau syntaxe: "on est pas mal" mais lambdapi introduit la commande REQUIRE manquante dans Dedukti mais qui pourra être introduite (après la release évidemment). D'ici 1/2 semaines, lambdapi devrait être dans un état exactement équivalent à Dedukti.

Type checking des règles:

Dedukti doit assurer la propriété de subject reduction d'une règle quand il l'ajoute.

• le typage du membre gauche entraîne la génération de contraintes
• le typage du membre droit doit être possible et correspondre au type inférer pour le membre gauche
• le typage du membre droit peut "utiliser" les contraintes générées La question est: comment les utiliser ?

Idées:

• Souvent ce sont des contraintes algébriques.
• On souligne la nécessiter d'élaborer les contraintes: quand f est injectif, il faut remplacer f(t) = f(u) par t = u
• Possibilité d'orienter la théorie équationnelle sous-jacente et de l'utiliser dans le typage du membre de droite pour décider la convertibilité des types.

Notes sur l'algorithme actuel (deux PR en cours sur le sujet)

• Actuellement une contrainte f(t) = f(u) est jetée (ignorée)
• Actuellement une contrainte A = B lève une exception (incohérence avec l'exemple dessus), ne faudrait-il pas simplement émettre un warning ?
• Dans les deux exemples, si f, A et B sont injectifs, on a une preuve que la règle ne sera jamais utilisée (le membre de gauche n'est jamais bien typé). Dans ce cas nécessité d'afficher un GROS warning (ou de fail ?)

Contraintes d'arité

Éliminer les contraintes sur les arités:

• Un même symbole peut avoir des règles d'arités différentes (ex: plus 0 --> x => x). Théoriquement ça devrait poser aucun problème mais limitation simplement pratique: nécessité de modifier un peu les arbres de décision. C'est déjà implémenté dans la branche ACU. Feu vert pour l'ajouter à master (après la release)

ACU

Renouvellement de la volonté de l'intégrer à master: utilité pour CiC, utilité pour Guillaume Bury (?) Projet de le réimplémenter directement dans lambdapi.

• Sur pause pour l'instant en attendant que lambdapi soit stabilisé.
• Roadblock: l’implémentation actuelle repose sur les arbres de décisions par encore implémentés dans lambdapi.

Automatic coding style

Outil de François: A priori remis en cause, il faudrait revert le dernier commit. On préférera définir proprement et précisément le coding style attendu dans un document écrit et inciter les développeurs à s'y tenir. Se référer à la définition des bonnes pratiques de lambdapi.

Remarques de syntaxe

Question du mot clef "def"

Faut-il être def par défaut et déclarer plutôt les symboles injectifs A l'origine ça avait été ajouté pour des questions de modularité (si f est injectif: c'est un contrat: il le restera tout le temps). Par défaut les symboles devraient être définissables. L'injectivité devrait être précisée ([ctor] ?) Eventuellement, un symbole pour préciser qu'un symbole ne peut plus être réécrit.

Ambiguités

Il reste des ambiguïtés de la syntaxe: type des produits ou le type des variables doit être entre parenthèses.

#NAME

Le mot clef #NAME est mort et enterré ! Génial !

Point . à la fin des règles

Les multiples règles groupées derrière un point . sont ajoutées ensembles à la signature et entraînent un unique calcul de l'arbre de décision. Exemple CTT de Bruno : importance du point à la fin des règles. Orientation faisant à peu près l'unanimité (semble-t-il):

• Obligation d'avoir un point à la fin de chaque règle de réécriture.

Contexte des règles

Proposition de supprimer les contextes et de préfixer les variables des règles par ? (nuit peut-être un peu à la lisibilité des règles) Actuellement deux types de variables dans lambdapi :

• Des méta-variables appliquées à un contexte de variables locales x => y => ?F[x] matche x => y => x et pas x => y => y
• Un matching syntaxique: x => y => F x matche x => y => plus y x (avec F ~ plus y) mais pas x => y => plus x y ni x => y => x. Donc a priori le matching syntaxique n'est pas suffisant pour avoir les patterns à la Miller.

A réfléchir

Possibilité de séparer la génération de code et le kernel dans les générateurs. On pourrait donc avoir des générateurs capables de sortir plusieurs syntaxes différentes

Autre remarques

Note: on a beaucoup de branches et c'est un problème quand on veut faire des grosses modification (comme refactoring de tout le code) Branches : tenir la liste des branches à jour et faire l'effort de la réduire (fermer systématiquement les branches PR)

Idée de Frédéric: Ajouter en tête de tout les fichiers générés .dk un commentaire standard avec:

• quel programme l'a généré
• quelle version
• Pourquoi pas aussi: la date de génération