-
Notifications
You must be signed in to change notification settings - Fork 22
4 October 2018
- termination of rules in iProverModulo files? (G. Genestier, G. Burel)
- reduction engine competition (François)
- performances of lambdapi on ZenonModulo files (Rodolphe, Bruno)
- new release of Dedukti?
- SizeChangeTool in lambdapi (G. Genestier)
- confluence checking in lambdapi?
- rewriting modulo AC in lambdapi? (Gaspard)
- tactics in lambdapi (Aris, Franck)
- interface for lambdapi (Emilio)
- internship proposals
- Performance entre la nouvelle et l'ancienne syntaxe ?
- Tout basculer vers la nouvelle syntaxe ?
- Est-ce qu'on porte les outils que François a développé dans se thèse vers la nouvelle version de Dedukti ? Combien de temps cela va prendre ?
- Prochaine release de Dedukti bloqué par François. La dernière release avant le passage à Dedukti 3.0 (lambdapi)
- Guillaume n'a pas beaucoup avancé sur le passage du termination checker vers lambdapi
- Il faudrait brancher un confluence checker sur la signature de Dedukti
- Franck prévoit de développer une librairie d'arithmétique avec le set de nouvelles tactiques développé en lambdapi
- Les tactiques implémentés pour le moment : (intro ; refine ; apply ; refl ; symmetry ; rewrite). Sur le court terme, la tactique induction serait implémenté.
- L'interface "ça va". Émilio propose un stagiaire pour gérer le protocole "lsp" avec Dedukti pour emacs. Émilio a proposé ce matin un nouveau paquet : "lambdapi-lsp". Rodolphe se propose de développer un prototype basique pour emacs.
Quelques dernières PR à merger avant de faire la prochaine (et dernière) release de l' "ancien Dedukti".
Se pose la question de l'avenir des outils développés par François, sachant que le temps lui est compté. François a besoin d'une API bien précise pour faire marcher ses outils (Universo, DkMeta, ...). Faut-il créer la même API dans le "nouveau Dedukti" ? La charge de travail est estimée à quelques jours. -> François et Franck se portent volontaires pour créer les features manquantes à lambdapi (règle de réécriture nommées, réécriture paramétrable, etc) et porter ces outils dans lambdapi. -> François doit d'abord finir ses softs, cleaner le code et le commenter.
Syntaxe: Faut-il garder l'ancienne syntaxe et continuer à être capable de la parser ? Faut-il migrer tous les outils, tous les traducteurs vers la nouvelle syntaxe qui sera la seule à être supportée ? La nouvelle syntaxe utiliser un parser expressif qui explose en complexité sur des exemples très gros (fichiers générés).
Gilles: intérêt à avoir deux syntaxes:
- une "user friendly", très riche pour l'écriture manuelle de preuves.
- une autre très rapide pour supporter les fichiers de preuves générés. Ne pas garder deux syntaxes par flemme.
Travail de séparation de l'intelligence interne à l'algo et de la représentation des termes fait. Problèmes d'installation de lambapi qui ont freiné le portage. La partie dépendante de la représentation des termes fait ~160 lignes. L'équipe est confiante que ça devrait être facilement porté.
Le travail consiste simplement à printer des règles du lambda-pi vers la syntaxe de la compétition. Rodolphe se propose de s'en occuper.
Les tactiques actuelles (intro, refine, apply, refl, symetry, rewrite) ainsi que les quelques commandes sont déjà assez satisfaisantes et permettent d'écrire manuellement de petites bibliothèques de preuves. Il faut souvent donner manuellement beaucoup de variables qui pourraient être inférées.
Les méta-variables portent actuellement leur type (contextuel) ce qui génère des complexités avec les types dépendants.
L'ensemble de tactiques est satisfaisant. Possibilité d'ajouter une induction.
Puisque les tactiques reposent sur l'existence de définitions particulière de la théorie (égalité de Leibniz, connecteurs logiques, principes d'induction, etc), Gilles suggère de factoriser ces définitions dans un fichier qui serait importé par toutes les théories qui souhaitent pouvoir utiliser les tactiques correspondantes. L'autre possibilité serait de paramétrer les tactiques par le nom des symboles sur lesquels elles reposent. C'est un peu plus lourd.
Discussion: il faudrait développer des outils qui analysent les théories dans lesquelles les preuves sont faîtes et vérifient, au delà de la terminaison / confluence, que les réécritures correspondent à des définitions totales des fonctions, etc.
Développement de l'interface pour Dedukti sous Atom (même si le framework est en bout de vie). Pour l'extension LSP, il est recommandé d'utiliser Emacs ou VSCode. Autres possibilités: Jupiter, Eclipse, etc Rodolphe a déjà un fichier de coloring Vim-mode. La technologie "Lenses" permettrait sous Emacs (mais pas Atom) d'avoir une fenêtre "Goal" qui montre le goal actuel. Les interfaces sont en cours de développement, si Franck veut commencer à développer des preuves il peut utiliser le "hack" qui consiste à afficher le goal courant à chaque étape.
- Proposition de Gilles:
Isabelle pourrait ne pas (ou plus) gérer le format OpenTheory. Nécessité d'avoir une sortie directement dans la syntaxe d'Isabelle. Essayer de faire ce projet en partenariat avec une équipe Isabelle -> prendre un stagiaire allemand (ou autre).
- 2ème proposition de Gilles:
Faire une visite du labo par tous les élèves MPRI de Gilles, Bruno, etc mais aussi d'autres écoles (X, ENS, ENSIIE, M2 FIIL/Orsay). -> Présentation du labo, petits exposés, présentation des sujets de stage, ... -> Opération séduction avec petits fours et cie Plutôt viser des M2 que des M1.