This is the command coqmktop that can be run in the OnWorks free hosting provider using one of our multiple free online workstations such as Ubuntu Online, Fedora Online, Windows online emulator or MAC OS online emulator
coqmktop - The Coq Proof Assistant user-tactics linker
coqmktop [ options ] files
coqmktop builds a new Coq toplevel extended with user-tactics. files are the Objective
Caml object or library files (i.e. with suffix .cmo, .cmx, .cma or .cmxa) to link with the
Coq system. The linker produces an executable Coq toplevel which can be called directly
or through coqc(1), using the -image option.
-h Help. List the available options.
Specify where the Coq source files are
Specify the name of the resulting toplevel
-opt Compile in native code
-full Link high level tactics
-top Build Coq on a ocaml toplevel (incompatible with -opt)
-R dir Specify recursively directories for Ocaml
-v8 Link with V8 grammar
Use coqmktop online using onworks.net services