Questo è il comando coqmktop che può essere eseguito nel provider di hosting gratuito OnWorks utilizzando una delle nostre molteplici workstation online gratuite come Ubuntu Online, Fedora Online, emulatore online Windows o emulatore online MAC OS
PROGRAMMA:
NOME
coqmktop - Il linker di tattiche utente di Coq Proof Assistant
SINOSSI
coqmktop [ Opzioni ] file
DESCRIZIONE
coqmktop costruisce un nuovo livello superiore di Coq esteso con le tattiche dell'utente. file sono l'obiettivo
File oggetto o libreria Caml (cioè con suffisso .cmo, .cmx, .cma o .cmxa) da collegare al
Sistema Coq. Il linker produce un eseguibile Coq toplevel che può essere chiamato direttamente
o attraverso coqc(1), utilizzando l'opzione -image.
VERSIONI
-h Aiuto. Elenca le opzioni disponibili.
-srcdir dir
Specificare dove si trovano i file sorgente Coq
-o file-exec
Specificare il nome del livello superiore risultante
-optare Compila in codice nativo
-pieno Collega tattiche di alto livello
-superiore Costruisci Coq su un toplevel ocaml (incompatibile con -optare)
-R dir Specifica ricorsivamente le directory per Ocaml
-v8 Collegamento con la grammatica V8
Usa coqmktop online utilizzando i servizi onworks.net
