Este es el comando coqdoc 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
coqdoc: una herramienta de documentación para el asistente de pruebas de Coq
SINOPSIS
coqdoc [ opciones ] archivos
DESCRIPCIÓN
coqdoc es una herramienta de documentación para el asistente de pruebas Coq. Crea LaTeX o HTML
documentos de un conjunto de archivos Coq. Consulte el manual de referencia de Coq para obtener documentación (url
abajo).
OPCIONES
En general opciones
-h Ayudar. Le dará la lista completa de opciones aceptadas por coqdoc.
--html Seleccione una salida HTML.
--látex
Seleccione una salida LATEX.
--dvi Seleccione una salida DVI.
--PD Seleccione una salida PostScript.
--texmacs
Seleccione una salida de TeXmacs.
--salida estándar
Redirigir la salida a stdout
-o archivo,--producción presentar
Redirigir la salida al archivo archivo.
-d es, --directorio dir
Archivos de salida al directorio dir en lugar del directorio actual (la opción -d no
cambie el nombre de archivo especificado con la opción -o, si corresponde).
-s, --pequeño
No inserte títulos para los archivos. El comportamiento predeterminado es insertar un título como
`` Library Foo '' para cada archivo.
-t cuerda, --título cadena
Establezca el título del documento.
--solo cuerpo
Suprima el encabezado y el final del documento final. Por lo tanto, puede insertar el
documento resultante en uno más grande.
-p cuerda, --preámbulo cadena
Inserta algo de material en el preámbulo de LATEX, justo antes de \ begin {document}
(sin sentido con -html).
- archivo vernac archivo, --archivo tex presentar
Considera el archivo "archivo" respectivamente como un archivo .v (o .g) o un archivo .tex.
--archivos-de presentar
Lea los nombres de los archivos para procesarlos en el archivo `archivo 'como si se hubieran dado en el comando
línea. Útil para fuentes de programas divididas en varios directorios.
-q, --tranquilo
Tranquilizarse. No imprima nada excepto errores.
-h, --ayuda
Dé un breve resumen de las opciones y salga.
-v, --versión
Imprime la versión y sal.
Home opciones
El comportamiento predeterminado es crear un índice, solo para la salida HTML, en index.html.
--sin índice
No imprima el índice.
--multi-índice
Genere una página para cada categoría y cada letra del índice, junto con una
página superior index.html.
Mesa of contenido opción
-toc, --Tabla de contenido
Inserte una tabla de contenido. Para una salida LATEX, inserta un \ tableofcontents en
el comienzo del documento. Para una salida HTML, crea una tabla de contenido.
en toc.html.
Los hipervínculos opciones
--globo de presentar
Haga referencias utilizando globalizaciones de Coq desde archivo. (Tales globalizaciones son
obtenido con la opción Coq -dump-glob).
--no-externos
No inserte enlaces a la biblioteca estándar de Coq.
--externo url librero
Establezca la URL base para la biblioteca externa cuyo prefijo raíz es libroot.
--coqlib url
Establecer URL base para la biblioteca estándar de Coq (la predeterminada es
http://coq.inria.fr/library/).
--coqlib_ruta dir
Establezca la ruta base donde se instalan los archivos Coq, especialmente los archivos de estilo
coqdoc.sty y coqdoc.css.
-R dir coqdir
Asigne el directorio del directorio físico al directorio lógico de Coq coqdir (de manera similar a la opción Coq
-R). Nota: La opción -R solo tiene efecto en los archivos que la siguen en el comando
línea, por lo que probablemente necesitará poner esta opción primero.
Contenido opciones
-gramo, --gallina
No imprima pruebas.
-yo, --luz
Modo de luz. Suprime las pruebas (como con -g) y los siguientes comandos:
* Definición de táctica [recursiva]
* Sugerencia / sugerencias
* Exigir
* Transparente / Opaco
* Argumento / Implicitos implícitos
* Sección / Variable / Hipótesis / Fin
El comportamiento de las opciones -g y -l se puede anular localmente usando (* begin show
*) ... (* end show *) entorno (ver arriba).
Idioma opciones
El comportamiento predeterminado es asumir archivos de entrada ASCII de 7 bits.
-latino1, --latín1
Seleccione los archivos de entrada ISO-8859-1. Es equivalente a --inputenc latin1 --charset
iso-8859-1.
-utf8, --utf8
Seleccione archivos de entrada UTF-8 (Unicode). Es equivalente a --inputenc utf8 --charset
utf-8. La compatibilidad con LATEX UTF-8 se puede encontrar en
http://www.ctan.org/tex-archive/macros/latex/contrib/supported/unicode/.
--entrada cadena
Proporcione una codificación de entrada LATEX, como una opción para el paquete LATEX inputenc.
--juego de caracteres cadena
Especifique el juego de caracteres HTML que se insertará en el encabezado HTML.
Use coqdoc en línea usando los servicios de onworks.net