coqtop(1)

Usage

coqtop [options]

Overview

coqtop is the toplevel system of Coq, for interactive use. It reads phrases on the standard input, and prints results on the standard output. For batch-oriented use of Coq, see coqc(1).

Options

-h, --help: Help. Will give you the complete list of options accepted by coqtop.

`-I dir, --include dir`	Add directory dir in the include path.
`-R dir coqdir`	Recursively map physical dir to logical coqdir.
`-top coqdir`	Set the toplevel name to be coqdir instead of Top.

-nois: Start with an empty initial state.

`-load-ml-source filename`	Load ML file filename.
`-load-ml-object filename`	Load ML object file filenname.
`-load-vernac-source filename, -l filename`	Load Coq file filename.v. (Load filename.)
`-load-vernac-source-verbose filename, -lv filename`	Load verbosely Coq file filename.v. (Load Verbose filename.)
`-require lib`	Load Coq library lib. (Require lib.)
`-require-import lib, -ri lib`	Load Coq library lib and import it. (Require Import lib.)
`-require-export lib, -re lib`	Load Coq library lib and transitively import it. (Require Export lib.)
`-require-from root lib, -rfrom root lib`	Load Coq library lib. (From root Require lib.)
`-require-import-from root lib, -rifrom root lib`	Load Coq library lib and import it. (From root Require Import lib.)
`-require-export-from root lib, -refrom root lib`	Load Coq library lib and transitively import it. (From root Require Export lib.)
`-load-vernac-object lib`	Obsolete synonym of `-require`.

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

-v: Print Coq version and exit.

-q: Skip loading of rcfile (resource file) if any.

-init-file filename: Set the rcfile to filename.

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

-emacs: Tells Coq it is executed under Emacs.

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

-impredicative-set: Set sort Set impredicative.

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

Releases

14 releases since Debian 2.2 (Potato); the text changed 9 times.

--help since Debian 5.0 (Lenny); -batch since Debian 5.0 (Lenny); -dont-load-proofs since Debian 5.0 (Lenny); -emacs since Debian 5.0 (Lenny); -h since Debian 3.0 (Woody); -impredicative-set since Debian 5.0 (Lenny); -nois since Debian 5.0 (Lenny); -q since Debian 5.0 (Lenny); -v since Debian 5.0 (Lenny); -where since Debian 5.0 (Lenny).

-boot until Debian 10 (Buster); -byte until Debian 8 (Jessie); -debug until Debian 2.2 (Potato); -full until Debian 2.2 (Potato); -notactics until Debian 2.2 (Potato); -opt until Debian 8 (Jessie); -outputstate until Debian 8 (Jessie); -quality until Debian 8 (Jessie); -searchisos until Debian 2.2 (Potato); -xml until Debian 9 (Stretch).

Referred to by

coqc(1) Coq compiler coqchk(1) verify compiled Coq libraries coqide(1) graphical interface for the Coq proof assistant coq-tex(1) process Coq phrases embedded in LaTeX files coqmktop(1) The Coq Proof Assistant user-tactics linker coqc.byte(1) Coq compiler coqnative(1) native Coq compiler coq-parser(1) Coq parser coq_vo2xml(1) Exports the content of a Coq module to XML coqchk.opt(1) verify compiled Coq libraries coqide.opt(1) graphical interface for the Coq proof assistant coqtop.opt(1) The native-code Coq toplevel coqide.byte(1) graphical interface for the Coq proof assistant coqtop.byte(1) bytecode toplevel Coq system coq_makefile(1) generate makefiles for Coq proof development coq-interface(1) Customized Coq toplevel to make user interfaces coq-parser.opt(1) Coq parser coq-interface.opt(1) Customized Coq toplevel to make user interfaces

Usage

Overview

Options

Releases

See also

Mentioned on this page

Referred to by