Este es el comando coqdep 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
coqdep: calcula las dependencias entre módulos para los programas Coq y Caml
SINOPSIS
coqdep [ -w ] [ -I directorio ] [ -coqlib directorio ] [ -c ] [ -i ] [ -D ] [ -barra oblicua ]
nombre de archivo ... directorio ...
DESCRIPCIÓN
coqdep calcula las dependencias entre módulos para los programas Coq y Caml, e imprime el
dependencias de la salida estándar en un formato legible por make. Cuando un directorio es
dado como argumento, se mira de forma recursiva.
Las dependencias de los módulos Coq se calculan observando Exigir comandos (Requerir, Requerir
Exportar, Requerir Importación), Declarar ML Módulo comandos y Carga comandos. Dependencias
en relación con los módulos de la biblioteca Coq no se imprimen.
Las dependencias de los módulos Caml se calculan observando abierto directivas y el punto
notación módulo.valor.
CAMPUS
-c Imprime las dependencias de los módulos Caml. (En los módulos Caml, el comportamiento es
exactamente igual que ocamldep).
-w Imprime una advertencia si un comando Coq Declarar ML Módulo Es incorrecto. (Por ejemplo,
escribiste `Declare ML Module" A ". ', pero el módulo A contiene #open" B "). los
Se imprime el comando correcto (ver opción -D). La advertencia está impresa en estándar
error.
-D Este comando busca cada comando Declarar ML Módulo de cada archivo Coq dado como
argumento y complete (si es necesario) la lista de módulos Caml. El nuevo comando es
impreso en la salida estándar. No se calcula ninguna dependencia con esta opción.
-barra oblicua Imprime rutas con una barra en lugar del separador específico del sistema operativo. Esta opcion es
útil cuando se desarrolla bajo Cygwin.
-I directorio
Los archivos .v .ml .mli del directorio directorio se tienen en cuenta durante la
cálculo de dependencias, pero sus propias dependencias no se imprimen.
-coqlib directorio
Indica dónde está la biblioteca Coq. El valor predeterminado se ha determinado en
tiempo de instalación y, por lo tanto, esta opción no debe utilizarse en condiciones normales.
circunstancias.
Use coqdep en línea usando los servicios de onworks.net
