CRADT20090324
see http://coq.inria.fr/adt/journee-automatisation.html
Nombre de participants: environ 25
- 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 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
To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.