1 March 2018

Générateurs

Krajono fonctionne, François déplace la bonne version de son répertoire personnel vers celui de l'équipe (fait pendant la réunion).
Holide doit sans doute fonctionner, mais aucune des personnes présentes à la réunion n'a testé.

Contrairement à ce qui a été annoncé à la réunion précédente, la commande #NAME est supprimée dans le sens où elle est ignorée au parsing et il n'est plus possible d'avoir un nom de module différent du nom de fichier.
La commande #EVAL qui peut prendre en argument une stratégie et/ou un nombre d'étapes remplace toutes les commandes #WHNF, #SNF, #ONESTEP...
Le #REQUIRE obligatoire viendra, mais dans un second temps, il est décidé qu'il ne fera pas partie de la release 2.6 à venir.

Le dépôt Opam de l'équipe doit être mis à jour avec les versions compatibles de Dedukti, Krajono et Holide, puisque pour l'instant, l'on a au moins ça.

Pour l'instant la traduction de l'encodage de STTForall dans Dedukti vers OpenTheory suivi de l'utilisation d'Holide fait grossir les fichiers d'un facteur 400. C'est beaucoup, mais il n'est pas dans les objectifs proches de faire en sorte d'avoir des traductions inverses l'une de l'autre.
AC serait sans doute intéressant à ajouter dans Dedukti pas seulement pour le polymorphisme d'univers de Coq, mais aussi pour les prouveurs automatiques utilisant la résolution.
Le prochain programme générant du Dedukti que nous aurons à accueillir sera le SMT-solver de Guillaume Bury. Cela constituera un bon test pour évaluer avec quelle facilité nous pouvons agrandir l'écosystème Dedukti.