Este es el comando prooftree que se puede ejecutar en el proveedor de alojamiento gratuito de OnWorks utilizando una de nuestras múltiples estaciones de trabajo en línea gratuitas, como Ubuntu Online, Fedora Online, emulador en línea de Windows o emulador en línea de MAC OS.
PROGRAMA:
NOMBRE
prooftree - visualización de árbol de pruebas para Proof General
SINOPSIS
árbol de pruebas [Opciones ...]
DESCRIPCIÓN
árbol de prueba visualiza árboles de pruebas durante el desarrollo de pruebas con Pruebas General. En la actualidad
solo funciona para gallo, aunque agregar soporte para otros asistentes de prueba debe ser
relativamente fácil.
Para iniciar una visualización de árbol de pruebas, presione el árbol de prueba ícono en el Pruebas General barra de herramientas o
seleccione la entrada del menú Prueba general -> Start / Stop árbol de prueba o tipo Cc Discos compactos (la cual recorre
prueba-árbol-pantalla-externa-alternar). Dentro de una prueba, esto iniciará inmediatamente una prueba-
visualización de árbol para la prueba actual. Fuera de una prueba Pruebas General recuerda comenzar el
visualización del árbol de pruebas para la siguiente prueba.
Bajo circunstancias normales árbol de prueba es iniciado por Pruebas General como una emacs subproceso.
El usuario interactúa con árbol de prueba solo a través de la interfaz gráfica de usuario. Una sustancial
parte de la tarea de visualización del árbol de pruebas se realiza mediante Pruebas General. Por lo tanto, no solo
el árbol de prueba Los argumentos de la línea de comandos, pero también otros aspectos, solo se pueden configurar dentro
Pruebas General, consulte nuestra página, Pruebas General Personalización abajo.
OPCIONES
-ayuda Imprimir sinopsis y salir.
-config
Abra el cuadro de diálogo de configuración al iniciar (si desea cambiar la configuración
sin empezar Pruebas General).
-geometría especulación
Establece la geometría X de la ventana principal. especulación es una cadena de geometría X estándar en
la forma pos xxypos[+xoff[+yoff]].
-tee presentar
Escribe toda la entrada en presentar (generalmente con fines de depuración).
-debug Proporciona más detalles sobre los errores.
-ayuda-diálogo
Abra el cuadro de diálogo de ayuda al inicio. Principalmente útil para corregir el texto de ayuda.
PRINCIPAL COMPROBANTE DISPLAY
árbol de prueba abre una ventana para cada prueba que se solicita mostrar. Esta ventana
contiene el gráfico del árbol de pruebas y una pequeña pantalla para las secuencias y los comandos de prueba.
Colors
Las ramas en el gráfico del árbol de pruebas están coloreadas según su estado. árbol de prueba
distingue entre los siguientes estados.
actual (azul por defecto)
La rama actual es la rama desde la raíz del árbol de prueba hasta la rama actual
Gol.
no probado (color de primer plano predeterminado)
Una rama no está probada si contiene objetivos de prueba abiertos.
resultó incompleto (cian por defecto)
Una rama incompletamente probada tiene su prueba terminada, pero algunas de las
las variables que se han introducido en esta rama no están (todavía) instanciadas.
probado parcialmente (verde oscuro por defecto)
En una rama parcialmente probada, todas las variables existenciales de la rama misma son
instanciadas, pero algunas de esas instanciaciones contienen variables existenciales que
no están (todavía) instanciados.
probado completo (verde por defecto)
Se demuestra que una rama está completa si todas sus variables existenciales se instancian con
términos que en sí mismos no contienen ninguna variable existencial.
engañado (rojo por defecto)
Una rama engañada contiene un comando de prueba de trampa, como admitir
Los colores así como muchos otros árbol de prueba los parámetros se pueden cambiar en el árbol de prueba
Configuration Diálogo (vea abajo).
Navegación
Cuando el árbol de pruebas crece, uno puede navegar por una variedad de medios. Además de
barras de desplazamiento y las teclas habituales, se puede mover el árbol de prueba arrastrando con el botón 1 del ratón
presionado. De forma predeterminada, arrastrar mueve la ventana gráfica (es decir, el árbol de prueba debajo se mueve en
la dirección opuesta). Después de establecer un valor negativo para Arrastre (Resistencia) aceleración en la sección de
árbol de prueba Configuration Diálogo, arrastrando moverá el árbol de prueba en su lugar (es decir, la prueba
el árbol se mueve en la misma dirección que el mouse).
Consecuente Visualización
La siguiente pantalla debajo del árbol de pruebas normalmente muestra el ancestro secuente del
objetivo actual. Con un solo clic izquierdo del mouse, uno puede mostrar cualquier objetivo o comando de prueba en
la pantalla siguiente. Un solo clic fuera del árbol de prueba volverá a los valores predeterminados
comportamiento. El tamaño inicial de la pantalla siguiente se puede configurar en el árbol de prueba
Configuration Diálogo. Un valor de 0 oculta la pantalla siguiente.
Propinas
Los comandos de prueba abreviados y las secuencias se muestran en su totalidad como información sobre herramientas cuando el mouse
el puntero descansa sobre ellos. Tanto la información sobre herramientas para comandos de prueba abreviados como para
Las secuencias se pueden desconectar de forma independiente en el árbol de prueba Configuration Diálogo.
También se puede configurar la longitud a la que se abrevian los comandos de prueba.
Beneficios adicionales Pantalla
Un doble clic o shift-clic muestra cualquier objetivo o comando de prueba en una
ventana. Estas ventanas adicionales se eliminan cuando desaparece la ventana principal del árbol de pruebas,
a menos que su Fijo (Sticky) se presiona el botón.
Existencial Variables
árbol de prueba realiza un seguimiento de las variables existenciales, ya sea que hayan sido instanciadas y
si dependen de algún otro existencial no instanciado (todavía). Utiliza diferentes
colores para ramas probadas que contienen variables existenciales no instanciadas y
ramas que solo dependen de algunas existenciales no instanciadas. La lista de actualmente no
(aún) las variables existenciales instanciadas se añaden a los comandos de prueba y las secuencias en
consejos sobre herramientas y otras pantallas.
La Existencial Variable Diálogo muestra una tabla con todas las variables existenciales del
prueba actual y sus dependencias. Cada línea de la tabla contiene un botón que marca
el comando de prueba que introdujo esta variable (con fondo amarillo, por defecto) y,
si está presente, el comando de prueba que instancia esta variable (con fondo naranja, por
defecto).
Main Menú
La Menú El botón muestra el menú principal. los Clon elemento clona el árbol de prueba actual en un
ventana adicional. Esta ventana adicional continúa mostrando una instantánea del clonado
árbol de pruebas, pase lo que pase con la prueba original.
La Mostrar corriente El elemento mueve la ventana gráfica al árbol de pruebas de modo que la prueba actual
objetivo (si hay alguno) será visible.
La Exit el artículo termina árbol de prueba y cierra todas las pantallas del árbol de pruebas.
Los tres elementos restantes muestran, respectivamente, la árbol de prueba Configuration Diálogo y
el Ayuda y Acerca de ventanas
Contexto Menú
Un clic derecho muestra el Contexto Menú, que contiene elementos adicionales.
El objeto deshacer a punto está activo sobre los nodos siguientes en el árbol de prueba. Entonces envía un
retirar o deshacer la solicitud a Proof General que retrae el búfer de scripting hasta ese
consecuente.
Los artículos recuadro comando y recuadro subprueba están activos sobre comandos de prueba. Ellos enviaron,
respectivamente, el comando de prueba seleccionado o todos los comandos de prueba en el subárbol seleccionado, para
Proof General, que los inserta en el punto.
CONFIGURACIÓN
árbol de prueba Configuration Diálogo
Los cambios en el cuadro de diálogo de configuración solo tienen efecto cuando el Aplica or OK el botón es
presionado. los Guarde El botón almacena la configuración actual (como calculada OCaml registro) en
~ / .prooftree, que sobrescribirá la configuración predeterminada incorporada para lo siguiente
árbol de prueba carreras. los Restaurar El botón carga y aplica la configuración guardada.
Pruebas General Personalización
La ubicación de la árbol de prueba ejecutable y los argumentos de la línea de comando están en el
grupo de personalización árbol de prueba. Probar puntos específicos, como las expresiones regulares.
para los comandos de navegación y trampa están en el grupo de personalización prueba-arbol-interior.
Para visitar un grupo de personalización, escriba Mx personalizar-grupo seguido del nombre del
grupo de personalización dentro Pruebas General.
LIMITACIONES
Para los ensayos clínicos de CRISPR, gallo, las pruebas deben iniciarse con el comando Pruebas, que es la práctica recomendada
de todos modos (consulte el informe de problemas de Coq 2776).
REQUISITOS
Esta versión de árbol de prueba requiere gallo 8.4beta o mejor y Pruebas General 4.3pre130327 o
mejor.
Utilice prooftree en línea utilizando los servicios de onworks.net
