Este es el comando coqide.byte 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
coqide - La interfaz gráfica Coq Proof Assistant
SINOPSIS
coquide [ opciones ]
DESCRIPCIÓN
coquide es una interfaz gráfica gtk para el asistente de pruebas Coq.
Para el uso de Coq orientado a la línea de comandos, consulte coqueta(1); para el uso de Coq orientado a lotes, consulte
coqc(1).
CAMPUS
-h Mostrar la lista completa de opciones aceptadas por coquide.
-I dir, -incluir dir
Agregue directorio de directorio en la ruta de inclusión.
-R dir coqdir
Mapeo físico recursivo dir a la lógica coqdir.
-origen Agregue directorios de origen en la ruta de inclusión.
-es f, -estado de entrada f
Leer estado de f.coq.
-ruido Comience con un estado vacío.
estado de salida f
Escribir estado en archivo f.coq.
-carga-ml-objeto f
Cargar archivo de objeto ML f.
-carga-ml-fuente f
Cargar archivo ML f.
-l f, -cargar-fuente-vernac f
Cargar archivo Coq f.v (Cargar f.).
-lv f, -load-vernac-fuente-detallada f
Cargar archivo Coq f.v (carga detallada f.).
-cargar-objeto-vernac f
Cargar archivo de objeto Coq f.vo.
-exigir f
Cargar archivo de objeto Coq f.vo e importarlo (Requerir f.).
-compilar f
Compilar archivo Coq f.v (implica -lote).
-compilar-detallado f
Compilar detalladamente el archivo Coq f.v (implica -lote).
-optar Ejecute la versión de código nativo de Coq o Coq_SearchIsos.
-byte Ejecute la versión de código de bytes de Coq o Coq_SearchIsos.
-dónde Imprima la ubicación de la biblioteca estándar de Coq y salga.
-v Imprime la versión de Coq y sal.
-q Omitir la carga de rcfile.
-archivo-inicial f
Establezca el rcfile en f.
-lote Modo por lotes (sale justo después del análisis de argumentos).
-bota Modo de arranque (implica -q y -lote).
-emacs Le dice a Coq que se ejecuta en Emacs.
-volcado-glob f
Volcar globalizaciones en archivo f (ser usado por coqdoc(1)).
-conjunto-impredicativo
Establecer ordenación Establecer impredicativo.
-no-pruebas-de-carga
No cargue pruebas opacas en la memoria.
-xml Exportar archivos XML a la jerarquía enraizada en el directorio
COQ_XML_LIBRARY_ROOT (si está configurado) o stdout (si no está configurado).
Use coqide.byte en línea usando los servicios de onworks.net
