CRADT20090324

root edited this page Oct 11, 2017 · 5 revisions

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

see http://coq.inria.fr/adt/journee-automatisation.html

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.

Questions d'ordre « technologique » liées au développement de l'automatisation en Coq

  • 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 Ltac, 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 Ltac est souvent inefficace
    • il pourrait être judicieux de fournir une meilleure API de certaines fonctionnalités Ltac 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
Clone this wiki locally
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.