EnglishFrenchSpanish

OnWorks favicon

coqchk.opt - Online in the Cloud

Run coqchk.opt in OnWorks free hosting provider over Ubuntu Online, Fedora Online, Windows online emulator or MAC OS online emulator

This is the command coqchk.opt 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


coqchk - The Coq Proof Checker compiled libraries verifier

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

Use coqchk.opt online using onworks.net services


Free Servers & Workstations

Download Windows & Linux apps

  • 1
    KompoZer
    KompoZer
    KompoZer is a wysiwyg HTML editor using
    the Mozilla Composer codebase. As
    Nvu's development has been stopped
    in 2005, KompoZer fixes many bugs and
    adds a f...
    Download KompoZer
  • 2
    Free Manga Downloader
    Free Manga Downloader
    The Free Manga Downloader (FMD) is an
    open source application written in
    Object-Pascal for managing and
    downloading manga from various websites.
    This is a mirr...
    Download Free Manga Downloader
  • 3
    UNetbootin
    UNetbootin
    UNetbootin allows you to create bootable
    Live USB drives for Ubuntu, Fedora, and
    other Linux distributions without
    burning a CD. It runs on Windows, Linux,
    and ...
    Download UNetbootin
  • 4
    Dolibarr ERP - CRM
    Dolibarr ERP - CRM
    Dolibarr ERP - CRM is an easy to use
    ERP and CRM open source software package
    (run with a web php server or as
    standalone software) for businesses,
    foundations...
    Download Dolibarr ERP - CRM
  • 5
    SQuirreL SQL Client
    SQuirreL SQL Client
    SQuirreL SQL Client is a graphical SQL
    client written in Java that will allow
    you to view the structure of a JDBC
    compliant database, browse the data in
    tables...
    Download SQuirreL SQL Client
  • 6
    Brackets
    Brackets
    Brackets is a free, modern open-source
    text editor made especially for Web
    Development. Written in HTML, CSS, and
    JavaScript with focused visual tools and
    prepr...
    Download Brackets
  • More »

Linux commands

Ad