Prooftree - En ligne dans le Cloud

PROGRAMME:

Nom

prooftree - affichage de l'arbre d'épreuves pour Proof General

SYNOPSIS

arbre à épreuves [Options de ...]

DESCRIPTION

Arbre d'épreuves visualise les arbres de preuve pendant le développement de la preuve avec Preuves Général. Actuellement
ça ne marche que pour coq, bien que l'ajout de la prise en charge d'autres assistants de preuve devrait être
relativement facile.

Pour démarrer un affichage de l'arbre d'épreuves, appuyez sur le bouton Arbre d'épreuves icône dans le Preuves Général barre d'outils ou
sélectionnez l'entrée de menu Preuve générale -> Start/Stop Arbre d'épreuves ou tapez Cc CD (qui court
preuve-arbre-externe-affichage-bascule). À l'intérieur d'une preuve, cela lancera immédiatement une preuve-
arborescence de l'épreuve courante. En dehors d'une preuve, Preuves Général se souvient de démarrer le
affichage de l'arbre d'épreuves pour la prochaine épreuve.

Dans des circonstances normales Arbre d'épreuves est commencé par Preuves Général en tant que Emacs sous-processus.
L'utilisateur interagit avec Arbre d'épreuves uniquement via l'interface utilisateur graphique. Un substantiel
une partie de la tâche de visualisation de l'arbre de preuve est effectuée par Preuves Général. Donc non seulement
le Arbre d'épreuves les arguments de ligne de commande mais aussi d'autres aspects ne peuvent être configurés qu'à l'intérieur
Preuves Général, Voir Preuves Général Personnalisation ci-dessous.

OPTIONS

-help Imprimer le synopsis et quitter.

-config
Ouvrez la boîte de dialogue de configuration au démarrage (si vous souhaitez modifier la configuration
sans commencer Preuves Général).

-géométrie spec
Définit la géométrie X de la fenêtre principale. spec est une chaîne de géométrie X standard dans
la forme xposxoui[+xoff[+yoff]].

-tee filet
Écrire toutes les entrées dans filet (généralement à des fins de débogage).

-debug Fournit plus de détails sur les erreurs.

-aide-dialogue
Ouvrez la boîte de dialogue d'aide au démarrage. Principalement utile pour la relecture du texte d'aide.

PRINCIPAL PREUVE DISPLAY

Arbre d'épreuves ouvre une fenêtre pour chaque épreuve qu'il est demandé d'afficher. Cette fenêtre
contient le graphique de l'arbre de preuve et un petit affichage pour les séquences et les commandes de preuve.

Couleurs
Les branches de l'arbre de preuve sont colorées en fonction de leur état. Arbre d'épreuves
distingue les états suivants.

courant (bleu par défaut)
La branche courante est la branche de la racine de l'arbre de preuve à la branche courante
objectif.

non prouvé (couleur de premier plan par défaut)
Une branche n'est pas prouvée si elle contient des objectifs de preuve ouverte.

avéré incomplet (cyan par défaut)
Une branche incomplètement prouvée a sa preuve terminée, mais certains des éléments existentiels
les variables qui ont été introduites dans cette branche ne sont pas (encore) instanciées.

prouvé partiellement (vert foncé par défaut)
Dans une branche partiellement prouvée, toutes les variables existentielles de la branche elle-même sont
instanciées, mais certaines de ces instanciations contiennent des variables existentielles qui
ne sont pas (encore) instanciés.

avéré complet (vert par défaut)
Une branche est prouvée complète si toutes ses variables existentielles sont instanciées avec
termes qui eux-mêmes ne contiennent aucune variable existentielle.

triché (rouge par défaut)
Une branche trichée contient une commande de preuve de triche, telle que admettre

Les couleurs ainsi que bien d'autres Arbre d'épreuves les paramètres peuvent être modifiés dans le Arbre d'épreuves
Configuration Dialogue (voir ci-dessous).

Navigation
Lorsque l'arbre de preuve grandit, on peut naviguer par divers moyens. En plus de
les barres de défilement et les touches habituelles on peut déplacer l'arbre de preuve en tirant avec le bouton de la souris 1
pressé. Par défaut, faire glisser déplace la fenêtre (c'est-à-dire que l'arbre d'épreuve en dessous se déplace dans
la direction opposée). Après avoir défini une valeur négative pour Faites glisser accélération dans le
Arbre d'épreuves Configuration Dialogue, faire glisser déplacera l'arbre de preuve à la place (c'est-à-dire, la preuve
l'arbre se déplace dans le même sens que la souris).

Séquent Écran
L'affichage de séquence sous l'arbre de preuve montre normalement l'ancêtre de la séquence
objectif actuel. D'un simple clic gauche de la souris, on peut afficher n'importe quelle commande d'objectif ou de preuve dans
l'affichage séquentiel. Un simple clic en dehors de l'arbre de preuve reviendra à la valeur par défaut
comportement. La taille initiale de l'affichage séquentiel peut être réglée dans le Arbre d'épreuves
Configuration Dialogue. Une valeur de 0 masque l'affichage séquentiel.

Outil Tips
Les commandes de preuve abrégées et les séquences sont affichées dans leur intégralité sous forme d'info-bulles lorsque la souris
le pointeur repose sur eux. Les deux, les info-bulles pour les commandes de preuve abrégées et pour
les séquences peuvent être désactivées indépendamment dans le Arbre d'épreuves Configuration DialogueL’
la longueur à laquelle les commandes de preuve sont abrégées peut également être configurée.

Supplémentaire Affichages
Un double-clic ou un maj-clic affiche n'importe quelle commande d'objectif ou de preuve dans un
la fenêtre. Ces fenêtres supplémentaires sont supprimées lorsque la fenêtre principale de l'arbre d'épreuves disparaît,
à moins que leur gluant bouton est enfoncé.

Existentiel Variables
Arbre d'épreuves garde une trace des variables existentielles, qu'elles aient été instanciées et
s'ils dépendent d'un autre existentiel non (encore) instancié. Il utilise différents
couleurs pour les branches prouvées qui contiennent des variables existentielles non instanciées et
branches qui ne dépendent que de certains existentiels non instanciés. La liste des non
(encore) des variables existentielles instanciées sont ajoutées aux commandes de preuve et aux séquences dans
info-bulles et les autres affichages.

Le manuel de formation Existentiel Variable Dialogue affiche un tableau avec toutes les variables existentielles du
preuve actuelle et leurs dépendances. Chaque ligne du tableau contient un bouton qui marque
la commande de preuve qui a introduit cette variable (avec fond jaune, par défaut) et,
si présente, la commande de preuve qui a instancié cette variable (sur fond orange, par
défaut).

Entrée Menu
Le manuel de formation Menu bouton affiche le menu principal. Les Cloner item clone l'arbre d'épreuves actuel dans un
fenêtre supplémentaire. Cette fenêtre supplémentaire continue d'afficher un instantané du cloné
arbre de preuve, peu importe ce qui se passe avec la preuve originale.

Le manuel de formation Afficher actuel l'élément déplace la fenêtre vers l'arbre d'épreuve de telle sorte que l'épreuve courante
l'objectif (s'il y en a) sera visible.

Le manuel de formation Sortie l'élément se termine Arbre d'épreuves et ferme tous les affichages de l'arbre d'épreuves.

Les trois éléments restants affichent respectivement le Arbre d'épreuves Configuration Dialogueet
le Aidez et À propos les fenêtres.

Contexte Menu
Un clic droit affiche le Contexte Menu, qui contient des éléments supplémentaires.

L'article annuler à point est actif sur les nœuds séquentiels dans l'arbre de preuve. Ensuite, il envoie un
rétracter ou annuler la demande à Proof General qui rétracte le tampon de script jusqu'à cela
séquentiel.

Les objets insérer commander et insérer sous-preuve sont actifs sur les commandes de preuve. Ils ont envoyé,
respectivement, la commande de preuve sélectionnée ou toutes les commandes de preuve dans le sous-arbre sélectionné, pour
Preuve générale, qui les insère au point.

CONFIGURATION

Arbre d'épreuves Configuration Dialogue
Les modifications dans la boîte de dialogue de configuration ne prennent effet que lorsque le Appliquer or OK le bouton est
pressé. Les Enregistrer Le bouton stocke la configuration actuelle (telle que marshalée OCaml enregistrement) dans
~/.prooftree, qui écrasera la configuration par défaut intégrée pour les éléments suivants
Arbre d'épreuves s'exécute. Les Restaurer Le bouton charge et applique la configuration enregistrée.

Preuves Général Personnalisation
La localisation de la Arbre d'épreuves exécutable et les arguments de la ligne de commande sont dans le
groupe de personnalisation arbre-preuve. Démontrer des points spécifiques, tels que les expressions régulières
pour la navigation et les commandes de triche sont dans le groupe de personnalisation preuve-arbre-internes.
Pour visiter un groupe de personnalisation, tapez Mx personnaliser-groupe suivi du nom du
groupe de personnalisation à l'intérieur Preuves Général.

LIMITATIONS

Pour coq, les preuves doivent être lancées avec la commande Preuves, ce qui est la pratique recommandée
de toute façon (voir rapport de problème Coq 2776).

CONDITIONS PRÉALABLES

Cette version de Arbre d'épreuves a besoin coq 8.4beta ou mieux et Preuves Général 4.3pre130327 ou
mieux.

Utilisez Prooftree en ligne en utilisant les services onworks.net