Este es el comando coqchk 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
coqchk - El verificador de bibliotecas compiladas Coq Proof Checker
SINOPSIS
coqchk [ opciones ] módulos
DESCRIPCIÓN
coqchk es el verificador independiente de bibliotecas compiladas (archivos .vo producidos por coqc) para
el Asistente de pruebas de Coq. Consulte el Manual de referencia para obtener más información. Vuelve con
código de salida 0 si todas las tareas solicitadas se realizaron correctamente. Un código de retorno distinto de cero significa que
algo salió mal: no se encontró alguna biblioteca, contenido dañado, verificación de tipos
fracaso, etc.
módulos es una lista de módulos que se deben verificar. Se puede hacer referencia a los módulos mediante un
nombre calificado.
OPCIONES
-I es, --incluir dir
agregar directorio dir en la ruta de inclusión
-R dir coqdir
mapear recursivamente físico dir a la lógica coqdir
-silencio
hace que coqchk sea menos detallado.
-admitir módulo
etiquetar el módulo especificado y todas sus dependencias como de confianza, y no se
se vuelve a comprobar, a menos que otras opciones lo soliciten explícitamente.
-norec módulo
especifica que el módulo dado debe ser verificado sin solicitar verificar su
dependencias.
-metro, --memoria
muestra un resumen de la memoria utilizada por el verificador.
-Oh, --contexto de salida
muestra un resumen del contenido lógico que se ha verificado: supuestos y
uso de la impredicatividad.
-conjunto-impredicativo
permite que el verificador acepte bibliotecas que se han compilado con este indicador.
-v imprima la versión coqchk y salga.
-coqlib dir
anula la ubicación predeterminada de la biblioteca estándar.
-dónde imprima la ubicación de la biblioteca estándar de coqchk y salga.
-h, --ayuda
imprimir lista de opciones
Use coqchk en línea usando los servicios de onworks.net
