GSP
Quick Navigator

Search Site

Unix VPS
A - Starter
B - Basic
C - Preferred
D - Commercial
MPS - Dedicated
Previous VPSs
* Sign Up! *

Support
Contact Us
Online Help
Handbooks
Domain Status
Man Pages

FAQ
Virtual Servers
Pricing
Billing
Technical

Network
Facilities
Connectivity
Topology Map

Miscellaneous
Server Agreement
Year 2038
Credits
 

USA Flag

 

 

Man Pages


Manual Reference Pages  -  COQCHK (1)

NAME

coqchk - The Coq Proof Checker compiled libraries verifier

CONTENTS

Synopsis
Description
Options
See Also

SYNOPSIS

coqchk [ options ] modules

DESCRIPTION

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 failure, etc.

modules is a list of modules to be checked. Modules can be referred to by a short or qualified name.

OPTIONS

-I dir, --include dir
  add directory dir in the include path

-R dir coqdir
  recursively map physical dir to logical coqdir

-silent makes coqchk less verbose.

-admit module
  tag the specified module and all its dependencies as trusted, and will not be rechecked, unless explicitly requested by other options.

-norec module
  specifies that the given module shall be verified without requesting to check its dependencies.

-m, --memory
  displays a summary of the memory used by the checker.

-o, --output-context
  displays a summary of the logical content that have been verified: assumptions and usage of impredicativity.

-impredicative-set
  allows the checker to accept libraries that have been compiled with this flag.

-v print coqchk version and exit.

-coqlib dir
  overrides the default location of the standard library.

-where print coqchk standard library location and exit.

-h, --help print list of options

SEE ALSO

coqtop(1), coqc(1), coq_makefile(1), coqdep(1).
The Coq Reference Manual. The Coq web site: http://coq.inria.fr

Search for    or go to Top of page |  Section 1 |  Main Index


--> COQ (1) July 7, 201

Powered by GSP Visit the GSP FreeBSD Man Page Interface.
Output converted with manServer 1.07.