Proof Manager
Proof Manager est un outil de gestion d'une base de tests pour des prouveurs SMT. Son existence est justifiée par un certain nombre de besoins au sein de l'équipe qui travaille sur Alt-Ergo. Un tel outil est en effet indispensable pour continuer de faire évoluer le démonstrateur automatique. Son principal objectif est de fournir à l'équipe une plateforme de test pour le prouveur qui soit à la fois efficace et facile d'utilisation. Il joue le rôle de véritable outil de suivi du prouveur en permettant à l'utilisateur d' observer son comportement en fonction des différentes évolutions. Il fait aussi office d'environnement d'exécution et de test, pour rapprocher au plus près l'utilisation du démonstrateur automatique Alt-Ergo qui a vocation à être utilisé sur des séries d'obligations de preuves de plus en plus grandes et complexes.
Pour ce faire Proof Manager permet de gérer une base de benchmarks (obligations de preuves) en regard de différents prouveurs et de différentes versions de ces prouveurs. Il associe à chaque couple (prouver, benchmark) un result qui est le résultat de l'éxécution de ce prouveur sur ce benchmark.
Aperçu des fonctionalités:
- une interface graphique
- permet l'exécution de prouveurs en parallèle (sur machine multi-coeurs/multi-processeurs)
- permet l'exécution distribuée sur un ensemble de machines du réseau
- accès aux résultats (et plus généralement à toutes les données enregistées) à distance
- générer des rapports d'exécution à intervalles réguliers
Son intéret réside dans différents aspects de son fonctionnement :
- Post-traitement
-
Il permet de post-traiter les résultats d'un grand nombre d'exécutions
pour les rendre lisibles et manipulables par un être humain au travers
d'une interface graphique (ou texte). L'utilisateur peut alors
visualiser les résultats par catégorie de benchmarks ou même comparer
plusieurs prouveurs sur une série de tests.
- Éxécution parallèle et/ou distribuée
-
Proof Manager permet aussi de lancer un prouveur sur une suite de
benchmarks. Ces exécutions sont effectuées en parallèle si la
machine possède plusieurs processeurs/cœurs. Si l'utilisateur
travaille dans un environnement distribué, il peut déclarer les
machines qui effectueront les calculs au travers d'un fichier de
configuration et ainsi tirer parti des performances des machines
puissantes qui sont à sa disposition.
- Réutilisation
-
Proof Manager fourni une interface complète
en ligne de
commande, qui donne accès à toutes les fonctions de l'outil
(ajout / suppression de prouveurs, benchmarks, exécution des
prouveurs, etc.). Ce qui permet d'écrire par exemple un script exécuté toutes
les nuits qui :
- Récupère des sources d'Alt-Ergo
- Compile la dernière version (si modifications dans les sources)
- Ajoute le nouveau prouveur dans la base
- Exécute ce prouveur sur tous les benchmarks (ou une catégorie digne d'intérêt comme des tests de non-régression)
- Génère un rapport d'exécution (comparaison avec la version précédente)
- Met en ligne ce rapport HTML