Pcoq doit fournir des fonctionnalités équivalentes à CtCoq, à savoir un environnement de travail pour le système de preuves Coq.
Cet environnemnt de travail est basé sur une interface graphique adaptée à l'élaboration et la validation de preuves. Il permet la visualisation simultanée des commandes saisies par l'utilisateur, des buts qu'il souhaite atteindre et des résultats (intermédaires et finaux) obtenus.
Afin de permettre un affichage structuré des commandes, cette interface communique avec un parser.
De la même façon, l'interface communique avec le système de preuves.
Outre l'édition et l'affichage structuré de formules, le système offre une fonctionalité appelée "proof-by-pointing".
L'interface graphique doit reprendre la structuration utilisée dans CtCoq, c'est à dire une décomposition en trois fenêtres principales de l'environnement de tavail :
fenêtre d'édition structurée, contenant les commandes qui vont être envoyées au système de preuves.
Contient les "buts" lors de l'exécution de preuves directes
contient les "résultats"
Ces fenêtres doivent être redimensionnable indépendemment. La fenêtre de commandes ainsi que sa barre de menu associée doivent être "clonable", afin de pouvoir afficher des vues différentes du même document de travail.
Les formules et les commandes sont affichées de manière
structurée.
Représentation graphique des arbres (couleurs, polices).
Sélection d'expression.
| File | |
| Open... | Remplace le script de travail par par celui obtenu à partir partir d'un fichier choisi dans une fenêtre de sélection de fichier. Le fichier est analysé par le parser et on affiche l'arbre corresdpondant dans la fenêtre de commandes. |
| ReOpen | Remplace le script de travail par par celui obtenu à partir partir du dernier sélectionné avec la commande "Open". |
| Save | Enregistre sous forme de texte le script de travail courant dans le fichier associé avec la dernière commande "Open". Si pas de dernière commande "Open" fonctionne comme la commande "Save as". |
| Save as... | Idem Save, mais une fenêtre de dialogue (de sélection de fichier) est ouverte et l'utilisateur doir fournir un nom de fichier. |
| Display | |
| Edit | |
| Selections | |
| Editing-tools | |
| Help | |
Structuration en objets des messages de retour du parser et du système de preuve ; Construction d'objets représentant une structure arborescente (aioli.vtp.Tree) à partir d'un flux de données.
L'interface graphique et le processus de preuves fonctionnent de manière indépendante (2 processus). Ces 2 processus peuvent se trouver sur des machines différentes (environnement distribué).
Ce mode de fonctionnement suggère une communication entre l'interface et le système de preuves au moyens de sockets. Toutefois, on peut également explorer la possibilité d'utiliser les RMI pour envoyer les requêtes à Coq, et d'envoyer les résultats sur un MultiCast Socket, permettant d'avoir plusieur fenêtres de scripts associées au même process Coq.
Remonter les messages d'erreurs jusqu'à l'interface (fenêtres de dialogue).
Possibilité depuis l'interface d'arréter l'exécution d'une preuve. (utilisation de l'interface RMI ?).