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
PROGRAM:
NAME
coqmktop - The Coq Proof Assistant user-tactics linker
SYNOPSIS
coqmktop [ options ] files
DESCRIPTION
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.
OPTIONS
-h Help. List the available options.
-srcdir dir
Specify where the Coq source files are
-o exec-file
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