This is the command coqchk 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
coqchk - The Coq Proof Checker compiled libraries verifier
coqchk [ options ] modules
coqchk is the standalone checker of compiled libraries (.vo files produced by coqc) for
the Coq Proof Assistant. See the Reference Manual for more information. It returns with
exit code 0 if all the requested tasks succeeded. A non-zero return code means that
something went wrong: some library was not found, corrupted content, type-checking
modules is a list of modules to be checked. Modules can be referred to by a short or
-I dir, --include dir
add directory dir in the include path
-R dir coqdir
recursively map physical dir to logical coqdir
makes coqchk less verbose.
tag the specified module and all its dependencies as trusted, and will not be
rechecked, unless explicitly requested by other options.
specifies that the given module shall be verified without requesting to check its
displays a summary of the memory used by the checker.
displays a summary of the logical content that have been verified: assumptions and
usage of impredicativity.
allows the checker to accept libraries that have been compiled with this flag.
-v print coqchk version and exit.
overrides the default location of the standard library.
-where print coqchk standard library location and exit.
print list of options
Use coqchk online using onworks.net services