Skip site navigation (1)Skip section navigation (2)

FreeBSD Manual Pages


home | help
COQ(1)			    General Commands Manual			COQ(1)

       coqchk -	The Coq	Proof Checker compiled libraries verifier

       coqchk [	options	] modules

       coqchk  is the standalone checker of compiled libraries (.vo files pro-
       duced 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.

       -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.

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

       -norec module
	      specifies	 that  the  given module shall be verified without re-
	      questing 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	 veri-
	      fied: assumptions	and usage of impredicativity.

	      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

       coqtop(1), coqc(1), coq_makefile(1), coqdep(1).
       The Coq Reference Manual.  The Coq web site:

				  July 7, 201				COQ(1)


Want to link to this manual page? Use this URL:

home | help