Este es el comando coqmktop 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
coqmktop - El enlazador de tácticas de usuario de Coq Proof Assistant
SINOPSIS
coqmktop [ opciones ] archivos
DESCRIPCIÓN
coqmktop construye un nuevo nivel superior de Coq ampliado con tácticas de usuario. archivos son el objetivo
Objeto Caml o archivos de biblioteca (es decir, con sufijo .cmo, .cmx, .cma o .cmxa) para vincular con el
Sistema Coq. El enlazador produce un nivel superior de Coq ejecutable que se puede llamar directamente
o a través de coqc(1), usando la opción -image.
OPCIONES
-h Ayudar. Enumere las opciones disponibles.
-srcdir dir
Especificar dónde están los archivos fuente de Coq
-o archivo-exec
Especifique el nombre del nivel superior resultante
-optar Compilar en código nativo
-completo Vincular tácticas de alto nivel
-parte superior Construya Coq en un nivel superior ocaml (incompatible con -optar)
-R dir Especificar directorios de forma recursiva para Ocaml
-v8 Enlace con la gramática V8
Use coqmktop en línea usando los servicios de onworks.net