coqchk man page on DragonFly

Man page or keyword search:  
man Server   44335 pages
apropos Keyword Search (all sections)
Output format
DragonFly logo
[printable version]

COQ(1)									COQ(1)

NAME
       coqchk - The Coq Proof Checker compiled libraries verifier

SYNOPSIS
       coqchk [ options ] modules

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

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	 veri‐
	      fied: 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

				  July 7, 201				COQ(1)
[top]

List of man pages available for DragonFly

Copyright (c) for man pages and the logo by the respective OS vendor.

For those who want to learn more, the polarhome community provides shell access and support.

[legal] [privacy] [GNU] [policy] [cookies] [netiquette] [sponsors] [FAQ]
Tweet
Polarhome, production since 1999.
Member of Polarhome portal.
Based on Fawad Halim's script.
....................................................................
Vote for polarhome
Free Shell Accounts :: the biggest list on the net