Ito ang command na coqmktop na maaaring patakbuhin sa OnWorks na libreng hosting provider gamit ang isa sa aming maramihang libreng online na workstation gaya ng Ubuntu Online, Fedora Online, Windows online emulator o MAC OS online emulator
PROGRAMA:
NAME
coqmktop - Ang Coq Proof Assistant user-tactics linker
SINOPSIS
coqmktop [ pagpipilian ] file
DESCRIPTION
coqmktop bubuo ng bagong Coq toplevel na pinalawig gamit ang mga taktika ng gumagamit. file ay ang Layunin
Caml object o library file (ibig sabihin, may suffix na .cmo, .cmx, .cma o .cmxa) para i-link sa
Sistema ng Coq. Ang linker ay gumagawa ng isang executable na Coq toplevel na maaaring direktang tawagan
o sa pamamagitan ng coqc(1), gamit ang -image na opsyon.
Opsyon
-h Tulong. Ilista ang mga magagamit na opsyon.
-srcdir dir
Tukuyin kung nasaan ang mga source file ng Coq
-o exec-file
Tukuyin ang pangalan ng resultang toplevel
-optino Mag-compile sa native code
-puno I-link ang mga taktika sa mataas na antas
-tuktok Bumuo ng Coq sa isang ocaml toplevel (hindi tugma sa -optino)
-R dir Tukuyin ang recursively na mga direktoryo para sa Ocaml
-v8 Link sa V8 grammar
Gumamit ng coqmktop online gamit ang mga serbisyo ng onworks.net
