Compte-rendu synthétique de la journée ADT automatisation du 24 mars 2009

Nombre de participants: environ 25

Questions d'ordre général

Workshop Coq: il a été suggéré de diffuser l'annonce aussi sur les listes TYPES (US), et éventuellement aussi sur les listes des GDR IM et GLP et sur la caml-list.
Coq 8.3: il a été convenu que les développeurs prépareraient chacun d'ici le prochain GT un document annonçant leurs projets des 6 prochains mois pour la 8.3.
Prochaine journée ADT : après vote, il a été convenu que la prochaine journée porterait sur les langages de tactiques (L_''tac'', C-zar, ssreflect, boîtes à outils de tactiques spécialisées, ...), avec éventuellement l'intervention d'extérieurs, et que la journée suivante porterait sur les interfaces graphiques et outils de communication.

L'inefficacité de l'instantiation des modules est bloquant pour le développement (modulaire) de tactiques (cf l'exposé sur Alt-Ergo).
L'utilité de la tactique external est reconnue mais on se retrouve vite face à des limitations dans son utilisation : passage de tactiques ou de commandes non implanté; taille des données XML trop élevée; inefficacité (?) dans l'utilisation de rawconstr en entrée.
L'absence d'un mécanisme solide et clair de réification est limitant : quote ne s'applique pas aux hypothèses, ni à des sous-expressions; la réification via L_tac, comme dans ring est trop lente; les exemples de réification via ocaml devraient être constitués en boîte à outil). Il a été proposé de mettre cette question à l'ordre du jour du prochain GT.
Rappel de l'importance en pratique de l'abstraction des méthodes de décision vis à vis des structures mathématiques sous-jacentes.
Plusieurs autres petites limitations ont été soulignées :
- L'interprétation de L_tac est souvent inefficace
- il pourrait être judicieux de fournir une meilleure API de certaines fonctionnalités L_tac au niveau ML
- mieux partager les sous-termes dans les réifications faites par quote et ring
- réifier les implications dans quote
- système de cache (utilisé par micromega/csdp) trop rudimentaire
- autorewrite inefficace, avec termes de preuve qui mériteraient de partager les contextes dans lesquels les réécritures interviennent