EnglishFrenchSpanish

OnWorks favicon

coqide.byte - Online in the Cloud

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

This is the command coqide.byte 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


coqide - The Coq Proof Assistant graphical interface

SYNOPSIS


coqide [ options ]

DESCRIPTION


coqide is a gtk graphical interface for the Coq proof assistant.

For command-line-oriented use of Coq, see coqtop(1) ; for batch-oriented use of Coq, see
coqc(1).

OPTIONS


-h Show the complete list of options accepted by coqide.

-I dir, -include dir
Add directory dir in the include path.

-R dir coqdir
Recursively map physical dir to logical coqdir.

-src Add source directories in the include path.

-is f, -inputstate f
Read state from f.coq.

-nois Start with an empty state.

-outputstate f
Write state in file f.coq.

-load-ml-object f
Load ML object file f.

-load-ml-source f
Load ML file f.

-l f, -load-vernac-source f
Load Coq file f.v (Load f.).

-lv f, -load-vernac-source-verbose f
Load Coq file f.v (Load Verbose f.).

-load-vernac-object f
Load Coq object file f.vo.

-require f
Load Coq object file f.vo and import it (Require f.).

-compile f
Compile Coq file f.v (implies -batch).

-compile-verbose f
Verbosely compile Coq file f.v (implies -batch).

-opt Run the native-code version of Coq or Coq_SearchIsos.

-byte Run the bytecode version of Coq or Coq_SearchIsos.

-where Print Coq's standard library location and exit.

-v Print Coq version and exit.

-q Skip loading of rcfile.

-init-file f
Set the rcfile to f.

-batch Batch mode (exits just after arguments parsing).

-boot Boot mode (implies -q and -batch).

-emacs Tells Coq it is executed under Emacs.

-dump-glob f
Dump globalizations in file f (to be used by coqdoc(1)).

-impredicative-set
Set sort Set impredicative.

-dont-load-proofs
Don't load opaque proofs in memory.

-xml Export XML files either to the hierarchy rooted in the directory
COQ_XML_LIBRARY_ROOT (if set) or to stdout (if unset).

Use coqide.byte online using onworks.net services


Free Servers & Workstations

Download Windows & Linux apps

Linux commands

  • 1
    a2j_control
    a2j_control
    a2j_control - utility to control
    a2jmidid daemon ...
    Run a2j_control
  • 2
    a2mp3
    a2mp3
    a2mp3 - program to optimize your music
    for your mp3 player ...
    Run a2mp3
  • 3
    create_common
    create_common
    ctn_manpage - Generic CTN manual page
    DESCRIPTION: This is a generic manual
    package for a CTN program. All CTN
    programs will give their brief usage
    synopsis wh...
    Run create_common
  • 4
    create_compressed_fs
    create_compressed_fs
    create_compressed_fs,
    extract_compressed_fs - convert and
    extract a filesystem to/from a cloop
    volume ...
    Run create_compressed_fs
  • 5
    gapi2-codegen
    gapi2-codegen
    undocumented - No manpage for this
    program. DESCRIPTION: This program does
    not have a manpage. Run this command
    with the help switch to see what it
    does. For f...
    Run gapi2-codegen
  • 6
    gapi2-fixup
    gapi2-fixup
    undocumented - No manpage for this
    program. DESCRIPTION: This program does
    not have a manpage. Run this command
    with the help switch to see what it
    does. For f...
    Run gapi2-fixup
  • More »

Ad