Aceasta este comanda coqmktop care poate fi rulată în furnizorul de găzduire gratuit OnWorks folosind una dintre multiplele noastre stații de lucru online gratuite, cum ar fi Ubuntu Online, Fedora Online, emulator online Windows sau emulator online MAC OS
PROGRAM:
NUME
coqmktop - Linkerul de tactici utilizator Coq Proof Assistant
REZUMAT
coqmktop [ Opțiuni ] fișiere
DESCRIERE
coqmktop construiește un nou nivel superior Coq extins cu tactici de utilizator. fișiere sunt Obiectivul
Obiecte Caml sau fișiere de bibliotecă (adică cu sufixul .cmo, .cmx, .cma sau .cmxa) pentru a le conecta cu
Sistemul Coq. Linker-ul produce un nivel superior Coq executabil care poate fi apelat direct
sau prin coqc(1), folosind opțiunea -image.
OPŢIUNI
-h Ajutor. Listați opțiunile disponibile.
-srcdir dir
Specificați unde sunt fișierele sursă Coq
-o exec-file
Specificați numele nivelului superior rezultat
-opta Compilați în cod nativ
-deplin Legați tactici de nivel înalt
-top Construiți Coq pe un nivel superior ocaml (incompatibil cu -opta)
-R dir Specificați în mod recursiv directoare pentru Ocaml
-v8 Legătură cu gramatica V8
Utilizați coqmktop online folosind serviciile onworks.net
